A Minimal Agent for Automated Theorem Proving

이 논문은 반복적 증명 정제, 라이브러리 검색, 컨텍스트 관리 등 최첨단 시스템의 핵심 기능을 간소화하여 구현한 최소한의 자동 증명 에이전트를 제안하고, 다양한 벤치마크에서 복잡한 아키텍처와 경쟁력 있는 성능을 보이면서도 샘플 효율성과 비용 효율성 면에서 단일 생성 방식보다 우월함을 입증했습니다.

핵심

이 논문은 **"수학 문제를 해결하는 AI 에게 '단순하지만 똑똑한' 비법을 가르친 연구"**라고 할 수 있습니다.

기존의 복잡한 수학 증명 AI 들은 거대한 공장처럼 많은 자원을 소모하고 복잡한 기계 장치로 작동했습니다. 하지만 이 연구팀은 **"작은 공방처럼 간단하지만, 실수하면 다시 시도하고 메모장을 잘 활용하는 방식"**이 훨씬 더 효율적이고 강력하다는 것을 증명했습니다.

이 내용을 일상적인 비유로 설명해 드릴게요.

---

1. 핵심 아이디어: "거대한 공장 vs. 똑똑한 장인"

• 기존 방식 (거대한 공장):
  이전의 AI 수학자들은 문제를 풀 때, 수천 번의 시도를 하거나 거대한 데이터베이스를 뒤적이며 복잡한 알고리즘을 돌렸습니다. 마치 거대한 공장에서 컨베이어 벨트를 돌려 무작위로 부품을 조립하다가 우연히 맞는 것을 찾는 것과 비슷했습니다. 비용도 많이 들고, 새로운 수학 언어 (Lean) 가 업데이트되면 공장을 다시 지어야 하는 번거로움이 있었습니다.

• 이 연구의 방식 (똑똑한 장인 - AxProverBase):
  연구팀은 **"단순한 도구 세 개"**만 갖춘 작은 공방을 만들었습니다.

  1. 시도하고 피드백 받기 (Iterative Refinement): 한 번에 완벽하게 맞추려 하지 않습니다. "이건 안 맞네?"라는 오류 메시지를 보고 수정합니다.
  2. 메모장 (Memory): 같은 실수를 반복하지 않기 위해 "어제 실수했던 부분"을 메모장에 적어두고 다음에 참고합니다.
  3. 참고서 찾기 (Tools): 모르는 개념이 나오면 도서관 (Mathlib) 이나 인터넷을 검색해서 답을 찾아옵니다.

이 세 가지만으로도 거대한 공장보다 훨씬 더 빠르고 정확하게 문제를 해결할 수 있다는 것이 이 논문의 핵심입니다.

2. 구체적인 작동 원리: "수학 시험을 보는 학생"

이 AI 에이전트가 문제를 풀 때의 과정을 한 학생의 시험 공부에 비유해 볼까요?

1. 문제 제시 (Proposer):
   학생 (AI) 이 수학 문제를 받습니다. 처음엔 막연하게 "아마 이 공식으로 풀 수 있겠지?"라고 추측해서 답안을 작성합니다.

2. 채점과 피드백 (Compiler & Reviewer):
   선생님이 답안을 채점합니다.

   • "여기 계산 실수했어 (컴파일 오류)"
   • "이 단계는 생략했네 (sorry)"
   • "문제를 바꿨잖아? 원래 문제대로 다시 해."
     이 피드백을 학생은 그대로 받습니다.

3. 메모장 활용 (Memory):
   여기서 중요한 건 메모장입니다.

   • 이전 방식: 매번 처음부터 다시 시작해서 같은 실수를 반복했습니다.
   • 이 연구의 방식: 학생은 "어제 '링 (Ring)' 이론에서 비가환적일 때 'ring' 명령어를 쓰면 안 된다는 걸 배웠어"라고 메모장에 적어둡니다. 다음 문제를 풀 때 이 메모를 보고 "아, 이번엔 수동으로 식을 풀어야지!"라고 바로 수정합니다.
   • 결과: 같은 실수를 반복하지 않아서 훨씬 빨리 정답에 도달합니다.

4. 참고서 검색 (Tools):
   막히는 부분이 생기면 학생은 "Mathlib 이라는 도서관"이나 "Tavily 라는 인터넷 검색"을 통해 필요한 공식을 찾아옵니다. 하지만 연구 결과에 따르면, 메모장을 잘 쓰는 것이 도서관을 찾는 것보다 훨씬 더 큰 효과를 보였습니다.

3. 놀라운 결과: "작은 비용으로 거대한 성과"

연구팀은 이 간단한 방식을 다양한 수학 대회 문제 (Putnam, FATE 등) 로 테스트했습니다.

• 성공률: 복잡한 거대 AI 들과 비교해도 뒤지지 않는, 오히려 더 좋은 성적을 냈습니다.
• 비용: 거대 AI 들은 문제를 하나 풀기 위해 수백만 원의 계산 비용이 들지만, 이 간단한 방식은 그 10 분의 1, 100 분의 1 비용으로 해결했습니다.
• 유연성: 수학 언어 (Lean) 가 업데이트되어도, 복잡한 공장을 고칠 필요 없이 이 간단한 '학생'에게 새로운 규칙만 알려주면 바로 적응합니다.

