수면 중인 에이전트 깨우기: Lean 특정 에이전트 데이터가 Gödel 증명기에서 일반적인 도구 사용 능력을 재활성화합니다.

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

특정 도메인에 대한 집중적인 지도 학습은 기본 모델에 존재했던 능력을 크게 억제할 수 있습니다. 우리는 Gödel-Prover-V2라는 오픈 소스 모델을 사용하여 형식 수학 분야에서 이 현상을 연구했습니다. 이 모델은 180만 개의 형식 수학 예제로 집중적으로 학습되었습니다. 도메인 특화 후, 모델은 도구를 사용하라는 명시적인 지시가 내려져도 유효한 도구 호출을 생성하는 능력을 거의 완전히 잃어버리며, 기본 모델의 89.4% 함수 호출 정확도에서 거의 0%로 떨어집니다. 우리는 이러한 에이전트 기능의 붕괴가 영구적인 것인지, 아니면 되돌릴 수 있는 것인지 조사했습니다. 이 질문에 답하기 위해, 우리는 특화된 모델을 Lean에 특화된 소량의 도구 사용 데이터로 추가 학습시켰습니다. 놀랍게도, 단 100개의 에이전트 추적만으로도 강력한 도구 호출 기능을 회복하는 데 충분했습니다. 중요한 점은 이러한 회복이 보상 해킹이나 벤치마크 특화 최적화의 결과가 아니라는 것입니다. 회복에 사용된 데이터는 Mathlib 라이브러리에서 관련 정리 및 보조정리를 검색하기 위해 자연어 쿼리를 사용하는 Lean 환경에서 완전히 추출되었지만, 회복된 기능은 해당 도메인 너머에서도 잘 작동합니다. 특히, 동일한 100개의 Lean에 특화된 추적은 Berkeley 함수 호출 순위표에서 성능을 거의 0%에서 83.8%로 향상시켜, 작업 분포 및 프로토콜의 불일치에도 불구하고 기본 모델의 89.4%에 근접합니다. 회복된 기능은 실제 사용에서도 유용합니다. ProofNet에서 pass@32는 21.51%에서 25.81%로 향상되었습니다. 종합적으로, 이러한 결과는 집중적인 도메인 지도 학습이 일반적인 도구 사용 능력을 억제할 수 있지만 영구적으로 소멸시키는 것은 아니며, 소량의 도메인 특화된 에이전트 데이터가 잠재된 도구 사용 능력을 활성화할 수 있음을 보여줍니다.

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.