唤醒沉睡的智能体：轻量化专用智能数据重新激活通用工具在哥德尔证明器中的使用

在目标领域进行大量监督微调会显著抑制基础模型中存在的能力。我们在形式数学领域进行此类研究，采用开源模型 Goedel-Prover-V2，其在 180 万个形式数学示例上进行了深度训练。经过领域专化后，该模型几乎完全丧失了生成有效工具调用的能力，即便明确指示使用工具，函数调用准确率从基础模型的 89.4% 降至接近 0%。我们提出疑问：这种智能体崩溃是永久性的，还是可逆的。为此，我们在少量 Lean 专用工具使用数据上进行微调。惊人之处在于，仅需 100 个智能体轨迹即可恢复强大的工具调用行为。值得注意的是，这种恢复并非源于奖励作弊或针对基准的优化：恢复数据完全来自 Lean 场景，模型使用自然语言查询来搜索 Mathlib 库以检索相关定理和引理，然而恢复出的能力在该领域之外也能良好迁移。具体而言，这 100 个 Lean 专用轨迹将在伯克利函数调用排行榜上的表现从接近零提升至 83.8%，虽然任务分布和协议不匹配，仍接近基础模型的 89.4%。恢复的能力在领域内也具有实际用途。ProofNet 上，pass@32 从 21.51% 提升至 25.81%。综上所述，这些结果表明，大规模领域监督微调可以抑制通用工具使用能力而非永久消除其作用，少量领域特定智能数据即可唤醒潜伏的工具使用能力。