A Minimal Agent for Automated Theorem Proving

Motivation

• Known: Lean과 Mathlib을 기반으로 한 automated theorem proving 분야에서 tree-search 방식(AlphaProof, REAL-Prover, Aristotle)과 whole-proof generation 방식(DeepSeek-Prover-V2, Goedel-Prover-V2, Hilbert, Seed Prover V1.5)이 각각 발전해왔으며, iterative refinement, compiler feedback, library search, lemma decomposition 등의 복잡한 구성 요소를 결합한 시스템들이 PutnamBench, MiniF2F 등에서 state-of-the-art 성능을 달성하고 있다.
• Gap: 기존 최고 성능 시스템들은 매우 복잡한 구조를 가지고 있어 대규모 인프라 구축이 필요하거나 proprietary model 사용으로 인해 비용이 높으며, LLM 자체의 빠른 성능 향상 때문에 성능 개선이 아키텍처 혁신 덕분인지 아니면 더 강력한 base model 덕분인지 구분하기 어렵다는 근본적 문제가 있다.
• Why: 아키텍처 요소와 base LLM의 기여도를 분리해서 이해하는 것은 향후 prover 설계 개선 방향을 정하는 데 필수적이며, 단순하고 저비용이며 접근 가능한 baseline은 학계와 실무 커뮤니티가 formal method를 실제로 채택하는 데 있어 진입 장벽을 크게 낮출 수 있다.
• Approach: iterative proof refinement, memory 기반 context management, library/web search라는 세 가지 핵심 구성 요소만을 갖춘 모듈형 minimal agent(AxProverBase)를 bottom-up 방식으로 구축하고, 각 구성 요소를 하나씩 추가하며 ablation study를 수행해 성능 기여도를 분리 분석한다.

Achievement

Figure 2. Ablation study on different components of the min-

1. 경쟁력 있는 성능: 훨씬 단순한 아키텍처와 훨씬 낮은 비용으로 복잡한 state-of-the-art provers에 필적하는 성능을 달성했다.
2. iterative refinement의 압도적 중요성: proof를 반복적으로 개선하는 능력이 성능에 가장 큰 영향을 미치는 요소이며, 이 기능 하나만으로도 다수의 복잡한 state-of-the-art 접근법을 능가할 수 있음을 보였다.
3. memory의 두 번째 효과: memory 메커니즘이 오류 수를 크게 줄여 두 번째로 큰 성능 향상을 가져온다는 것을 확인했다.
4. tool 사용의 보조적 효과: Mathlib과 같은 Lean library를 검색하는 tool이 도움이 되지만 iterative refinement나 memory에 비해서는 영향이 상대적으로 작다는 것을 밝혔다.
5. 더 강력한 model의 이득 확인: 더 강력한 frontier language model일수록 적절한 scaffolding을 갖췄을 때 성능 향상 폭이 가장 크다는 것을 보였다.
6. 오픈소스 공개: 평가 인프라와 함께 구현을 오픈소스로 공개하여 향후 연구의 baseline이자 커뮤니티가 접근 가능한 prover로 활용될 수 있게 했다.

How

• proposer agent가 target theorem에 대해 Lean 코드를 작성하여 proof를 제안
• compiler가 제안된 proof의 유효성을 검증
• proof가 컴파일에 성공하면 reviewer agent가 이를 재검토하여 부정 사용(cheating)을 방지
• 컴파일 실패 또는 reviewer의 반대 시 feedback을 memory module로 전달하고, proposer가 추가된 context를 바탕으로 이전 proof를 개선하며 cycle을 반복(iterative proof refinement)
• proposer에게 library search나 web search 같은 tool에 대한 접근권을 부여하고 고정된 횟수만큼 호출 가능하게 함
• 여러 frontier language model과 다양한 design choice(단일 컴포넌트 추가 여부 등)를 비교하는 ablation study 및 qualitatively 다른 benchmark들에 대한 평가 수행
• single-shot 생성 다회 시도와 iterative approach를 비교하여 sample efficiency 및 cost effectiveness 측면에서의 차이 분석

Originality

• 최신 state-of-the-art theorem prover들이 공유하는 핵심 구성 요소(iterative refinement, memory, tool/search)만을 추출하여 최소한의 modular 아키텍처로 구현한 최초의 시도로서, 복잡한 시스템들 사이의 공정한 비교를 위한 baseline을 제공한다는 점에서 독창적이다.
• 성능 향상의 원인을 아키텍처 혁신과 base LLM의 발전 중 어디에 기인하는지 분리하여 분석하겠다는 문제의식 자체가 해당 분야에서 명확히 지적된 바 없는 새로운 관점이다.
• reviewer agent를 통한 이중 검증으로 cheating을 방지하는 설계를 minimal 아키텍처 내에 포함시킨 점이 실용적 독창성을 더한다.

Limitation & Further Study

• 발췌된 내용만으로는 구체적인 benchmark 성능 수치, 비용 비교의 정량적 근거, 그리고 reviewer agent의 정확도나 실패 사례에 대한 상세한 분석이 부족하다.
• Lean과 Mathlib의 빠른 버전 변화에 따른 장기적 유지보수성 문제는 언급되었으나 이에 대한 구체적 해결책은 제시되지 않았다.
• 향후 연구로는 tool의 다양화(정리 검색 외 다른 형식적 추론 tool), 더 복잡한 recursive decomposition과의 결합, 그리고 다양한 도메인(물리학, 제어이론, 양자 알고리즘 등)으로의 일반화 검증이 필요하다.
• 저자 전원이 해당 시스템을 개발한 회사 소속이라는 conflict of interest가 존재하여 독립적인 재현 검증이 중요하다.

Evaluation

총평: 복잡성 경쟁으로 치닫는 automated theorem proving 분야에서 핵심 요소만을 남긴 minimal baseline을 제안하고 이를 통해 성능 기여 요인을 명확히 분리해낸 실용적이고 시의적절한 연구로, 오픈소스 공개를 통한 커뮤니티 기여도도 높다.