StepFun-Formalizer: Het ontgrendelen van het autoformaliseringspotentieel van LLM's door kennis-redeneerfusie

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

August 6, 2025

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

cs.AI

Samenvatting

Autoformalizatie heeft als doel om wiskundige uitspraken in natuurlijke taal te vertalen naar een formele taal. Hoewel LLM's de vooruitgang op dit gebied hebben versneld, lijden bestaande methoden nog steeds aan een lage nauwkeurigheid. Wij identificeren twee cruciale vaardigheden voor effectieve autoformalizatie: een uitgebreide beheersing van domeinkennis in formele taal, en het redeneervermogen om natuurlijke taalproblemen te begrijpen en informele-formele afstemming te realiseren. Zonder de eerste kan een model de juiste formele objecten niet identificeren; zonder de tweede heeft het moeite om real-world contexten te interpreteren en deze precies in formele uitdrukkingen om te zetten. Om deze tekortkomingen aan te pakken, introduceren we ThinkingF, een gegevenssynthese- en trainingspijplijn die beide vaardigheden verbetert. Eerst construeren we twee datasets: één door grootschalige voorbeelden die rijk zijn aan formele kennis te destilleren en te selecteren, en een andere door informele-naar-formele redeneertrajecten te genereren die worden geleid door door experts ontworpen sjablonen. Vervolgens passen we SFT en RLVR toe met deze datasets om de twee vaardigheden verder te integreren en te verfijnen. De resulterende 7B- en 32B-modellen vertonen zowel uitgebreide formele kennis als sterk informele-naar-formeel redeneervermogen. Opmerkelijk is dat StepFun-Formalizer-32B SOTA BEq@1-scores behaalt van 40,5% op FormalMATH-Lite en 26,7% op ProverBench, waarmee het alle voorgaande algemene en gespecialiseerde modellen overtreft.

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.