In the intersection of modern mathematics and artificial intelligence, how to enable machines to accurately "read" and verify mathematical theorems through formalization has always been one of the core challenges in overcoming general artificial intelligence (AGI). Recently, the OpenBMB team officially released a new open-source framework, dataset, and model for mathematical formalization—MathForm.
For a long time, mathematical formalization (such as based on the Lean4 language) is not just about translating natural language into code. A rigorous model must precisely map each mathematical concept to the correct type and definition in the Mathlib library. The industry often faces a pain point: even if a formalized statement can pass the compiler, it may still fail to accurately describe the original problem semantically.
To tackle this challenge, the MathForm framework innovatively introduces a retrieval-augmented and verification-guided data construction mechanism. The core logic lies in the system first extracting the required Mathlib definitions and existing formalized models through a retrieval planner; then, the generator will revise the output content up to three times based on the diagnostic results from the Lean compiler and semantic consistency feedback, thereby significantly ensuring the quality of the code and the consistency of the mathematical semantics.
In terms of data and models, OpenBMB introduced the FormalVerse dataset, which includes more than 367,000 verified Lean4 examples, covering diverse mathematical fields and sources. Experimental results show that, under the same training budget and initial conditions, the consistency check rate of models trained with FormalVerse reached 60.32%, far exceeding FineLeanCorpus's 46.53% and NuminaMath-LEAN's 41.49%.
As one of the core achievements, the MathForm-8B model delivered impressive results in six benchmark tests, achieving an 88.06% syntax check pass rate and a 72.37% consistency check pass rate (on an 8-point scale). Particularly notable is that it outperformed larger models such as ReForm-32B and Goedel-Formalizer-V2-32B with only a quarter of their parameter size. Especially in the most challenging FATE-H and FATE-X subsets, its consistency check success rates reached 63% and 37% respectively, surpassing the strongest specialized benchmarks by 10 and 12 percentage points, demonstrating strong reasoning and formal error correction capabilities.
Project address: https://github.com/openbmb/MathForm
