[논문 리뷰] LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

TL;DR

LeanMarathon은 연구 수준의 복잡한 수학 논문을 기계가 검증할 수 있는 형식 언어(Lean)로 자동 변환하는 혁신적인 다중 에이전트 시스템입니다. 이 시스템은 거대한 형식화 작업을 여러 개의 작고 독립적인 작업으로 분해하고, '진화하는 청사진(Evolving Blueprint)'을 통해 전체 과정을 체계적으로 관리합니다. 여러 AI 에이전트가 병렬적으로 협력하여 증명을 생성하고 검증함으로써, 기존 단일 LLM 접근법의 한계였던 안정성과 확장성 문제를 해결합니다. LeanMarathon은 두 편의 최신 수학 논문을 성공적으로 형식화하며, AI가 인간 수학자와 협력하는 'AI 공동 수학자'의 가능성을 제시합니다.

연구 배경 및 동기

수학의 자동 형식화(autoformalization)는 자연어로 작성된 수학적 내용을 컴퓨터가 이해하고 검증할 수 있는 형식 언어로 변환하는 과정입니다. 이는 AI 분야의 오랜 난제 중 하나로, 단순히 개별 정리를 증명하는 것을 넘어, 수백 개의 상호 연결된 개념으로 이루어진 논문 전체를 다루어야 합니다.

기존의 자동 증명 시스템들은 주로 단일 정리 증명에 초점을 맞추었으며, 논문 전체를 형식화하는 데에는 다음과 같은 근본적인 한계에 부딪혔습니다.

1. 규모와 복잡성 (Scale & Complexity): 논문은 수백 개의 정의, 보조정리, 정리가 복잡한 의존성 네트워크를 형성하고 있어, 전체 구조를 일관성 있게 관리하기 어렵습니다.
2. 의존성 지옥 (Dependency Hell): 초반의 작은 정의나 보조정리를 수정하면, 이를 의존하는 수십 개의 다른 증명에 연쇄적으로 영향을 미쳐 전체 프로젝트가 불안정해질 수 있습니다.
3. 문맥 손실 (Context Loss): LLM(거대 언어 모델)은 긴 증명 과정에서 초기 가정이나 전체 목표와 같은 중요한 문맥을 잊어버려 잘못된 방향으로 증명을 진행하기 쉽습니다.
4. 오류 전파 (Error Propagation): 초기에 발생한 사소한 형식화 오류가 나중에 발견되면, 그 위에 쌓아 올린 모든 작업을 무너뜨리는 심각한 재작업을 유발할 수 있습니다.

LeanMarathon은 이러한 문제들을 '분할 정복(Divide and Conquer)' 철학에 기반한 다중 에이전트 시스템으로 해결하고자 제안되었습니다.

관련 연구

수학의 형식화 및 자동 증명 분야는 오랜 역사를 가지고 있습니다.

• 상호작용 증명 보조기 (Interactive Theorem Provers): Lean, Coq, Isabelle, HOL Light 등은 인간 전문가가 증명 과정을 단계별로 안내하면 시스템이 각 단계의 유효성을 검증해주는 강력한 도구입니다. 하지만 완전 자동화와는 거리가 멉니다. LeanMarathon은 이러한 시스템 중 하나인 Lean을 기반으로 자동화를 구현합니다.
• 자동 증명 시스템 (Automated Theorem Provers): Mizar, Aristotle 등은 특정 논리 체계 내에서 정리를 자동으로 증명하려 시도했지만, 연구 수준의 복잡하고 긴 논문 전체를 다루는 데에는 확장성 한계가 있었습니다.
• LLM 기반 접근법: 최근 LLM을 활용하여 코드를 생성하듯 Lean 코드를 생성하는 연구들이 있었지만, 주로 단일 정리 증명에 머물렀고 위에서 언급한 '문맥 손실'과 '오류 전파' 문제로 인해 긴 형식화 작업에는 불안정한 모습을 보였습니다.

