ReForm: Reflectieve Autoformalisering met Prospectieve Gebonden Sequentieoptimalisatie

Samenvatting

Autoformalisering, het vertalen van natuurlijketaalwiskunde naar machine-verifieerbare formele uitspraken, is cruciaal voor het gebruik van formeel wiskundig redeneren om wiskundeproblemen opgelost in natuurlijke taal op te lossen. Hoewel grote taalmodellen syntactisch correcte formele uitspraken kunnen genereren, slagen zij er vaak niet in de semantische intentie van het oorspronkelijke probleem te behouden. Deze beperking ontstaat doordat LLM-benaderingen autoformalisering behandelen als een simplistische vertaaltaak, waarbij mechanismen voor zelfreflectie en iteratieve verfijning ontbreken die menselijke experts van nature toepassen. Om deze problemen aan te pakken, stellen wij ReForm voor, een reflectieve autoformaliseringmethode die semantische consistentie-evaluatie nauw integreert in het autoformaliseringproces. Hierdoor kan het model iteratief formele uitspraken genereren, de semantische trouw ervan beoordelen en geïdentificeerde fouten zelf corrigeren door progressieve verfijning. Om dit reflectieve model effectief te trainen, introduceren wij Prospective Bounded Sequence Optimization (PBSO), dat verschillende beloningen gebruikt op verschillende sequentieposities om ervoor te zorgen dat het model zowel accurate autoformalisering als correcte semantische validaties ontwikkelt, waardoor oppervlakkige kritieken worden voorkomen die het doel van reflectie zouden ondermijnen. Uitgebreide experimenten over vier autoformaliseringbenchmarks tonen aan dat ReForm een gemiddelde verbetering van 17,2 procentpunten bereikt ten opzichte van de sterkste baselines. Om de betrouwbaarheid van de evaluatie verder te waarborgen, introduceren wij ConsistencyCheck, een benchmark van 859 door experts geannoteerde items die niet alleen LLM's als beoordelaars valideert, maar ook aantoont dat autoformalisering inherent moeilijk is: zelfs menselijke experts produceren semantische fouten in tot 38,5% van de gevallen.

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: Reflectieve Autoformalisering met Prospectieve Gebonden Sequentieoptimalisatie

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

Samenvatting

Support