4. 결론: "왜 이것이 중요한가?"

이 논문은 **"AI 가 똑똑해지려면 무조건 크고 복잡해져야 하는 것은 아니다"**라고 말합니다.

• 핵심 메시지: AI 가 문제를 해결할 때, 거대한 뇌 (모델) 만 믿는 것이 아니라 **잘못된 것을 고치는 과정 (반복)**과 **과거의 교훈을 기억하는 것 (메모)**이 훨씬 중요합니다.
• 일상적인 비유:
  • 과거: "나는 천재야, 한 번에 다 맞춰!"라고 외치다가 실패하는 사람.
  • 이 연구: "아, 이번엔 틀렸네. 왜 틀렸지? 메모장에 적어두고 다음엔 고쳐보자."라고 차분하게 접근하는 사람.

이 연구는 앞으로 AI 가 과학적 발견이나 복잡한 논리 문제를 해결할 때, 복잡한 시스템보다는 '학습하고 성장하는 과정'에 집중하는 것이 더 효율적임을 보여주었습니다. 이제 누구나 이 간단한 '공방'을 가져와서 자신의 프로젝트에 적용할 수 있게 되었습니다.

기술 요약

1. 문제 정의 (Problem)

자동화된 정리 증명 (Automated Theorem Proving, ATP) 은 인공지능의 검증 가능한 과학적 추론을 위한 핵심 분야입니다. 특히 Lean 4 와 같은 상호작용형 정리 증명기 (Interactive Theorem Prover) 는 수학 및 공학 분야의 논리적 일관성을 보장하는 데 필수적입니다. 그러나 현재 존재하는 최첨단 (State-of-the-Art, SOTA) ATP 시스템들은 다음과 같은 심각한 한계를 가지고 있습니다.

• 복잡성과 유지보수 비용: 대부분의 SOTA 시스템은 강화 학습 (RL), 대규모 합성 데이터 파인튜닝, 복잡한 재귀적 분해 구조 등 여러 복잡한 구성 요소를 결합하고 있습니다. 이는 Lean 및 Mathlib(Lean 의 수학 라이브러리) 의 빠른 버전 업데이트에 따라 시스템 유지보수가 어렵게 만듭니다.
• 비효율적인 비용: 대규모 인프라 구축과 고비용의 상용 모델 의존성으로 인해 실제 연구나 프로젝트에 적용하기 어렵습니다.
• 성능 향상의 원인 불명확: 최신 LLM 의 성능 향상과 아키텍처 혁신 중 어느 것이 실제 성능 향상을 주도하는지 구분하기 어렵습니다.

따라서, 간단하면서도 확장 가능하고, 비용 효율적이며, 다양한 LLM 의 능력을 활용할 수 있는 최소한의 에이전트 아키텍처가 필요합니다.

2. 방법론 (Methodology)

저자들은 AxProverBase라는 이름의 최소 에이전트 아키텍처를 제안합니다. 이 설계는 Figure 1 에 명시된 대로 세 가지 핵심 모듈로 구성되며, 복잡한 시스템 없이도 SOTA 수준의 성능을 달성할 수 있도록 설계되었습니다.

핵심 구성 요소

1. 제안자 에이전트 (Proposer Agent):

   • 주어진 정리 (Theorem) 를 증명하기 위해 Lean 코드를 작성합니다.
   • ReAct 스타일의 에이전트로 구현되며, 필요 시 도구 (Tool) 를 호출할 수 있습니다.
   • 도구: Mathlib 내의 정리 및 전술 (tactic) 을 검색하는 LeanSearch 와 증명 전략을 찾기 위한 웹 검색 (Tavily) 을 지원합니다.

2. 검증 시스템 (Review System):

   • 컴파일러: 제안된 코드를 컴파일하여 문법 오류나 증명 실패를 감지합니다.
   • 검토자 에이전트 (Reviewer Agent): 코드가 컴파일되더라도 sorry(미해결 목표) 가 포함되지 않았는지, 그리고 정리의 진술이 변경되지 않았는지 확인합니다. 이는 허위 성공을 방지하는 안전 장치 역할을 합니다.

3. 메모리 시스템 (Memory System):

   • 이전 시도에서 실패한 이유와 얻은 교훈을 저장하여 에이전트가 같은 실수를 반복하지 않도록 합니다.
   • 구현 방식 비교:
     • 메모리 없음: 이전 맥락 없이 단일 시도.
     • 이력 (History): 최근 $n$개의 시도 기록을 모두 전달.
     • 자가 관리 컨텍스트 (Self-managed Context): 에이전트가 이전 시도와 피드백을 분석하여 핵심 교훈 (Key Lessons) 만 추려내어 '실험 노트' 형태로 관리합니다. 이는 컨텍스트 길이 제한을 피하고 비용 효율성을 높입니다.

