StepFun-Formalizador: Desbloqueando el Potencial de Autoformalización de los LLM mediante la Fusión de Conocimiento y Razonamiento

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

August 6, 2025

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

cs.AI

Resumen

La autoformalización tiene como objetivo traducir enunciados matemáticos en lenguaje natural a un lenguaje formal. Si bien los LLM han acelerado el progreso en esta área, los métodos existentes aún presentan una baja precisión. Identificamos dos habilidades clave para una autoformalización efectiva: un dominio exhaustivo del conocimiento del lenguaje formal y la capacidad de razonamiento para comprender problemas en lenguaje natural y alinear lo informal con lo formal. Sin la primera, un modelo no puede identificar los objetos formales correctos; sin la segunda, tiene dificultades para interpretar contextos del mundo real y mapearlos con precisión en expresiones formales. Para abordar estas brechas, presentamos ThinkingF, una canalización de síntesis de datos y entrenamiento que mejora ambas habilidades. Primero, construimos dos conjuntos de datos: uno mediante la destilación y selección de ejemplos a gran escala ricos en conocimiento formal, y otro generando trayectorias de razonamiento de informal a formal guiadas por plantillas diseñadas por expertos. Luego, aplicamos SFT y RLVR con estos conjuntos de datos para fusionar y refinar aún más las dos habilidades. Los modelos resultantes de 7B y 32B exhiben tanto un conocimiento formal exhaustivo como un fuerte razonamiento de informal a formal. En particular, StepFun-Formalizer-32B alcanza puntajes SOTA BEq@1 de 40.5% en FormalMATH-Lite y 26.7% en ProverBench, superando a todos los modelos generales y especializados anteriores.

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.