ReForm: Autoformalización Reflexiva con Optimización de Secuencia Acotada Prospectiva

Resumen

La autoformalización, que traduce matemáticas en lenguaje natural a enunciados formales verificables por máquina, es crucial para utilizar el razonamiento matemático formal con el fin de resolver problemas matemáticos planteados en lenguaje natural. Si bien los Modelos de Lenguaje a Gran Escala pueden generar enunciados formalmente correctos, a menudo no logran preservar la intención semántica original del problema. Esta limitación surge porque los enfoques basados en LLM tratan la autoformalización como una tarea de traducción simplista, carente de los mecanismos de autorreflexión y refinamiento iterativo que los expertos humanos emplean naturalmente. Para abordar estos problemas, proponemos ReForm, un método de Autoformalización Reflexiva que integra estrechamente la evaluación de consistencia semántica en el proceso de autoformalización. Esto permite al modelo generar enunciados formales de manera iterativa, evaluar su fidelidad semántica y autocorregir los errores identificados mediante un refinamiento progresivo. Para entrenar eficazmente este modelo reflexivo, introducimos la Optimización de Secuencia con Límite Prospectivo (PBSO), que emplea diferentes recompensas en distintas posiciones de la secuencia para garantizar que el modelo desarrolle tanto una autoformalización precisa como validaciones semánticas correctas, evitando críticas superficiales que socavarían el propósito de la reflexión. Experimentos exhaustivos en cuatro benchmarks de autoformalización demuestran que ReForm logra una mejora promedio de 17.2 puntos porcentuales sobre las líneas base más sólidas. Para garantizar aún más la fiabilidad de la evaluación, introducimos ConsistencyCheck, un benchmark de 859 ítems anotados por expertos que no solo valida a los LLMs como evaluadores, sino que también revela que la autoformalización es inherentemente difícil: incluso los expertos humanos producen errores semánticos en hasta el 38.5% de los 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: Autoformalización Reflexiva con Optimización de Secuencia Acotada Prospectiva

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

Resumen

Support