ReForm: Autoformalizzazione Riflessiva con Ottimizzazione Prospettica di Sequenze Limitate

Abstract

L'autoformalizzazione, che traduce la matematica in linguaggio naturale in enunciati formali verificabili dalla macchina, è fondamentale per utilizzare il ragionamento matematico formale nella risoluzione di problemi matematici espressi in linguaggio naturale. Sebbene i Modelli Linguistici di Grande Dimensione (LLM) possano generare enunciati formalmente corretti, spesso non riescono a preservare l'intento semantico originale del problema. Questa limitazione deriva dal fatto che gli approcci basati su LLM trattano l'autoformalizzazione come un semplice compito di traduzione, privo dei meccanismi di autoriflessione e raffinamento iterativo che gli esperti umani impiegano naturalmente. Per affrontare questi problemi, proponiamo ReForm, un metodo di Autoformalizzazione Riflessiva che integra strettamente la valutazione della coerenza semantica nel processo di autoformalizzazione. Ciò consente al modello di generare iterativamente enunciati formali, valutarne la fedeltà semantica e autocorreggere gli errori identificati attraverso un raffinamento progressivo. Per addestrare efficacemente questo modello riflessivo, introduciamo l'Ottimizzazione di Sequenza con Limite Prospettico (PBSO), che utilizza ricompense diverse in diverse posizioni della sequenza per garantire che il modello sviluppi sia un'autoformalizzazione accurata che validazioni semantiche corrette, prevenendo critiche superficiali che minerebbero lo scopo della riflessione. Esperimenti estesi su quattro benchmark di autoformalizzazione dimostrano che ReForm ottiene un miglioramento medio di 17,2 punti percentuali rispetto ai baseline più robusti. Per garantire ulteriormente l'affidabilità della valutazione, introduciamo ConsistencyCheck, un benchmark di 859 elementi annotati da esperti che non solo convalida gli LLM come giudici, ma rivela anche che l'autoformalizzazione è intrinsecamente difficile: persino esperti umani producono errori semantici fino al 38,5% dei casi.

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: Autoformalizzazione Riflessiva con Ottimizzazione Prospettica di Sequenze Limitate

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

Abstract

Support