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.
Figures & tables
Figure 1: SLERP merge sweeps on two Lean theorem-proving benchmarks. Left axis (blue): evaluation performance on the Lean task (on MiniF2F and ProofNet ). Right axis (orange): problem-level tool-call compliance. Across both benchmarks, increasing the base-model weight consistently improves tool-calling behavior while degrading in-domain Lean performance. The overall tradeoff is very clear: as tool-use capability returns, evaluation accuracy on the Lean task drops substantially. This shows that naive merging does not jointly preserve strong theorem-proving ability and strong tool-calling behavior.
Figure 2: Cross-model trace distillation pipeline. (A) Qwen3-32B runs the full agentic loop (tool calls + Lean code) but produces low-quality code. (B) We keep Qwen3-32B ’s agentic prefix and have Goedel-Prover-V2-32B-SFT regenerate the final proof, then filter for compilation success and retrieval grounding. (C) Goedel-Prover-V2-32B-SFT alone generates strong Lean code but skips tool use entirely.
Table 1: ProofNet (186 problems) and MiniF2F (244 problems) results in a strictly post-hoc setting. Starting from already specialized checkpoints ( Goedel-Prover-V2-32B-SFT or Goedel-Prover-V2-32B-RL ), we continue supervised fine-tuning with Lean agentic data of size 100, 1K, or 18K, without rerunning the original specialization pipeline. We report standard pass@ k performance together with retrieval-grounding statistics. “Retr.” denotes the proportion of compiled proofs that used at least one theorem returned by LeanSearch .
Table 2: Analysis of retrieved theorem usage on ProofNet at pass@32 after agentic SFT on Goedel-Prover-V2-32B-SFT SFT checkpoint. A retrieved theorem is in-model if its identifier appears in the generative support of the base Goedel-Prover-V2-32B-SFT model, without any tool calling, and out-of-model otherwise. “Retr. & used” counts retrieved theorem occurrences referenced in compiled proofs. “Out-of-model” and “In-model” report the counts in each category, with unique theorem counts in parentheses. “Solved w/ out” is the number of pass@32-solved problems whose compiled proof contains at least one out-of-model retrieved theorem.
Table 3: BFCL v4 function-calling accuracy (%). “Simple” is the mean over simple function-calling tasks in Python, Java, and JavaScript. “Non-Live” and “Live” are means over their respective four functional categories, excluding irrelevance, and “Overall” averages these two. Panel A starts from the SFT checkpoint Goedel-Prover-V2-32B-SFT , while Panel B starts from the post-RL checkpoint Goedel-Prover-V2-32B-RL . All post-hoc agentic SFT models are trained only on Lean-specific LeanSearch traces (Section 3 ), with no exposure to general-purpose APIs or BFCL-style function schemas.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
Category
Qwen3-32B
Goedel-Prover-V2-32B-SFT
+100
+1k
+18k
+120k
Non-live
simple_python
95.75
10.75
93.50
92.00
91.00
83.75
simple_java
62.00
2.00
63.00
65.00
55.00
56.00
simple_javascript
74.00
0.00
68.00
68.00
62.00
58.00
multiple
96.00
9.00
92.50
94.00
88.50
87.00
parallel
93.00
3.50
86.50
85.50
82.50
75.50
Appendix
Table 4: Full BFCL v4 per-category results for 32B models (accuracy, %).
Category
Goedel-Prover-V2-32B-RL
+100
+1k
+18k
Non-live
simple_python
46.50
94.75
93.50
93.50
simple_java
29.00
65.00
62.00
57.00
simple_javascript
16.00
72.00
66.00
64.00
multiple
25.00
94.00
92.00
94.00
parallel
13.50
88.00
89.50
88.50
Appendix
Table 5: Full BFCL v4 per-category results for Goedel-Prover-V2-32B-RL (post-RL checkpoint) and reactivation variants (accuracy, %).