mlsanityData to 7 Oct 2026

Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover

arXiv 2604.08388 ↗First posted 9 Apr 2026cs.AIcited by 0

On the map: LLM agents and tool use → Educational agents and math problem solving

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. Builds on 21 of its 28 references that are in the map. First posted on arXiv 9 Apr 2026.

Builds on

21 of 28 references.

Closest ancestors · 1

Same direction, newest first

  1. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics20 Jan

Other references · 20

  1. 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,355
  2. 2016Overcoming catastrophic forgetting in neural networkscited by 4,718
  3. 2024LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Modelscited by 1,442
  4. 2023An Empirical Study of Catastrophic Forgetting in Large Language Models During Continual Fine-tuningcited by 622
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2024Model Merging in LLMs, MLLMs, and Beyond: Methods, Theories, Applications and Opportunitiescited by 247
  7. 2024Continual Learning of Large Language Models: A Comprehensive Surveycited by 228
  8. 2025AIMO-2 Winning Solution: Building State-of-the-Art Mathematical Reasoning Models with OpenMathReasoning datasetcited by 165
  9. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  10. 2023Understanding Catastrophic Forgetting in Language Models via Implicit Inferencecited by 138
  11. 2024Mitigating Catastrophic Forgetting in Large Language Models with Self-Synthesized Rehearsalcited by 114
  12. 2024Revisiting Catastrophic Forgetting in Large Language Model Tuningcited by 93
8 more
  1. 2023TRACE: A Comprehensive Benchmark for Continual Learning in Large Language Modelscited by 59
  2. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  3. 2025Spurious Forgetting in Continual Learning of Language Modelscited by 47
  4. 2024Scaling Laws for Forgetting When Fine-Tuning Large Language Modelscited by 36
  5. 2024Mitigating Catastrophic Forgetting in Language Transfer via Model Mergingcited by 36
  6. 2025Scaling Laws for Forgetting during Finetuning with Pretraining Data Injectioncited by 35
  7. 2024A Semantic Search Engine for Mathlib4cited by 30
  8. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
  2. 2026Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
  3. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
  4. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?
  5. 2026Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
  6. 2026When Tools Fail: Benchmarking Dynamic Replanning and Anomaly Recovery in LLM Agents
  7. 2026DIVE: Scaling Diversity in Agentic Task Synthesis for Generalizable Tool Use
  8. 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement