Technical Report for AI4Math-2026 Track 2: Mechanically Orchestrated LLM Sub-Agents for Theorem Proving in Lean 4

Motivation

• Known: 기존 연구들은 LeanDojo/ReProver, DeepSeek-Prover, Goedel-Prover, Kimina-Prover 등 whole-proof 혹은 tactic-level generation에 집중했고, DSP, DeepSeek-Prover-V2, Prover Agent, APOLLO 등은 decomposition을 도입했으나 decomposition과 proof 단계 사이의 조율은 여전히 LLM이 담당했다.
• Gap: decomposition 단계와 proof 단계 사이의 coordination decision을 LLM이 아닌 완전히 mechanized된 방식으로 처리하는 시스템이 부재했으며, sub-agent 간 진단 정보 전달 시 해석 계층(interpretive layer) 없이 byte-identical하게 전달하는 원칙도 확립되지 않았다.
• Why: formal verifier 하에서는 soundness가 구조적으로 보장되므로 관건은 invalid proof를 탐지하는 것이 아니라 valid proof를 실제로 만들어내는 것이며, 이를 위해 mathematician의 작업 방식을 모사하는 재현 가능하고 감사 가능한(auditable) 자동화 파이프라인이 중요하다.
• Approach: 정리를 sub-lemma로 분해하고, 반례를 탐색하며, 각 sub-lemma를 독립적으로 증명하고, 라이브러리에 없는 것은 처음부터 구성한 뒤 kernel control 하에 조립하는 working-mathematician 워크플로우를 여섯 개의 LLM sub-agent와 deterministic shell state machine으로 기계화했다.

Achievement

Figure 1. Pipeline workflow for a single challenge. Five of six sub-agents are shown; Campaign (the outer worklist drive

1. 파이프라인 설계: Generator, Refuter, Formalizer Coordinator, Formalizer Node, Inliner, Campaign의 6개 sub-agent와 이를 조율하는 deterministic shell state machine을 통해 모든 coordination decision을 reproducible하고 auditable하게 만들었다.
2. verbatim-preservation 원칙: sub-agent 간 진단 정보(diagnostic output)를 해석 계층 없이 byte-identical하게 전달하는 원칙을 확립했다.
3. benchmark 성과: ICML 2026 AI4Math Challenge 2의 34개 challenge 중 30개(600/1000점)를 kernel-verified 방식으로 해결했으며, human-in-the-loop 개입 없이 모든 sub-agent dispatch 및 coordination decision을 수행했다.
4. failure mode 분석: 파이프라인이 겪은 4가지 실패 모드와 그 해결책을 카탈로그화했다.

How

Figure 1. Pipeline workflow for a single challenge. Five of six sub-agents are shown; Campaign (the outer worklist drive

• 정리를 sub-lemma로 decompose하고 Refuter sub-agent가 counterexample을 probe함
• Generator가 각 sub-lemma를 독립적으로 증명 시도
• Formalizer Coordinator/Node가 필요한 library fact를 검색하거나 부재 시 처음부터 construct
• Inliner가 검증된 조각들을 kernel control 하에 assemble
• Campaign sub-agent가 전체 진행을 관리
• 6개 sub-agent 간 조율은 모두 deterministic shell state machine이 담당하며 LLM은 개입하지 않음
• 진단 출력은 sub-agent 사이에서 byte-identical하게 전달되어 해석 계층으로 인한 정보 손실/왜곡을 방지
• validation gate(Section 4.5)에서 byte-pristine submission, 3개 permitted axioms, 공식 judge인 SafeVerify, implicit heartbeat budget(200,000-heartbeat) 등 challenge 고유 제약을 확인
• 모든 sub-agent prompt와 dispatch template은 challenge별로 튜닝되지 않고 동일하게 적용, challenge-specific 내용은 pristine challenge file과 per-challenge scoped library index(+1-hop)를 통해서만 반영

Originality

• LLM sub-agent 간 coordination을 LLM이 아닌 순수 deterministic shell state machine으로 완전히 기계화한 최초의 시도로, 기존 decomposition 파이프라인들(DSP, DeepSeek-Prover-V2, Prover Agent, APOLLO 등)이 LLM-driven coordination에 의존하던 것과 차별화됨
• sub-agent 간 diagnostic 정보 전달에 해석 계층 없이 byte-identical하게 전달하는 verbatim-preservation 원칙을 명시적으로 도입
• working mathematician의 인지적 workflow(분해-반례탐색-독립증명-구성-조립)를 여섯 개의 역할 분리된 sub-agent로 명시적으로 대응시킨 설계

Limitation & Further Study

• 34개 challenge 중 4개는 여전히 실패했으며, 이 실패 모드들이 근본적으로 해결 가능한지 혹은 파이프라인의 구조적 한계인지에 대한 논의가 제한적임
• 단일 benchmark(ICML 2026 AI4Math Challenge 2, CSLib 기반 TCS 도메인)에 대해서만 검증되어 일반화 가능성(다른 수학 분야, 다른 Lean 라이브러리)에 대한 근거가 부족함
• deterministic shell state machine이 실제로 얼마나 복잡한 coordination logic을 감당할 수 있는지, 더 어려운 정리나 더 큰 스케일에서도 확장 가능한지에 대한 분석이 부족함
• technical report 형태로 ablation이나 각 sub-agent의 개별 기여도에 대한 정량적 분석이 상대적으로 제한적일 가능성이 있음
• 후속 연구로는 다양한 도메인 및 더 큰 benchmark(miniF2F 등)로의 확장, sub-agent 조율 로직의 이론적 정당화, 실패 모드에 대한 자동 복구 메커니즘 강화 등이 필요함

Evaluation

총평: LLM 기반 자율 판단을 최소화하고 결정론적 조율 메커니즘으로 대체한다는 아이디어는 formal proof 자동화에서 신뢰성과 재현성을 높이는 실용적이고 참신한 접근이며, 실제 competitive benchmark에서 높은 solve rate를 보여 기술적 타당성을 입증했다.