StepFun-Formalizer: 知識推論融合によるLLMの自動形式化可能性の解放

StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion

August 6, 2025

著者: Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu

cs.AI

要旨

自動形式化は、自然言語で記述された数学的命題を形式言語に翻訳することを目指す。LLM（大規模言語モデル）がこの分野の進展を加速しているものの、既存の手法は依然として精度の低さに悩まされている。効果的な自動形式化には、形式言語のドメイン知識を包括的に習得する能力と、自然言語の問題理解および非形式的-形式的な整合性を推論する能力という2つの重要な能力が必要である。前者がなければ、モデルは正しい形式的対象を特定できず、後者がなければ、現実世界の文脈を解釈し、それを正確に形式的表現にマッピングすることが困難となる。これらの課題に対処するため、我々はThinkingFを提案する。これは、両方の能力を向上させるデータ合成およびトレーニングパイプラインである。まず、形式知識が豊富な大規模な例を蒸留・選択して構築したデータセットと、専門家が設計したテンプレートに基づいて非形式的から形式的な推論軌跡を生成したデータセットを作成する。次に、これらのデータセットを用いてSFT（Supervised Fine-Tuning）とRLVR（Reinforcement Learning with Value-based Rewards）を適用し、両方の能力をさらに融合・洗練させる。その結果、7Bおよび32Bのモデルは、包括的な形式知識と強力な非形式的-形式的推論能力を兼ね備えた。特に、StepFun-Formalizer-32Bは、FormalMATH-Liteで40.5%、ProverBenchで26.7%のSOTA BEq@1スコアを達成し、これまでの汎用モデルおよび専門モデルをすべて上回った。

English

Autoformalization aims to translate natural-language mathematical statements into a formal language. While LLMs have accelerated progress in this area, existing methods still suffer from low accuracy. We identify two key abilities for effective autoformalization: comprehensive mastery of formal-language domain knowledge, and reasoning capability of natural language problem understanding and informal-formal alignment. Without the former, a model cannot identify the correct formal objects; without the latter, it struggles to interpret real-world contexts and map them precisely into formal expressions. To address these gaps, we introduce ThinkingF, a data synthesis and training pipeline that improves both abilities. First, we construct two datasets: one by distilling and selecting large-scale examples rich in formal knowledge, and another by generating informal-to-formal reasoning trajectories guided by expert-designed templates. We then apply SFT and RLVR with these datasets to further fuse and refine the two abilities. The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning. Notably, StepFun-Formalizer-32B achieves SOTA BEq@1 scores of 40.5% on FormalMATH-Lite and 26.7% on ProverBench, surpassing all prior general-purpose and specialized models.