기술 요약: LeanMarathon

문제 정의

본 논문은 **연구 수준의 수학에 대한 장기적 자동 형식화(long-horizon autoformalization)**에서 발생하는 결정적인 병목 현상을 다룹니다. 대규모 언어 모델(LLM)은 자연어 증명을 생성하고 고립된 보조 정리(lemma)를 검증하는 데는 진전이 있었으나, 전체 연구 논문을 형식화하는 과업에는 실패해 왔습니다. 핵심적인 어려움은 단순히 하나의 어려운 보조 정리를 증명하는 것이 아니라, 수백 개의 상호 의존적인 선언들이 얽힌 수 시간, 혹은 수 일간의 과정 전반에 걸쳐 **에이전트 내구성(agent durability)**을 유지하는 데 있습니다.

현재의 단일 구조적(monolithic) 접근 방식은 세 가지 주요 실패 모드에 직に 직면합니다:

1. 일관성 상실(Coherence Loss): 이 작업은 전역적으로 결합되어 있습니다(스도쿠와 유사함). 전체 그래프를 설계, 증명, 수리하려는 단일 에이전트는 근시안적이 되어, 한 부분의 증명을 다른 부분을 패치하기 위해 "희생"시키는 경-향이 있습니다.
2. 자기 평가 편향(Self-Evaluation Bias): 자신의 출력을 스스로 평가하도록 요청받은 에이전트는 과잉 확신을 보여, 미묘한 형식화 드리프트(formalization drifts)를 감지하지 못합니다.
3. 가역 불가능성(Irreversibility): 일단 에이전트의 추론이 목표 정리로부터 벗어나면, 그 피해는 누적되며 시스템은 회복할 수 없습니다. 이는 로컬 수리가 먼 곳의 작업을 손상시키는 "컨텍스트 부패(context rot)"로 이어집니다.

기존 시스템들은 특히 연구 수준의 형식화가 교과서적 형식화와 달리 사전에 정교한 청사진을 갖추고 있지 않기 때문에, 목표 드리프트(goal drift)(논리적 경로에서의 이탈)와 중간에 갇힘(lost-in-the-middle)(비생산적인 하위 문제에 갇힘) 문제로 어려움을 겪습니다.

방법론: LeanMarathon

저자들은 장기적 자동 형식화를 가독성 있고, 회복 가능하며, 드리프트에 강하게 만들기 위한 다중 에이전트 하네스인 LeanMarathon을 제안합니다. 이 시스템은 네 가지 핵심 원칙을 기반으로 구축되었습니다:

1. 동적 증명 DAG를 통한 분해: 시스템은 초기 분해 상태를 고정하지 않습니다. 대신, 증명의 유향 비순환 그래프(DAG)를 진화시키며, 개별 에이전트가 처리하기 충분히 작아질 때까지 큰 노드를 분할하거나 잘못 형식화된 노드를 수리합니다.
2. 외부 또는 결정론적 검증: 어떤 에이전트도 자신의 출력을 판단하지 않습니다. 진행 상황은 오직 결정론적인 CI 검증기와 외부 에이전트에 의해서만 결정됩니다.
3. 제한된 도구 범위: 각 에이전트는 코드베이스의 경계가 정해진 영역만을 편집합니다. 이를 통해 실수가 발생하더라도 글로벌한 부패가 아닌 거부된 패치(rejected patch)로 끝나도록 보장합니다.
4. 형식화와 동시에 자연어화 수행: 각 노드는 Lean 타입과 그에 대응하는 LaTeX 산문 문장을 모두 유지합니다. 검증기는 자연어 의존성 그래프와 형식적 정교화(elaborator)의 그래프 사이의 일치 여부를 확인하여 조용한 발산을 방지합니다.

청사진(The Blueprint)

중심 산물은 **청사진(Blueprint)**으로, 이는 공식적인 증명 스켈레톤이자 자연어 증명 그래프이며 공유된 기록 시스템 역할을 하는 단일 Lean 파일입니다. 여기에는 정리 문구, 중간 보조 정리, 정의 및 산문 설명이 포함됩니다. 의존성 그래프는 Lean의 정교화 메타데이터로부터 추론되며, LaTeX 산문 인용(\cref)에 의해 강제됩니다.

계약 범위 지정 에이전트(Contract-Scoped Agents)

이 하네스는 좁은 인터페이스와 제한된 편집 범위를 가진 네 가지 특화된 에이전트를 운용합니다:

• Blueprinter: 소스 증명과 표준 타겟 문구를 읽어 초기 Lean 스켈레톤을 구성합니다. 증명 본문을 sorry 또는 sorry_using 자리 표시자(placeholder)로 작성합니다. 이의 목표는 "수리 반경"(문구가 틀렸을 때 영향을 받는 하위 선언의 수)을 최소화하는 것입니다.
• Target-Reviewer: 증명이 시작되기 전 청사진을 감사합니다. 표준 타겟, LaTeX 문구, 그리고 Lean 타입을 비교하여 충실도를 확인합니다. 이 에이전트는 청사진을 편집할 수 없으며, 불일치는 이슈로 등록됩니다.
• Worker: 이미 증명된 의존성을 가진 단일 증명 노드에 할당됩니다. 다음 네 단계로 작동합니다:
  1. 오형식화 감사(Misformalization Audit): Lean 문구가 산문 및 의도된 역할과 일치하는지 확인합니다.
  2. 저비용 반증(Cheap Falsification): 수치적 또는 경계값 테스트를 시도하여 주장이 틀렸음을 입증합니다.
  3. 문구 정제(Statement Polish): Lean 타입과 정확히 일치하도록 산문 필드만을 편집합니다.
  4. 형식화(Formalization): 고정된 로컬 영역 내에서 자리 표시자를 완전한 증명으로 대체하려고 시도합니다.
