StepFun-Formalizer-7B: Autoformalization for Mathematics

StepFun-Formalizer-7B is a 7.6 billion parameter large language model developed by stepfun-ai, specializing in autoformalization. Its core function is to translate natural-language mathematical problems into formal statements using the Lean 4 proof assistant.

Key Capabilities

• Natural Language to Lean 4 Translation: Converts informal mathematical problem descriptions into precise Lean 4 code.
• Knowledge-Reasoning Fusion: Integrates formal mathematical knowledge with advanced reasoning capabilities to achieve high accuracy in formalization.
• Strong Benchmark Performance: Evaluated against mainstream autoformalization benchmarks including FormalMATH-Lite, ProverBench, and CombiBench, where it demonstrates performance comparable to or exceeding other specialized and general-purpose models of similar scale.

Good For

• Automated Theorem Proving: Assisting in the formalization step for automated theorem provers.
• Mathematical Research: Helping mathematicians formalize their conjectures and proofs in Lean 4.
• Educational Tools: Creating tools that aid students in understanding and formalizing mathematical concepts.

This model is released under the Apache License (Version 2.0). More details can be found in the associated paper.