StepFun-Formalizer: Freisetzung des Autoformalierungspotenzials von LLMs durch Wissens-Reasoning-Fusion

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

Autoformalisierung zielt darauf ab, mathematische Aussagen in natürlicher Sprache in eine formale Sprache zu übersetzen. Obwohl LLMs den Fortschritt in diesem Bereich beschleunigt haben, leiden bestehende Methoden immer noch unter geringer Genauigkeit. Wir identifizieren zwei Schlüsselfähigkeiten für eine effektive Autoformalierung: umfassende Beherrschung des Domänenwissens der formalen Sprache und die Fähigkeit, natürliche Sprache zu verstehen und informelle mit formalen Aussagen in Einklang zu bringen. Ohne erstere kann ein Modell die korrekten formalen Objekte nicht identifizieren; ohne letztere hat es Schwierigkeiten, reale Kontexte zu interpretieren und sie präzise in formale Ausdrücke abzubilden. Um diese Lücken zu schließen, stellen wir ThinkingF vor, eine Pipeline zur Datensynthese und zum Training, die beide Fähigkeiten verbessert. Zunächst erstellen wir zwei Datensätze: einen durch Destillation und Auswahl groß angelegter Beispiele, die reich an formalem Wissen sind, und einen anderen durch die Generierung von informell-zu-formal-Schlussfolgerungspfaden, die von Experten entworfenen Vorlagen folgen. Anschließend wenden wir SFT und RLVR mit diesen Datensätzen an, um beide Fähigkeiten weiter zu verschmelzen und zu verfeinern. Die resultierenden 7B- und 32B-Modelle zeigen sowohl umfassendes formales Wissen als auch starke informell-zu-formal-Schlussfolgerungsfähigkeiten. Bemerkenswerterweise erreicht StepFun-Formalizer-32B SOTA BEq@1-Werte von 40,5 % auf FormalMATH-Lite und 26,7 % auf ProverBench und übertrifft damit alle bisherigen allgemeinen und spezialisierten Modelle.

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.