StepFun-Formalizer: Sbloccare il Potenziale di Autoformalizzazione dei Modelli Linguistici di Grande Dimensione attraverso la Fusione di Conoscenza e Ragionamento

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

August 6, 2025

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

cs.AI

Abstract

L'autoformalizzazione mira a tradurre enunciati matematici in linguaggio naturale in un linguaggio formale. Sebbene i modelli linguistici di grandi dimensioni (LLM) abbiano accelerato i progressi in questo ambito, i metodi esistenti soffrono ancora di una bassa accuratezza. Identifichiamo due abilità chiave per un'autoformalizzazione efficace: una padronanza completa delle conoscenze del dominio del linguaggio formale e la capacità di ragionamento nella comprensione dei problemi in linguaggio naturale e nell'allineamento informale-formale. Senza la prima, un modello non può identificare gli oggetti formali corretti; senza la seconda, fatica a interpretare i contesti del mondo reale e a mapparli con precisione in espressioni formali. Per colmare queste lacune, introduciamo ThinkingF, una pipeline di sintesi dei dati e di addestramento che migliora entrambe le abilità. In primo luogo, costruiamo due dataset: uno distillando e selezionando esempi su larga scala ricchi di conoscenze formali, e un altro generando traiettorie di ragionamento da informale a formale guidate da modelli progettati da esperti. Applichiamo quindi SFT e RLVR con questi dataset per fondere e affinare ulteriormente le due abilità. I modelli risultanti da 7B e 32B mostrano sia una conoscenza formale completa che un forte ragionamento da informale a formale. In particolare, StepFun-Formalizer-32B raggiunge punteggi SOTA BEq@1 del 40,5% su FormalMATH-Lite e del 26,7% su ProverBench, superando tutti i modelli general-purpose e specializzati precedenti.

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.