도서관을 넘어: 연구 수학의 자동 형식화에 대한 주체 기반 프레임워크

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

대규모 언어 모델(LLM)은 수학적 추론 능력에서 뛰어난 성능을 보여주지만, 종종 인간이 감지하기 어려운 미묘한 오류를 생성합니다. Lean 4와 같은 형식 수학 언어는 기계적인 증명 검증 기능을 제공하며, 이는 자동 형식화의 필요성을 강조합니다. 자동 형식화란 자연어 수학을 검증 가능한 코드로 자동으로 변환하는 기술입니다. 최근 동향은 표준 프로그래밍에 최적화된 범용 LLM이 Lean에 특화되어 미세 조정된 작은 모델보다 더 뛰어난 성능을 보인다는 것을 보여줍니다. 이러한 변화를 활용하여, 우리는 범용 코딩 LLM으로 구동되는 주체 기반 자동 형식화 프레임워크를 소개합니다. 우리 시스템의 핵심은 연구 수준의 수학에 맞게 설계된 다중 에이전트 파이프라인을 관리하는 오케스트레이터입니다. 최첨단 연구는 종종 기존 라이브러리(예: Mathlib)의 범위를 벗어나는 개념에 의존하므로, 우리 시스템은 필요한 타입 정의를 동적으로 확장하고, 혁신적인 보조 정리 기술을 통해 이를 검증한 후 주요 정리를 형식화합니다. 우리는 제안하는 방법을 PutnamBench 데이터셋에 적용하여 32개의 문제에 대해 기계적으로 검증된 Lean 증명을 생성했습니다. 또한, 우리 시스템을 ACM Symposium on Theory of Computing (STOC)의 조합론, 통신 복잡성, 메커니즘 설계 및 학습 이론 분야의 5개 논문에 적용하여 주요 정리를 성공적으로 형식화하고, 생성된 형식화를 인간 전문가를 통해 검증했습니다. 이 다섯 가지 사례 모두에서 우리는 정리와 함께 증명도 형식화했으며, 주목할 만한 점은 두 사례는 Lean의 핵심 기능 외에는 어떠한 공리도 사용하지 않고 증명되었습니다. 모든 형식화 결과는 https://beyondthelibrary.github.io/formal_arxiv 에서 확인할 수 있습니다.

While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .