자동 정리 증명, 복잡한 워크플로우보다 단순 반복 루프가 더 효과적

핵심 요약

• 형식 정리 증명(formal theorem proving) 분야는 계획, 분해, 전문 도구 연계 등 인간이 설계한 복잡한 워크플로우에 의존해왔으나, 비형식 수학은 대규모 언어 모델의 연쇄 추론으로 진전을 이뤄왔다.
• 이 논문은 '비터 레슨' 질문을 제기한다: 테스트 타임 계산을 확장하는 단순한 에이전트 루프가 이런 복잡한 워크플로우와 경쟁할 수 있는가?
• h1이라는 단순한 도구를 개발했는데, 이는 모델에게 Lean 4의 효율적인 인터페이스를 제공하고 검증자 피드백과 자기 성찰로 작동하며, 명시적 분해나 탐색 구조를 강요하지 않는다.
• h1은 PutnamBench, FATE-X, FormalConjectures100-Solved에서 최고 성능을 기록했고, FormalConjectures의 8개 미해결 문제를 풀었으며, 동등한 모델과 비교하면 Goedel-Architect와 AlphaProof Nexus 같은 전문화된 워크플로우와 동등하거나 능가했다.
• 놀랍게도 단일 시도(pass@1)만으로도 미해결 문제를 풀 수 있음을 보였다.
• 절제 실험과 Claude Code, AxProverBase와의 동등 모델 비교를 통해, 단순성만으로는 부족하며 효율적인 Lean 인터페이스가 비용과 해결률을 크게 좌우함을 확인했다.
• 향후 연구는 워크플로우를 처방하기 전에 먼저 효율적인 실행 피드백으로 최고 성능 모델을 평가할 것을 권장한다.