ReForm: Autoformalização Reflexiva com Otimização Prospectiva de Sequência Limitada

Resumo

A autoformalização, que traduz matemática em linguagem natural para declarações formais verificáveis por máquina, é crucial para utilizar o raciocínio matemático formal na resolução de problemas matemáticos enunciados em linguagem natural. Embora os Grandes Modelos de Linguagem (LLMs) possam gerar declarações formais sintaticamente corretas, frequentemente falham em preservar a intenção semântica original do problema. Esta limitação surge porque as abordagens baseadas em LLM tratam a autoformalização como uma tarefa de tradução simplista, carecendo dos mecanismos de autorreflexão e refinamento iterativo que os especialistas humanos empregam naturalmente. Para resolver estas questões, propomos o ReForm, um método de Autoformalização Reflexiva que integra firmemente a avaliação da consistência semântica no processo de autoformalização. Isto permite que o modelo gere iterativamente declarações formais, avalie a sua fidelidade semântica e se autocorrija de erros identificados através de um refinamento progressivo. Para treinar eficazmente este modelo reflexivo, introduzimos a Optimização de Sequência Limitada e Prospetiva (PBSO), que emprega recompensas diferentes em diferentes posições da sequência para garantir que o modelo desenvolva tanto uma autoformalização precisa como validações semânticas corretas, prevenindo críticas superficiais que prejudicariam o propósito da reflexão. Extensos experimentos em quatro benchmarks de autoformalização demonstram que o ReForm alcança uma melhoria média de 17,2 pontos percentuais sobre as linhas de base mais fortes. Para garantir ainda mais a fiabilidade da avaliação, introduzimos o ConsistencyCheck, um benchmark de 859 itens anotados por especialistas que não só valida os LLMs como juízes, mas também revela que a autoformalização é intrinsecamente difícil: mesmo os especialistas humanos produzem erros semânticos em até 38,5% dos casos.

English

Autoformalization, which translates natural language mathematics into machine-verifiable formal statements, is critical for using formal mathematical reasoning to solve math problems stated in natural language. While Large Language Models can generate syntactically correct formal statements, they often fail to preserve the original problem's semantic intent. This limitation arises from the LLM approaches' treating autoformalization as a simplistic translation task which lacks mechanisms for self-reflection and iterative refinement that human experts naturally employ. To address these issues, we propose ReForm, a Reflective Autoformalization method that tightly integrates semantic consistency evaluation into the autoformalization process. This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors through progressive refinement. To effectively train this reflective model, we introduce Prospective Bounded Sequence Optimization (PBSO), which employs different rewards at different sequence positions to ensure that the model develops both accurate autoformalization and correct semantic validations, preventing superficial critiques that would undermine the purpose of reflection. Extensive experiments across four autoformalization benchmarks demonstrate that ReForm achieves an average improvement of 17.2 percentage points over the strongest baselines. To further ensure evaluation reliability, we introduce ConsistencyCheck, a benchmark of 859 expert-annotated items that not only validates LLMs as judges but also reveals that autoformalization is inherently difficult: even human experts produce semantic errors in up to 38.5% of cases.

ReForm: Autoformalização Reflexiva com Otimização Prospectiva de Sequência Limitada

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

Resumo

Support