ReForm : Autoformalisation Réflexive avec Optimisation de Séquence Bornée Prospective

papers.abstract

L'autoformalisation, qui traduit les mathématiques en langage naturel en énoncés formels vérifiables par machine, est essentielle pour utiliser le raisonnement mathématique formel afin de résoudre des problèmes mathématiques énoncés en langage naturel. Bien que les grands modèles de langage puissent générer des énoncés formels syntaxiquement corrects, ils échouent souvent à préserver l'intention sémantique originale du problème. Cette limitation découle du fait que les approches par LLM traitent l'autoformalisation comme une tâche de traduction simpliste, dépourvue des mécanismes d'autoréflexion et de raffinement itératif qu'emploient naturellement les experts humains. Pour résoudre ces problèmes, nous proposons ReForm, une méthode d'Autoformalisation Réflexive qui intègre étroitement l'évaluation de la cohérence sémantique dans le processus d'autoformalisation. Cela permet au modèle de générer itérativement des énoncés formels, d'évaluer leur fidélité sémantique et de s'auto-corriger des erreurs identifiées via un raffinement progressif. Pour entraîner efficacement ce modèle réflexif, nous introduisons l'Optimisation de Séquence à Borne Prospective (PBSO), qui utilise des récompenses différentes à différentes positions de la séquence pour garantir que le modèle développe à la fois une autoformalisation précise et des validations sémantiques correctes, évitant ainsi les critiques superficielles qui compromettraient l'objectif de la réflexion. Des expériences approfondies sur quatre benchmarks d'autoformalisation démontrent que ReForm obtient une amélioration moyenne de 17,2 points de pourcentage par rapport aux lignes de base les plus solides. Pour garantir davantage la fiabilité de l'évaluation, nous introduisons ConsistencyCheck, un benchmark de 859 éléments annotés par des experts qui valide non seulement les LLMs en tant qu'évaluateurs, mais révèle aussi que l'autoformalisation est intrinsèquement difficile : même les experts humains produisent des erreurs sémantiques dans jusqu'à 38,5 % des cas.

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 : Autoformalisation Réflexive avec Optimisation de Séquence Bornée Prospective

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

papers.abstract

Support