Guoxin Chen Jing Wu Xinjie Chen Wayne Xin Zhao Ruihua Song Chengxi Li Kai Fan Dayiheng Liu Minpeng Liao

Abstract

Autoformalisierung, also die Übersetzung von mathematischen Aussagen in natürlicher Sprache in maschinenprüfbar formale Aussagen, ist entscheidend für die Anwendung formaler mathematischer Schlussfolgerungen zur Lösung von in natürlicher Sprache formulierten mathematischen Problemen. Obwohl große Sprachmodelle syntaktisch korrekte formale Aussagen generieren können, verfehlen sie oft den ursprünglichen semantischen Gehalt des Problems. Dieser Mangel resultiert daraus, dass herkömmliche Ansätze mit großen Sprachmodellen die Autoformalisierung als eine vereinfachte Übersetzungsaufgabe betrachten, die fehlende Mechanismen für Selbstreflexion und iterative Verbesserung aufweist – Fähigkeiten, die menschliche Experten nahtlos einsetzen. Um diese Probleme zu beheben, schlagen wir ReForm vor, eine reflektierende Autoformalisierungsmethode, die die Bewertung der semantischen Konsistenz eng in den Prozess der Autoformalisierung integriert. Dadurch kann das Modell formale Aussagen iterativ generieren, ihre semantische Treue bewerten und identifizierte Fehler durch schrittweise Verbesserung selbst korrigieren. Um dieses reflektierende Modell effektiv zu trainieren, führen wir Prospective Bounded Sequence Optimization (PBSO) ein, das an verschiedenen Positionen innerhalb einer Sequenz unterschiedliche Belohnungen verwendet, um sicherzustellen, dass das Modell sowohl eine präzise Autoformalisierung als auch korrekte semantische Validierungen erlernt und oberflächliche Kritik vermeidet, die dem Ziel der Reflexion widerspricht. Ausführliche Experimente an vier Autoformalisierungs-Benchmarks zeigen, dass ReForm im Durchschnitt eine Verbesserung um 17,2 Prozentpunkte gegenüber den stärksten Baselines erreicht. Um die Zuverlässigkeit der Evaluation weiter zu sichern, führen wir ConsistencyCheck ein, ein Benchmark mit 859 von Experten annotierten Beispielen, der nicht nur die Eignung von Sprachmodellen als Beurteiler validiert, sondern auch aufzeigt, dass die Autoformalisierung inhärent schwierig ist: Selbst menschliche Experten begehen in bis zu 38,5 % der Fälle semantische Fehler.