MathForm: 지식 검색 및 검증 기반 개선을 통한 수학 자동 형식화 확장

MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

자동 형식화는 일반적으로 자연어 형태의 수학적 명제를 기계가 검증할 수 있는 Lean 4와 같은 형식 언어로 번역하는 것으로 정의됩니다. 그러나 정확한 형식화는 단순한 번역 이상을 요구합니다. 모델은 수학적 개념을 Mathlib과 같은 형식 라이브러리의 복잡한 유형 및 정의 체계에 매핑해야 하며, 동시에 생성된 명제가 원본 명제의 의미를 유지하도록 해야 합니다. 기존 접근 방식은 모델의 파라메트릭 메모리에 크게 의존하여 라이브러리별 지식을 활용하지만, 일반적인 데이터 구축 파이프라인은 종종 단일 패스 출력을 필터링하며 피드백 기반 수정 메커니즘을 결여합니다. 이러한 과제를 해결하기 위해, 우리는 Mathlib 지식 검색 및 검증 기반 반복 개선을 통해 검증된 학습 데이터를 생성하는 자동 형식화 프레임워크인 MathForm을 소개합니다. 생성 전에, 검색 계획기는 형식화 생성기를 안내하기 위해 Mathlib에서 관련 정의와 기존 형식화를 수집합니다. 생성된 명제는 컴파일러 진단 및 의미적 일관성 피드백을 사용하여 수정됩니다. 이 프레임워크를 통해, 다양한 수학 분야와 소스에 걸쳐 약 367,000개의 검증된 예제를 포함하는 Lean 4 데이터셋인 FormalVerse를 구축했습니다. 그런 다음 MathForm-8B 모델을 지도 학습 방식으로 미세 조정하고 강화 학습으로 추가 학습시켰습니다. 여섯 가지 벤치마크에서, MathForm-8B는 Syntax Check (SC) 조건에서 평균 Pass@8 비율이 88.06%, Consistency Check (CC) 조건에서 72.37%를 달성하여 여러 전문적인 32B 자동 형식화 모델보다 우수한 성능을 보였습니다. 특히 어려운 FATE-H 및 FATE-X 서브셋에서, 각각 63%와 37%의 CC Pass 비율을 기록하여 가장 강력한 전문 기본 모델을 모두 능가했습니다.

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.