MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hengyu Zhao, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang
cs.AI, cs.CL
2026-08-14
Retrieval from Mathlib plus three rounds of compiler and semantic checks yield 367K verified pairs; an 8B model trained on them beats 32B specialist autoformalizers.
Autoformalization converts natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. The hard part is not translation. Mathlib has a deep hierarchy of types and definitions; a concept may already have a canonical definition there, and the model must find the right mapping while preserving the meaning of the source proposition, with no dropped assumptions, no strengthened conditions, and no shifted quantifiers. Current approaches fail two ways: they lean on parametric memory to guess library-specific knowledge, and their data pipelines filter single-pass outputs with no feedback-driven revision.
MathForm has three stages:
Iteration carries real weight: the first round produces about 69% of retained pairs, the second and third add roughly 20% and 11%, so refinement recovers 31% of the data that single-pass generation would discard.
The pipeline yields FormalVerse, about 367K verified natural-language-to-formal pairs drawn from DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath, OpenR1-Math, and classical textbooks, spanning ten mathematical categories, decontaminated against evaluation benchmarks by 13-gram matching. Training is two-step: Qwen3-8B is fine-tuned on FormalVerse, then trained with DAPO under a binary reward for compilation plus semantic consistency.
Average Pass@8 across six benchmarks, against specialist baselines:
| Model | SC | CC |
| MathForm-8B | 88.06% | 72.37% |
| ReForm-32B | 81.61% | 68.41% |
| Goedel-Formalizer-V2-32B | 78.28% | 63.74% |
| StepFun-Formalizer-32B | 63.65% | 44.47% |
Against the strongest specialist baseline, ReForm-32B, the absolute gains are +6.45 SC and +3.96 CC, at a quarter of the parameter count. The RL stage is measurable on its own: SFT-only reaches 84.38/66.53, and RL takes it to 88.06/72.37, with the larger gain on CC, meaning verification-driven RL improves semantic alignment more than compilability, which was already near saturation. On the hard FATE subsets, CC is 97.33% on FATE-M, 63.00% on FATE-H, and 37.00% on FATE-X, each above the strongest specialist baseline. The judge itself is calibrated: gpt-oss-120b at high reasoning effort scores F1 = 0.8940 on 200 human-annotated examples.
Formalized data is the bottleneck asset for theorem proving, and this pipeline turns retrieval, executable checking, and LLM semantic judging into a data factory where the entire 31% increment comes from iterative refinement. The 367K verified pairs are released. The 8B size runs on a single GPU, so teams working on mathematical reasoning or formal methods can deploy it locally. The recipe transfers: any task whose outputs can be partially machine-verified can borrow the dual-gate refinement of compiler diagnostics plus a semantic judge.
The authors state that the average CC of 72.37% still trails frontier general-purpose models: Qwen3.7-Plus at 83.38% and DeepSeek-V4-Pro at 76.54%. Specialized training buys compilability, while frontier models keep the edge in semantic fidelity. Two unquantified concerns: the CC training signal is itself an LLM judgment with F1 0.894, so roughly one label in ten is wrong, and the paper does not measure how that noise propagates through RL; retrieval depends on LeanExplore's coverage of Mathlib, and Coq or Isabelle have no equivalent ready to use. FATE-X at 37% says out-of-distribution propositions remain hard.