LeanMarathon은 상호작용 증명 보조기의 엄밀함과 LLM의 유연성을 결합하고, 다중 에이전트 아키텍처를 통해 기존 접근법들의 확장성 한계를 극복하고자 합니다.

핵심 기여

1. 다중 에이전트 프레임워크: 복잡한 수학 논문 형식화를 위해 각기 다른 역할을 수행하는 AI 에이전트(청사진 작성자, 목표 검토자, 작업자, 정제자)가 협력하는 새로운 프레임워크를 제시했습니다.
2. 진화하는 청사진 (Evolving Blueprint): 형식적 증명 골격, 자연어 증명 그래프, 작업 기록을 통합한 '살아있는 문서'를 도입하여, 전체 증명 과정을 체계적으로 관리하고 문맥 손실을 방지합니다.
3. 병렬 처리 및 안정성: 증명 의존성을 **증명 지향 비순환 그래프(Proof DAG)**로 모델링하여, 독립적인 보조정리들을 병렬로 증명하고, 특정 증명의 실패가 전체 시스템에 미치는 영향을 최소화(국지화)했습니다.
4. 점진적 개발 (Incremental Development): 이미 검증된 형식화 라이브러리에 새로운 목표를 추가하여 증명을 확장할 수 있는 방법론을 제시하여, 대규모 수학 프로젝트의 점진적이고 안정적인 개발을 가능하게 합니다.
5. 실험적 검증: 두 편의 최신 연구 수준 수학 논문(조합론 분야)을 세계 최초로 완전히 자동 형식화하는 데 성공하여 제안된 시스템의 실효성을 입증했습니다.

제안 방법론

LeanMarathon은 '진화하는 청사진'을 중심으로 네 종류의 AI 에이전트가 협력하여 논문을 형식화합니다.

1. 진화하는 청사진 (Evolving Blueprint)

청사진은 단순한 계획이 아니라, 형식화 프로젝트의 모든 상태를 담고 있는 살아있는 문서입니다. 세 가지 주요 구성 요소를 가집니다.

• 형식적 증명 골격 (Formal Proof Skeleton): 논문의 모든 정의, 보조정리, 정리를 Lean 코드로 표현한 골격입니다. 초기에는 증명 부분이 sorry로 채워져 있습니다.
• 자연어 증명 그래프 (Natural Language Proof Graph): 원본 논문의 LaTeX 소스를 파싱하여 각 정리와 그 증명, 그리고 그들 간의 의존 관계를 그래프 형태로 구조화한 것입니다.
• 작업 기록 시스템 (Task Log System): 각 sorry를 해결하기 위한 작업의 상태(진행 중, 성공, 실패)와 에이전트의 활동 기록을 추적합니다.

이 청사진 덕분에 모든 에이전트는 프로젝트의 전체적인 맥락과 각자의 작업 목표를 명확히 인지할 수 있습니다.

2. 다중 에이전트 아키텍처

LeanMarathon은 네 종류의 전문화된 에이전트로 구성됩니다.

1. 청사진 작성자 (Blueprint Writer): 논문 전체를 읽고 초기 '진화하는 청사진'을 생성합니다. 즉, 논문의 구조를 파악하여 Lean 코드의 골격과 sorry로 채워진 초기 증명 파일을 만듭니다.
2. 목표 검토자 (Goal Reviewer): 청사진에 작성된 형식적 명제(Lean 코드)가 원본 논문(LaTeX)의 수학적 의도와 정확히 일치하는지 검토하고 미묘한 의미 차이를 수정합니다.
3. 작업자 (Worker): 청사진에 명시된 sorry를 채우는 핵심 역할을 합니다. 의존성이 없는 sorry부터 시작하여 증명을 시도합니다. 예를 들어, 다음과 같은 sorry를 실제 Lean 증명 코드로 대체합니다.

   theorem example_theorem (n : ℕ) (h : n > 0) : n + 1 > 1 := by
     sorry -- 작업자 에이전트가 이 부분을 증명 코드로 채웁니다.
   

