MerLean: An Agentic Framework for Autoformalization in Quantum Computation

Motivation

• Known: 최근 LLM 기반 자동형식화(autoformalization)와 멀티에이전트 정리증명 시스템이 경쟁 수준의 문제들에서 성과를 보였음. Ax-Prover, Numina-Lean-Agent 등이 인간의 지도하에 연구급 수학을 형식화함.
• Gap: 기존 접근법들은 모두 인간의 개입(human-in-the-loop)을 필요로 함. 정의, 정리, 증명 전략을 수동으로 제공해야 하며, 전체 논문 규모에서 완전 자동화된 형식화는 실현되지 않음.
• Why: 양자계산 분야는 연간 11,891개 arXiv 논문 투고로 인한 검증 병목 현상 발생. 동시에 선형대수, 그래프 이론, 위상수학 등 강력한 수학적 기초를 가지므로 신경기호적 검증에 적합함.
• Approach: 완전 자동화된 에이전트 프레임워크로 LaTeX 논문에서 명제를 추출→형식화→검증하고, 역으로 형식화된 코드를 인간이 읽을 수 있는 자연언어로 변환하는 양방향 파이프라인 구축.

Achievement

명제별 컴파일 시도 횟수 분포: 대부분의 명제는 1-10회 시도로 해결되지만 장기 꼬리를 형성하는 '어려운' 명제들이 존재

1. 완전 자동화 전체 논문 형식화: 3개 이질적 양자계산 논문(균형 곱 코드, 내결함 양자계산, 양자위상수학)에서 인간 개입 없이 114개 명제를 모두 형식화 성공. 특히 공개되지 않은 미발표 원고 포함으로 훈련 데이터 오염 완전 배제.
2. 규모있는 형식화 결과: 총 42시간 내에 2,050개 Lean 선언 생성 (균형 곱 코드: 14,997행/730선언, 내결함 QC: 18,557행/923선언, 양자위상: 7,761행/397선언).
3. 투명한 가정 처리: 미포함된 Mathlib 기능(스펙트럼 수열, Künneth 동형사상)에 대해 명시적 공리로 선언하여 의도적 가정과 미완성 증명을 구별. Balanced Product 논문의 9.1%만 공리화 필요.
4. 양방향 검증 가능성: 형식화된 Lean 코드를 다시 자연언어로 변환하여 인간 전문가가 의미적 일관성을 검토할 수 있는 blueprint 제공.

How

• 명제 추출(Statement Extraction): LaTeX 논문에서 정의, 정리, 보조정리 등 수학 명제를 구조화된 JSON으로 추출. 다단계 반복 처리로 모호한 표현("표준 논증으로"→구체 증명단계)을 명확화하고 의존성 순서 정렬.
• 반복적 형식화(Iterative Formalization): 각 명제마다 컴파일-수정 루프 실행. 컴파일 오류 메시지를 에이전트에 피드백하여 자동 수정. 최대 시도 횟수 도달 시 공리화 단계로 전환.
• 도구 활용: lean-lsp-mcp를 통해 Lean 언어 서버 기능 직접 노출. lean goal로 증명 상태 검사, lean hover info로 타입 시그니처 확인, leansearch/loogle로 관련 Mathlib 보조정리 발견.
• 충실성 검사(Faithfulness Checking): 타입 검사 성공 후 형식화된 결과가 원래 의미를 올바르게 표현하는지 LLM이 재검토. 의미적 불일치 시 재시도.
• 자동비형식화(Autoinformalization): 검증된 Lean 4 코드를 LLM이 자연언어로 역변환. 형식화 수행 모델이 해당 분야 전문성을 보였으므로 역방향도 가능. leanblueprint 호환 대화형 출력 및 교과서 스타일 서사 제공.

Originality

• 완전 자동화의 실현: 기존 Ax-Prover, Numina-Lean-Agent 등은 인간이 정의/정리/전략을 제공해야 하나, MerLean은 문장 추출부터 형식화까지 완전 자동화. 이는 연구급 수학에서 처음 달성한 결과.
• 양방향 형식화: 단방향 형식화가 아닌 양방향 파이프라인으로 기계검증성과 인간검증 가능성을 동시 확보. 의미적 일관성 검토를 위한 blueprint 생성은 새로운 기여.
• 영역 확장성: 양자계산 한정이 아닌 "엄밀한 수학 및 이론물리 모든 분야"로 일반화 가능함을 명시. Lean-QuantumInfo 등 기존 라이브러리와 시너지 창출.
• 투명한 가정 처리: sorry(불완전 증명)와 구별되는 명시적 공리 선언으로 미해결 과제를 투명하게 표시. Mathlib 확장에 따라 점진적으로 채울 수 있는 구조.

Limitation & Further Study

• Mathlib 의존성: 고급 대수기계(스펙트럼 수열, 특정 계수환에 대한 Künneth)가 Mathlib에 미포함되면 공리화 필요. 논문 도메인이 확대될수록 공리화 비율 증가 가능성.
• 인간 검토 부담: 새로운 정의와 공리에 대한 "수동 검토"가 여전히 필요함. 완전 자동화가 아닌 "검증 부담 감소"에 그침. 정의의 적절성까지 자동검증하는 메커니즘 부재.
• 평가 규모 제한: 3개 논문만 평가. 다양한 도메인, 복잡도, 길이의 논문에서의 확장성 미검증. 특히 기하학, 해석학 등 다른 분야에서의 성능 불명확.
• 세밀한 오류 분석 부족: 공리화되거나 실패한 명제들의 원인을 상세히 분류하지 않음. "왜" 어려운지(Mathlib 부족 vs 형식표현 난제 vs 에이전트 능력 한계)에 대한 깊이 있는 분석 부재.
• 후속 연구: (1) 동적 공리 재검증 방식 개발, (2) 다중 도메인 벤치마크 구축, (3) 합성 데이터 품질 평가 및 추론 모델 학습 파이프라인 완성.

Evaluation

총평: MerLean은 LLM 에이전트가 인간 개입 없이 실제 연구 논문을 대규모로 형식화할 수 있음을 최초로 입증한 주목할 만한 연구다. 양방향 설계로 기계검증과 인간검증을 결합하는 실용적 접근이 인상적이며, 양자계산을 넘어 수학·물리 전반으로의 확장 가능성도 높다. 다만 새로운 정의/공리의 인간 검토 필요성, 제한된 평가 범위, 미명확한 기술 상세사항이 보완 필요 영역이다.