연구 수준 수학의 장기 자동형식화(autoformalization)는 어려운 보조정리뿐 아니라 규모에서도 실패한다. 진술이 표류하고 의존성이 엉키며 컨텍스트가 쇠퇴하고 국소 수정이 멀리 떨어진 작업을 망가뜨린다. 이 논문은 신뢰할 수 있는 연구급 Lean 자동형식화를 위한 다중 에이전트 하니스 LeanMarathon을 제시한다. 핵심 추상화는 '진화하는 블루프린트'로, 형식 증명 골격이자 자연어 증명 그래프이며 공유 기록 시스템 역할을 동시에 하는 Lean 파일이다. 계약 범위가 정해진 네 에이전트가 이를 구성·감사·증명·수정하고, 2단계 오케스트레이터가 적대적 검토로 목표 충실도를 안정화한 뒤 증명 DAG를 동적 리프부터 위로 병렬 CI 게이트 라운드로 처리한다. 이로써 깨지기 쉬운 수 시간짜리 단일 실행을 국소적·복구 가능·병렬 트랜잭션으로 바꾼다. 에르되시 문제 4개(#1051·#1196·#164·#1217)를 다룬 최근 논문 2편에서 3회 자율 실행으로 목표 정리 7개를 모두 sorry 없이 형식화하고 258개 보조정리·정리를 증명했다.
- •장기 자동형식화의 실패 원인(진술 표류·의존성 엉킴·컨텍스트 쇠퇴)을 다중 에이전트 하니스로 해결
- •형식 증명 골격·자연어 그래프·공유 기록을 겸하는 '진화하는 블루프린트'가 핵심 추상화
- •구성·감사·증명·수정 4개 에이전트와 2단계 오케스트레이터(적대적 검토 → 병렬 CI 증명)
- •수 시간짜리 단일 실행을 국소·복구·병렬 트랜잭션으로 전환
- •에르되시 문제 4개에서 정리 7개를 sorry 없이 형식화, 총 258개 보조정리·정리 증명
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
- 1.AI 수학자 신뢰성 향상
- 2.장기 자동 형식화 난제 극복
- 3.LeanMarathon 시스템 제안
왜 중요한가?
AI를 활용한 수학 연구의 자동 형식화 과정에서 발생하는 스케일 문제와 신뢰성 문제를 해결하기 위한 다중 에이전트 시스템을 제안합니다. 이는 AI의 수학적 추론 능력을 획기적으로 향상시켜, 복잡한 수학 증명 및 이론 개발을 가속화할 잠재력이 있습니다.
🏷️ 언급 프로젝트
AI 기반 수학 연구 보조는 첨단 과학기술 분야에서 중요한 진전을 가져올 수 있으며, 이 연구는 장기적인 수학적 자동 형식화 과정에서 발생하는 신뢰성 문제를 해결하기 위한 다중 에이전트 시스템 LeanMarathon을 제시합니다. 이는 국내 AI 연구자들이 복잡한 수학적 문제를 해결하고 새로운 발견을 이끌어내는 과정에서 AI의 정확성과 지속성을 높이는 데 기여하며, 장기적인 R&D 경쟁력 강화에 일조할 것입니다.
본문 미리보기
arXiv:2606.05400v1 Announce Type: new Abstract: Long-horizon autoformalization of research mathematics fails not only at hard lemmas, but at scale: statements drift, dependencies tangle, context decays, and local repairs corrupt distant work. We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization. Its core abstraction is an evolving blueprint: a Lean file that serves simultaneously as formal proof skeleton, natural-language proof graph, and shared syst
전체 내용이 궁금하다면?
원문을 직접 읽어보세요