ReForm: Reflektierende Autoformalisierung mit prospektiver optimierter Sequenzbegrenzung

papers.abstract

Autoformalisierung, die natürliche mathematische Sprache in maschinenüberprüfbare formale Aussagen übersetzt, ist entscheidend für den Einsatz formalen mathematischen Schließens zur Lösung natürlichsprachlich formulierter Mathematikprobleme. Obwohl große Sprachmodelle syntaktisch korrekte formale Aussagen generieren können, bewahren sie häufig nicht die semantische Intention des ursprünglichen Problems. Diese Einschränkung ergibt sich daraus, dass LLM-Ansätze Autoformalisierung als simplistische Übersetzungsaufgabe behandeln, wobei Mechanismen zur Selbstreflexion und iterativen Verbesserung fehlen, die menschliche Experten natürlicherweise anwenden. Um diese Probleme zu adressieren, schlagen wir ReForm vor, eine reflexive Autoformalisierungsmethode, die semantische Konsistenzbewertung eng in den Autoformalisierungsprozess integriert. Dies ermöglicht dem Modell, iterative formale Aussagen zu generieren, deren semantische Treue zu bewerten und identifizierte Fehler durch progressive Verfeinerung selbst zu korrigieren. Um dieses reflexive Modell effektiv zu trainieren, führen wir Prospective Bounded Sequence Optimization (PBSO) ein, das verschiedene Belohnungen an verschiedenen Sequenzpositionen verwendet, um sicherzustellen, dass das Modell sowohl präzise Autoformalisierung als auch korrekte semantische Validierungen entwickelt und oberflächliche Kritiken verhindert, die den Zweck der Reflexion untergraben würden. Umfangreiche Experimente über vier Autoformalisierungs-Benchmarks demonstrieren, dass ReForm eine durchschnittliche Verbesserung von 17,2 Prozentpunkten gegenüber den stärksten Baseline-Modellen erzielt. Um die Bewertungszuverlässigkeit weiter zu gewährleisten, führen wir ConsistencyCheck ein, einen Benchmark mit 859 expertenannotierten Einträgen, der nicht nur LLMs als Richter validiert, sondern auch zeigt, dass Autoformalisierung inhärent schwierig ist: Selbst menschliche Experten produzieren in bis zu 38,5 % der Fälle semantische Fehler.

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: Reflektierende Autoformalisierung mit prospektiver optimierter Sequenzbegrenzung

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

papers.abstract

Support