StepFun-Formalizer: Desbloqueando o Potencial de Autoformalização de LLMs por meio da Fusão de Conhecimento e Raciocínio
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
Resumo
A autoformalização visa traduzir declarações matemáticas em linguagem natural para uma linguagem formal. Embora os LLMs tenham acelerado o progresso nessa área, os métodos existentes ainda sofrem com baixa precisão. Identificamos duas habilidades essenciais para uma autoformalização eficaz: domínio abrangente do conhecimento do domínio da linguagem formal e capacidade de raciocínio para compreensão de problemas em linguagem natural e alinhamento informal-formal. Sem a primeira, um modelo não consegue identificar os objetos formais corretos; sem a segunda, ele tem dificuldade em interpretar contextos do mundo real e mapeá-los com precisão em expressões formais. Para abordar essas lacunas, introduzimos o ThinkingF, um pipeline de síntese de dados e treinamento que melhora ambas as habilidades. Primeiro, construímos dois conjuntos de dados: um por destilação e seleção de exemplos em larga escala ricos em conhecimento formal, e outro pela geração de trajetórias de raciocínio informal-formal guiadas por modelos projetados por especialistas. Em seguida, aplicamos SFT e RLVR com esses conjuntos de dados para fundir e refinar ainda mais as duas habilidades. Os modelos resultantes de 7B e 32B exibem tanto conhecimento formal abrangente quanto forte raciocínio informal-formal. Notavelmente, o StepFun-Formalizer-32B alcança pontuações SOTA BEq@1 de 40,5% no FormalMATH-Lite e 26,7% no ProverBench, superando todos os modelos de propósito geral e 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.