唤醒沉睡的智能体：Lean专用智能体数据重新激活Goedel Prover的通用工具使用

在目标领域上进行重度监督微调，可能强烈抑制基座模型原有的能力。我们在形式数学领域用Goedel-Prover-V2研究这一现象，后者是一个在180万个形式数学样例上重度训练的开源模型。经过领域专精化，该模型几乎完全丧失了产生有效工具调用的能力，即使被明确指示使用工具也是如此，函数调用准确率从基座模型的89.4%跌至接近0%。我们探究这种智能体能力崩溃究竟是永久性的还是可逆的。为回答这一问题，我们用少量Lean专用工具使用数据对专精模型进行微调。令人惊讶的是，少至100条智能体轨迹就足以恢复强大的工具调用行为。重要的是，这种恢复并非奖励劫持或针对基准优化的结果：恢复数据完全取自Lean场景——模型用自然语言查询在Mathlib库中搜索相关定理与引理——而重获的能力可迁移到远超该领域的范围。特别是，同样是这100条Lean专用轨迹，将Berkeley Function Calling Leaderboard上的性能从接近零提升至83.8%，尽管任务分布与协议不匹配，已逼近基座模型的89.4%。恢复的能力在领域内也具有实用价值：在ProofNet上，pass@32从21.51%提升至25.81%。综合来看，这些结果表明，重度领域监督微调会抑制而非永久抹除通用工具使用能力，少量领域专用智能体数据即可唤醒休眠的工具使用能力。