MathForm: 지식 검색 및 검증 기반 정제를 통한 수학적 자동형식화 확장

초록

자동 형식화(autoformalization)는 자연어 수학 명제를 Lean 4와 같은 기계 검증 가능한 형식 언어로 번역하는 것으로 흔히 간주된다. 그러나 충실한 형식화는 단순한 번역 이상을 요구한다. 모델은 수학적 개념을 Mathlib과 같은 형식 라이브러리에 존재하는 복잡한 타입 및 정의의 계층 구조에 매핑해야 하며, 동시에 생성된 명제가 원래 명제의 의미를 보존하도록 보장해야 한다. 기존 접근 방식은 라이브러리 특정 지식에 대해 모델의 파라메트릭 메모리에 크게 의존하고, 일반적인 데이터 구축 파이프라인은 종종 단일 패스 출력을 필터링하거나 피드백 기반 수정 메커니즘이 부족하기 때문에 어려움을 겪는다. 이러한 문제를 해결하기 위해 우리는 Mathlib 지식 검색과 검증 기반 반복 개선을 통해 검증된 훈련 데이터를 구축하는 자동 형식화 프레임워크인 MathForm을 소개한다. 생성 전에 검색 계획자가 Mathlib에서 관련 정의와 기존 형식화를 수집하여 형식화 생성기를 안내한다. 이후 생성된 명제는 컴파일러 진단 및 의미 일관성 피드백을 활용하여 수정된다. 이 프레임워크를 사용하여 우리는 다양한 수학 분야와 출처에 걸쳐 약 367K개의 검증된 예제를 포함하는 Lean 4 데이터셋인 FormalVerse를 구축한다. 그런 다음 지도 미세 조정과 강화 학습을 통해 MathForm-8B를 훈련한다. 6개의 벤치마크에서 MathForm-8B는 구문 검사(SC) 기준 평균 Pass@8 88.06%, 일관성 검사(CC) 기준 72.37%를 달성하여 여러 특화된 32B 자동 형식화 모델보다 우수한 성능을 보인다. 특히 어려운 FATE-H 및 FATE-X 하위 집합에서는 각각 63%와 37%의 CC 통과율을 달성하여 두 경우 모두 가장 강력한 특화 기준선을 능가한다.

English

Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.