작동 프로세스

1. 제안자가 정리를 증명하려는 시도를 합니다 (도구 사용 가능).
2. 컴파일러가 코드를 검증합니다. 실패 시 오류 메시지, 성공 시 sorry 여부 확인을 위해 검토자에게 전달됩니다.
3. 검토자가 최종 확인을 거칩니다.
4. 실패 시, 피드백과 메모리 시스템의 교훈이 제안자에게 전달되어 다음 반복 (Iteration) 에서 개선된 증명을 시도합니다.

3. 주요 기여 (Key Contributions)

• 최소화된 아키텍처의 유효성 입증: 복잡한 RL 기반 파인튜닝이나 거대한 합성 데이터셋 없이도, **반복적 증명 정제 (Iterative Proof Refinement)**와 메모리 메커니즘만으로도 최첨단 시스템과 경쟁할 수 있는 성능을 달성함을 보였습니다.
• 성공 요인의 체계적 분석 (Ablation Study):
  • 반복적 정제 (Iterative Refinement): 성능 향상에 가장 큰 영향을 미치는 요소입니다. 단일 시도 (Single-shot) 보다 훨씬 효율적입니다.
  • 메모리 메커니즘: 에이전트가 같은 실수를 반복하는 '순환 (Cycles)'을 방지하여 두 번째로 큰 성능 향상을 가져옵니다. 특히 '자가 관리 컨텍스트'가 이력 (History) 방식보다 비용과 성능 면에서 우수했습니다.
  • 검색 도구 (Tools): Mathlib 검색은 도움이 되지만, 반복 정제나 메모리에 비해 영향력은 상대적으로 작았습니다.
• LLM 능력의 극대화: 복잡한 아키텍처가 아닌, 단순한 에이전트 프레임워크가 강력한 LLM(예: Claude Opus 4.5) 의 능력을 최대한 끌어올리는 '스캐폴딩 (Scaffolding)' 역할을 할 수 있음을 보였습니다.
• 오픈소스 및 재현성: 전체 구현 코드와 평가 인프라를 오픈소스로 공개하여, 향후 연구의 기준점 (Baseline) 으로 활용되도록 했습니다.

4. 실험 결과 (Results)

저자들은 PutnamBench, FATE, LeanCat 등 다양한 벤치마크에서 AxProverBase 를 평가했습니다.

• 성능 비교:
  • PutnamBench: AxProverBase (Claude Opus 4.5 사용) 는 단일 시도 (pass@1) 에서 **54.7%**의 성공률을 기록했습니다. 이는 복잡한 시스템인 Hilbert Prover(pass@1840 기준 70%) 에 비해 적은 리소스로 달성한 수치이며, 단순 반복 시도만으로는 도달하기 어려운 수준입니다.
  • FATE (수준 높은 대수학): FATE-M 에서 98.0%, FATE-H 에서 **66.0%**의 성공률을 기록하여, 기존 오픈소스 모델들이 거의 해결하지 못했던 난이도 높은 문제에서도 우수한 성능을 보였습니다.
  • LeanCat (범주론): **59.0%**의 성공률을 기록했습니다.
• 비용 효율성:
  • 샘플당 평균 비용은 $12.6으로, 기존 시스템에 비해 훨씬 저렴합니다.
  • 실행 시간은 Hilbert Prover 대비 10 배 이상 빠릅니다.
• 모델 비교:
  • Claude Opus 4.5 와 Sonnet 4.5 가 Gemini 모델보다 훨씬 우수한 성능을 보였으며, 특히 '생각 예산 (Thinking Budget)'을 늘렸을 때 성능이 크게 향상되었습니다.

5. 의의 및 결론 (Significance)

이 논문은 자동화된 정리 증명 분야에서 다음과 같은 중요한 시사점을 제공합니다:

1. 복잡함의 탈피: 고도의 강화 학습이나 대규모 파인튜닝 없이도, **간단한 에이전트 루프 (Iterative Loop)**와 피드백 메커니즘만으로도 정밀한 수학적 추론이 가능함을 증명했습니다.
2. 진화 가능한 기준점: AxProverBase 는 LLM 기술이 발전함에 따라 자동으로 성능이 향상되는 '진화형 기준점' 역할을 합니다. 새로운 LLM 이 등장하면 아키텍처를 재학습할 필요 없이 바로 적용 가능합니다.
3. 실용성: 비용 효율성과 사용 편의성이 뛰어나므로, 실제 연구 프로젝트나 산업 현장에서 Lean 기반의 형식적 증명을 수행하는 데 널리 채택될 수 있는 접근법입니다.
4. 연구 방향 제시: 정리 증명의 핵심은 모델의 크기나 복잡도가 아니라, 어떻게 피드백을 활용하고 메모리를 관리하여 반복적으로 학습하느냐에 있음을 보여주었습니다.

결론적으로, AxProverBase 는 복잡한 시스템을 대체할 수 있는 간결하고 강력한 대안을 제시하며, AI 기반 수학 증명 연구의 새로운 패러다임을 제시합니다.