TLDR: The research paper introduces ThinkingF, a novel data synthesis and training pipeline designed to significantly improve the accuracy of autoformalization, the process of translating natural-language mathematical statements into formal languages. By fusing comprehensive formal knowledge and strong informal-to-formal reasoning capabilities into LLMs, ThinkingF addresses key limitations of existing methods. The resulting StepFun-Formalizer models achieve state-of-the-art performance on various benchmarks, demonstrating a breakthrough in automating mathematical formalization and enhancing the potential for automated theorem proving.
In the rapidly evolving field of artificial intelligence, a significant challenge lies in bridging the gap between human language and the precise, unambiguous world of formal mathematics. This is the goal of autoformalization: translating natural-language mathematical statements into formal languages like Lean, Coq, or Isabelle, which can then be verified by automated theorem provers. While large language models (LLMs) have shown promise in this area, achieving high accuracy remains a hurdle, often requiring substantial human intervention for corrections.
A recent research paper, titled StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion, identifies two critical abilities for effective autoformalization: a comprehensive grasp of formal-language domain knowledge and robust reasoning capability. Without deep formal knowledge, models struggle to identify correct formal objects. Without strong reasoning, they fail to interpret real-world contexts and accurately map them into formal expressions. The authors, Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, and Xing Hu, propose an innovative solution called ThinkingF.
Introducing ThinkingF: A Novel Pipeline for Enhanced Autoformalization
ThinkingF is a data synthesis and training pipeline designed to enhance both the formal knowledge and reasoning abilities of LLMs. It addresses the limitations of existing methods, which often suffer from low accuracy and high human effort. The pipeline consists of four main stages, focusing on data construction and model training.
Building a Foundation: Knowledge and Reasoning Datasets
The first two stages of ThinkingF are dedicated to creating high-quality datasets. For formal knowledge, the researchers developed a large-scale dataset by distilling and selecting informal-formal pairs. This involved using a specialized LLM (Kimina-Autoformalizer) to translate natural language problems into formal statements, followed by a rigorous three-tier quality selection process. This process included syntax checks, majority voting among generated statements, and an LLM-based validity assessment to filter out trivial or contradictory problems.
To bolster reasoning capability, ThinkingF introduces a novel approach to synthesize informal-to-formal reasoning trajectories. Guided by an expert-designed template, a powerful instruction-following model (Claude 3.7 Sonnet) generated step-by-step reasoning processes for existing human-annotated informal-formal data pairs. This template encourages problem decomposition, mathematical object mapping, and anticipation of tricky formalization issues, ensuring the reasoning focuses on the translation process rather than problem-solving.
Training for Excellence: Supervised Fine-tuning and Reinforcement Learning
With these specialized datasets, the training process begins. ThinkingF employs a two-stage supervised fine-tuning (SFT) approach on a general-purpose LLM known for its mathematical and coding abilities (DeepSeek-R1-Distill-Qwen). The first stage integrates formal knowledge, while the second stage fuses in the reasoning trajectories. This sequential fine-tuning ensures the model acquires both capabilities effectively.
Finally, to further refine and fuse these abilities, the fine-tuned model undergoes reinforcement learning (RL) with a verifiable reward. The reward mechanism is based on Bidirectional Extended Definitional Equivalence (BEq) verification, which checks if the model’s generated formal statements are semantically equivalent to the ground truth. This direct feedback loop helps the model learn to produce more accurate and verifiable formalizations.
Also Read:
- Enhancing Mathematical Problem-Solving with Knowledge Graphs and Executable Code
- Deliberative Reasoning Networks: A New Path to Logical AI
Groundbreaking Results and Future Implications
The effectiveness of ThinkingF is evident in the performance of the resulting models, StepFun-Formalizer-7B and StepFun-Formalizer-32B. Notably, StepFun-Formalizer-32B achieved state-of-the-art BEq@1 scores of 40.5% on FormalMATH-Lite and 26.7% on ProverBench. These results surpass all prior general-purpose and specialized models, demonstrating the superior autoformalization capabilities and generalization of the ThinkingF pipeline. Even the smaller 7B model outperformed many larger competitors, highlighting its computational efficiency.
The research also shows that both the knowledge and reasoning datasets contribute significantly to performance, with reasoning being a primary driver. The template-guided reasoning synthesis proved more effective than direct distillation from general reasoning LLMs, which often exhibited off-task behaviors. Furthermore, the study demonstrated that StepFun-Formalizer can generate more verifiable formal statements across different mathematical domains, which is crucial for synthesizing diverse training data for theorem-proving models.
In conclusion, ThinkingF represents a significant leap forward in autoformalization by systematically integrating formal knowledge and informal-to-formal reasoning into LLMs. This approach not only improves accuracy but also paves the way for more robust automated theorem proving and verifiable code generation, bringing us closer to a future where AI can truly understand and formalize complex mathematical concepts.
