Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover
Just 100 training examples can restore a specialized AI's lost ability to use tools — suggesting fine-tuning damage is often reversible, not permanent.
The Thesis
When you train a general-purpose AI model intensively on a narrow domain, it can lose capabilities it previously had — a phenomenon this paper calls 'agentic collapse.' The authors show this using Goedel-Prover-V2, a model trained on 1.8 million formal mathematics examples that almost completely lost the ability to call external tools (dropping from 89.4% accuracy to near zero). The surprising finding is that this collapse is not permanent: retraining on as few as 100 carefully chosen examples from a related domain — in this case, using a proof assistant called Lean to search a math library — restores the capability broadly. The restored tool-use skill transfers to entirely different benchmarks the recovery data never touched, suggesting the base model's knowledge was suppressed rather than deleted. The catch is that this has been demonstrated in one specialized domain, and we do not yet know how reliably the principle generalizes across other AI systems or task types.
Catalyst
The broader AI community is actively deploying heavily fine-tuned 'specialist' models for legal, medical, coding, and scientific tasks — and only now encountering systematic evidence that domain fine-tuning can silently erase general capabilities. The availability of open-source base models like DeepSeek and their fine-tuned derivatives makes this phenomenon reproducible and economically relevant. Simultaneously, the rise of agentic AI workflows — where models must call APIs, search databases, and coordinate tools — makes tool-use regression a practical deployment failure, not just an academic curiosity.
What's New
Prior work on 'catastrophic forgetting' in neural networks focused mainly on losing factual knowledge or reasoning skills after continued training. This paper identifies a specific and practically important variant: the loss of structured behavioral skills like tool-calling, which require the model to produce syntactically correct function-call outputs. Earlier remedies typically required large, diverse replay datasets drawn from the original training distribution — expensive to curate and often proprietary. This paper proposes that a tiny amount of domain-adjacent agentic data (100 traces) is sufficient to reactivate suppressed skills, and demonstrates this with quantitative benchmarks including the Berkeley Function Calling Leaderboard.
The Counter
The entire result rests on a single model family in a single highly specialized domain — formal mathematics — which may be unusually amenable to this kind of recovery because the base model was extraordinarily capable before fine-tuning. It is far from clear that 100 examples would suffice for, say, a medical or legal model, where domain fine-tuning is more extensive and the original tool-use capability may have been weaker. The transfer to the Berkeley Function Calling Leaderboard is impressive on paper, but the gap between 83.8% and the base model's 89.4% still represents a meaningful regression in practical agentic workflows. There is also a chicken-and-egg problem: someone has to know the capability was lost in the first place, and identify the right 100 recovery examples — neither of which is trivial in a production deployment. Finally, the paper does not show whether the math-proving performance degrades after recovery fine-tuning, which would be the real cost-benefit tradeoff practitioners need to evaluate.
Longs
- MSFT — Azure AI fine-tuning infrastructure directly affected by specialist model deployment patterns
- IBM (IBM) — enterprise AI services built on fine-tuned foundation models for vertical domains
- SOUN — voice/agentic AI tool-calling pipelines benefit from robust function-call recovery
- PLTR — defense and enterprise agentic AI deployments where tool-use reliability is critical
- BOTZ (robotics/automation ETF) — robotic AI agents depend on reliable tool-use and API-calling behavior
Shorts
- Vendors selling 'domain-locked' fine-tuned models as premium products — if capability suppression is easily reversible, the value proposition of expensive full fine-tuning pipelines weakens
- Companies that built evaluation frameworks assuming fine-tuned models retain general capabilities — silent regressions may have gone undetected in shipped products
Enablers (Picks & Shovels)
- Lean 4 proof assistant and Mathlib library — the specific tool-use environment used to generate the 100 recovery traces
- Hugging Face (private) — open model hosting that makes fine-tuned specialist models like Goedel-Prover-V2 accessible for research
- Berkeley Function Calling Leaderboard — the external benchmark used to validate transfer of recovered capability
- DeepSeek open-source base models — the foundation from which Goedel-Prover-V2 was derived, making the experiment reproducible
Private Watchlist
- Imbue (private) — builds AI agents with robust tool use and reasoning, directly relevant domain
- Cognition AI (private) — developer of Devin, an agentic coding assistant reliant on reliable tool-calling
- Induced AI (private) — agentic workflow automation where tool-call fidelity is a core product requirement
- Morph Labs (private) — formal verification and theorem proving infrastructure
Resources
The Paper
Heavy supervised fine-tuning on a target domain can strongly suppress capabilities that were present in the base model. We study this phenomenon in formal mathematics using Goedel-Prover-V2, an open-source model heavily trained on 1.8 million formal-math examples. After domain specialization, the model almost completely loses its ability to produce valid tool calls, even when explicitly instructed to use tools, dropping from 89.4% function-calling accuracy in the base model to nearly 0%. We ask whether this agentic collapse is permanent or instead reversible. To answer this question, we fine-tune the specialized model on a small amount of Lean-specific tool-use data. Remarkably, as few as 100 agentic traces are sufficient to restore strong tool-calling behavior. Importantly, this recovery is not the result of reward hacking or benchmark-specific optimization: the recovery data is entirely drawn from the Lean setting, where the model uses natural-language queries to search the Mathlib library for relevant theorems and lemmas, yet the regained capability transfers well beyond that domain. In particular, these same 100 Lean-specific traces improve performance on the Berkeley Function Calling Leaderboard from near zero to 83.8%, approaching the base model's 89.4% despite the mismatch in task distribution and protocol. The recovered capability is also practically useful in-domain. On ProofNet, pass@32 improves from 21.51% to 25.81%. Together, these results show that heavy domain supervised fine-tuning can suppress general tool-use ability without permanently erasing it, and that a small amount of domain-specific agentic data can awaken dormant tool-use capabilities.