唤醒沉睡的代理：特定于 Lean 的代理数据重新激活 Goedel Prover 中的通用工具使用能力

针对目标领域的重度监督微调可能抑制基座模型原有能力的问题，本文以 Goedel-Prover-V2 为例，发现其在形式化数学训练后几乎完全丧失工具调用能力。研究表明这种“代理崩溃”是可逆的：仅需少量特定于 Lean 的代理轨迹数据（如 100 条），即可显著恢复模型的通用工具调用性能，并在跨域基准测试中接近基座水平。这证明领域微调虽会暂时抑制通用技能，但并未永久抹除，少量特定数据即可唤醒休眠能力。