stepfun-ai/StepFun-Formalizer-7B
StepFun-Formalizer-7B by stepfun-ai is a 7.6 billion parameter large language model with a 131072 token context length, specifically designed for autoformalization. It translates natural-language mathematical problems into formal statements in Lean 4 by fusing formal knowledge and informal-to-formal reasoning. The model achieves strong performance on autoformalization benchmarks like FormalMATH-Lite, ProverBench, and CombiBench, matching or exceeding prior models of comparable scale.
Loading preview...
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.