4. 정제자 (Refiner): 작업자가 생성한 증명에서 발생한 오류를 수정하거나, 더 효율적이고 가독성 높은 증명으로 코드를 개선합니다. 원본 논문을 참조하여 작업자의 실수를 바로잡는 중요한 역할을 합니다.

3. 증명 지향 비순환 그래프 (Proof DAG)

LeanMarathon은 논문의 논리적 구조를 DAG로 관리합니다.

• $V$ (정점, Vertices): 논문의 각 정의, 보조정리, 정리를 나타내는 노드. 각 노드는 (Lean 타입, LaTeX 명제, LaTeX 증명) 튜플로 구성됩니다.
• $E$ (간선, Edges): 증명 간의 의존 관계. 예를 들어, 보조정리 B가 정리 A의 증명에 사용된다면, B에서 A로 향하는 간선 $(B, A)$가 존재합니다.

이 DAG 구조 덕분에, 들어오는 간선(incoming edge)이 없는 노드들, 즉 다른 증명에 의존하지 않는 보조정리들은 병렬적으로 작업자 에이전트에게 할당될 수 있습니다. 이는 전체 형식화 과정의 효율을 극대화합니다.

      [Lemma 1]----->[Lemma 3]----
     /                            \
[Start]---->[Lemma 2]-------------->[Theorem 1]
     \                            /
      ----->[Definition 1]-------

위 예시에서 Lemma 1, Lemma 2, Definition 1은 병렬로 처리될 수 있습니다.

실험 설정

• 대상 논문: 조합론 분야의 두 편의 최신 연구 논문 (D. H. J. Polymath, 2021; J. D. Lichtman, 2023)을 형식화하는 것을 목표로 삼았습니다. 이 논문들은 유명한 에르되시 문제(Erdős problems)와 관련이 있습니다.
• 목표 정리: 두 논문의 핵심 정리 총 7개.
• 평가 지표:
  • 형식화 성공률: 목표 정리를 sorry 없이 완전히 증명했는가?
  • 증명 수: 형식화 과정에서 생성된 보조정리와 정리의 총 개수.
• 베이스라인: 다중 에이전트 시스템의 효과를 검증하기 위해, 단일 LLM이 전체 형식화 과정을 순차적으로 처리하는 모놀리식(monolithic) 접근법과 성능을 비교했습니다.
• 주요 설정:
  • 에이전트 모델: gpt-4-turbo-2024-04-09
  • 실행 환경: 모든 코드 변경 사항은 Lean 컴파일러를 통과해야 하는 CI(지속적 통합) 게이트에서 검증되어 증명의 무결성을 보장합니다.

실험 결과 분석

LeanMarathon은 목표로 한 7개의 핵심 정리를 모두 성공적으로 형식화했으며, 이 과정에서 총 258개의 보조정리와 정리를 증명했습니다.

주요 결과

이는 LLM 기반 시스템이 연구 수준의 논문 전체를 처음부터 끝까지 자동 형식화한 최초의 사례입니다. 모놀리식 접근법은 긴 문맥을 처리하지 못하고 중간에 사소한 오류가 발생했을 때 회복하지 못해 실패한 반면, LeanMarathon은 안정적으로 작업을 완료했습니다.

Ablation Study 분석

시스템의 핵심 설계 요소들의 중요성을 검증하기 위해 몇 가지 기능을 비활성화한 실험을 진행했습니다.

• 정제자(Refiner)의 논문 참조 제한: 정제자가 원본 논문을 참조하지 못하게 하자, 형식적 오류는 수정할 수 있었지만 원본의 수학적 의도와 다른 방향으로 증명을 수정하는 경우가 발생했습니다.
• 작업자(Worker)의 비효율적 중단 규칙: 작업자가 실패한 증명을 너무 오래 시도하게 두자, 전체 시스템의 처리량이 급격히 감소했습니다.