• Refiner: Reviewer나 Worker가 보고한 청사진 수준의 결함을 수리합니다. 청사진 전체를 편집할 수 있지만, 결함을 청사진 드리프트(소스와의 발산) 또는 소스 격차(불완전한 소스 증명)로 분류합니다. 엄격한 결정 트리를 따르며, 수리 후 컴파일되지 않는 경우 완전한 증명 본체를 다시 자리 표시자로 대체하기도 합니다.

오케스트레이션(Orchestration)

시스템은 두 단계로 작동합니다:

1. 1단계 (콜드 스타트/타겟 리뷰): Blueprinter가 스켈레톤을 만들고, Target-Reviewer가 이를 감사하며, Refiner가 이슈를 수리하여 타겟 문구들이 충실하다고 인증될 때까지 반복되는 중첩 루프입니다.
2. 2단계 (DAG 기반 증명 방출): 시스템은 "동적 리프(dynamic leaves)"(의존성이 충족된 미증명 노드)를 식별하고 이를 Worker들에게 병렬로 할당합니다. 모든 풀 리퀘스트(PR)는 병합 전 결정론적인 CI 게이트를 통과해야 합니다. Refiner는 축적된 이슈들을 라운드 단위로 처리합니다. 이 과정은 DAG가 완전히 증명될 때까지 반복됩니다.

주요 기여

1. 에이전트 내구성 프레임워크: 본 논문은 에이전트 내구성을 핵심 병목 현상으로 식별하고, **결함 격리(fault containment)**가 적용된 결함 있는 에이전트들의 시스템을 제안합니다. 적대적인 타겟 리뷰와 병렬 증명 방출을 분리함으로써, 하나의 취약한 다일(multi-day) 실행을 여러 개의 짧고 회복 가능한 병렬 트랜잭션으로 전환합니다.
2. 동적 증명 DAG 정식화: 저자들은 단일 청 blueprint가 공식적 스켈레톤, 자연어 그래프, 기록 시스템 역할을 하는 핵심 정식화를 도입했습니다. 하네스는 이 DAG를 동적으로 성장시키고 수리하며, 리프 노드로부터 상향식으로 병렬적으로 방출합니다.
3. 연구 문제에 대한 실증적 검증: 시스템은 네 개의 Erdős 문제(#1051, #1196, #164, #1217)를 다루는 두 개의 최근 연구 논문에 대해 평가되었습니다.

결과

LeanMarathon은 세 번의 자율 실행을 통해 두 편의 2026년 논문(Barreto et al., 2026; Alexeev et al., 2026)에 대해 평가되었습니다:

• 성공률: 7개의 타겟 정리를 sorry 자리 표시자 없이 모두 형식화했습니다.
• 규모: 총 258개의 보조 정리 및 정리를 증명했습니다.
• 점진적 개발: 시스템은 문제 #1196의 완료된 형식화를 성공적으로 확장하여 문제 #164와 #1217을 포함했으며, 59개의 노드를 변경 없이 재사용하고 145개의 새로운 노드를 추가했습니다.
• 비교: 상용 단일 에이전트 베이스라인(Aristotle)은 수십 시간의 실행 후에도 두 논문 모두에서 실패했으며, 결정적인 간극(예: 논문의 "가장 깊은 수학적 내용")을 남겼습니다.
• 효율성: 편집 가능한 영역을 고정하는 설계 덕분에 병렬 PR 간의 충돌이 발생하지 않았습니다. 시스템은 실패를 개별 노드로 국지화하여, 잘못된 초기 형식화가 후속 연산을 낭비하는 것을 방지했습니다.

의의 및 주장

본 논문은 신뢰할 수 있는 AI 수학 협업을 위해서는 더 강력한 증명기가 아니라, 긴 수학적 발전 과정 전반에 걸쳐 타겟 충실도를 유지할 수 있는 **내구성 있는 하네스(durable harnesses)**가 필요하다고 주장합니다.

• 신뢰성: (보조 정리의) 근접성, 증명 의존성 일치 등을 강제하고 에이전트가 고정된 구간을 편집하지 못하게 함으로써, 시스템은 공식적 기록으로서의 일관성을 보장합니다.
• 수학적 가치: 형식화 과정은 "그라운드 트루스 수학적 신호"로서 작동하여, 인간 독자가 간과할 수 있는 출판된 증명의 격차(예: 누락된 수렴 가설, 해석적 논증의 정당화되지 않은 단계)를 드러냅니다.
• 확장성: 이 아키텍처는 단일 에이전트가 전역적 일관성을 유지하도록 하는 대신, 드리프트와 수리를 국지적으로 처리하도록 설계된다면 연구 수준의 자동 형식화가 가능하다는 것을 보여줍니다.

저자들은 LeanMarathon이, 기초가 되는 Lean 라이브러리(Mathlib)가 해당 도메인에 충분하다는 전제하에, 장기적인 작업이 가독성 있고 회복 가능하며 검증 가능한 AI 수학 협업 데로 향하는 단계임을 결론짓습니다.