openbmb/MathForm-8B

MathForm-8B: Autoformalization for Lean 4

MathForm-8B is an 8 billion parameter model developed by OpenBMB, specifically engineered for mathematical autoformalization. Its primary function is to translate informal mathematical statements written in natural language into formal Lean 4 code.

Key Capabilities & Training

• Lean 4 Autoformalization: Directly converts natural language math into Lean 4 formal proofs.
• Advanced Training Methodology: Utilizes supervised fine-tuning on the FormalVerse dataset, followed by reinforcement learning. This RL phase incorporates feedback from Lean compilation and semantic consistency checks, enhancing the reliability and correctness of the generated formalizations.
• Knowledge Retrieval and Verification: The training pipeline integrates Mathlib knowledge retrieval and verification-guided refinement, allowing the model to generate robust formal data.
• High Context Length: Supports a context length of 32768 tokens, enabling the processing of longer and more complex mathematical descriptions.

Performance & Usage

MathForm-8B demonstrates competitive performance on various autoformalization benchmarks, as detailed in its accompanying paper. It is designed for integration with standard LLM inference frameworks like Transformers, vLLM, and SGLang, with recommended settings for optimal generation quality (temperature 0.6, top_p 0.95, max_new_tokens 16384).

Ideal Use Cases

• Formalizing Mathematical Texts: Automating the conversion of mathematical papers or textbooks into formal proof languages.
• Assisting Proof Engineers: Providing a powerful tool for generating initial formalizations that can then be refined.
• Educational Tools: Helping students and researchers understand the formal structure of mathematical concepts.