이러한 결과는 각 에이전트의 전문화된 역할과 유기적인 협력 구조가 시스템 성공의 필수 요소임을 명확히 보여줍니다.

비판적 평가

강점

1. 확장성과 안정성: 분할 정복과 병렬 처리 덕분에 논문의 규모가 커져도 안정적으로 형식화를 수행할 수 있습니다.
2. 오류 회복 능력: 특정 증명의 실패가 다른 병렬 작업에 영향을 주지 않으며, 정제자 에이전트를 통해 오류를 효과적으로 수정할 수 있습니다.
3. 투명성과 재현성: 모든 작업 과정이 Git으로 관리되고 청사진에 기록되므로, 특정 시점의 작업을 투명하게 추적하고 동일하게 재현할 수 있습니다.

한계점

1. 기존 라이브러리 의존성: Lean의 표준 라이브러리인 Mathlib에 관련 이론이 부족한 분야의 논문을 형식화하는 데에는 여전히 큰 어려움이 따릅니다.
2. 높은 계산 비용: 다수의 에이전트가 수많은 LLM API 호출을 생성하므로 상당한 계산 자원과 비용이 소요될 수 있습니다.
3. 초기 청사진의 품질: 초기 청사진의 품질이 전체 프로젝트의 성패에 큰 영향을 미치므로, 청사진 작성자 에이전트의 성능이 매우 중요합니다.

향후 연구 방향

1. 다양한 수학 분야로의 확장: 현재 성공한 조합론을 넘어 대수학, 해석학, 기하학 등 더 추상적이고 복잡한 수학 분야에 적용하는 연구가 필요합니다.
2. 에이전트 능력 고도화: LLM뿐만 아니라, 형식적 추론 엔진이나 기호 계산기 등 다른 도구를 활용하여 에이전트(특히 작업자)의 증명 능력을 향상시킬 수 있습니다.
3. 인간-AI 협력 모델: 완전 자동화를 넘어, 인간 수학자가 특정 어려운 부분을 지도하거나 에이전트에게 힌트를 주는 방식의 협력 모델을 구축하여 실용성을 높일 수 있습니다.

실무 적용 가이드

LeanMarathon의 아이디어를 복잡한 소프트웨어 개발이나 시스템 설계 프로젝트에 적용할 수 있습니다.

1. '진화하는 청사진' 도입: 프로젝트의 전체 아키텍처, 모듈 간 의존성, 작업 현황을 중앙에서 관리하는 '살아있는 문서'를 구축하여 팀 전체가 공유된 문맥을 갖도록 합니다.
2. 역할 기반 에이전트(팀) 구성: 코드 초안을 작성하는 '작성자', 요구사항과 구현의 일치 여부를 검토하는 '검토자', 실제 기능을 구현하는 '작업자', 코드를 리팩토링하고 버그를 수정하는 '정제자'로 역할을 명확히 분담하여 효율을 높입니다.
3. CI/CD를 통한 무결성 보장: 모든 변경 사항은 자동화된 테스트와 빌드를 통과해야만 병합되도록 하여 시스템의 안정성과 무결성을 유지합니다.

결론

LeanMarathon은 강력한 단일 AI 모델만으로는 해결할 수 없었던 '긴 호흡의 추론' 문제를 다중 에이전트 시스템이라는 새로운 아키텍처로 해결했습니다. 이 연구는 복잡한 의존성을 관리하고, 오류로부터 회복하며, 일관성을 유지하는 능력이야말로 진정한 'AI 공동 수학자'로 나아가기 위한 핵심임을 보여줍니다. LeanMarathon은 수학의 엄밀성을 높이는 데 기여할 뿐만 아니라, AI가 복잡하고 창의적인 지적 작업을 수행하는 방식에 대한 새로운 패러다임을 제시합니다.

참고 자료

• LeanMarathon 논문 (arXiv:2406.05400)
• LeanMarathon 코드 저장소
• The Lean Prover