StepFun-Formalizer : Libérer le potentiel d'autoformalisation des LLM grâce à la fusion connaissance-raisonnement
StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
August 6, 2025
papers.authors: Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu
cs.AI
papers.abstract
L'autoformalisation vise à traduire des énoncés mathématiques en langage naturel dans un langage formel. Bien que les modèles de langage de grande taille (LLMs) aient accéléré les progrès dans ce domaine, les méthodes existantes souffrent encore d'une faible précision. Nous identifions deux compétences clés pour une autoformalisation efficace : une maîtrise approfondie des connaissances du domaine du langage formel, et une capacité de raisonnement pour la compréhension des problèmes en langage naturel et l'alignement informel-formel. Sans la première, un modèle ne peut pas identifier les objets formels corrects ; sans la seconde, il peine à interpréter les contextes réels et à les mapper précisément en expressions formelles. Pour combler ces lacunes, nous introduisons ThinkingF, un pipeline de synthèse de données et d'entraînement qui améliore ces deux compétences. D'abord, nous construisons deux ensembles de données : l'un en distillant et en sélectionnant des exemples à grande échelle riches en connaissances formelles, et l'autre en générant des trajectoires de raisonnement informel-formel guidées par des modèles conçus par des experts. Nous appliquons ensuite l'apprentissage supervisé fin (SFT) et le renforcement par récompense verbale (RLVR) avec ces ensembles de données pour fusionner et affiner davantage ces deux compétences. Les modèles résultants de 7B et 32B montrent à la fois une connaissance formelle complète et un raisonnement solide de l'informel au formel. Notamment, StepFun-Formalizer-32B atteint des scores BEq@1 de pointe de 40,5 % sur FormalMATH-Lite et de 26,7 % sur ProverBench, surpassant tous les modèles généralistes et spécialisés précédents.
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.