ReForm: Рефлексивное автоформализация с перспективной оптимизацией ограниченных последовательностей

Аннотация

Автоформализация — процесс преобразования математических утверждений на естественном языке в машиночитаемые формальные утверждения — играет ключевую роль для применения формальных математических рассуждений к решению задач, сформулированных на естественном языке. Хотя большие языковые модели способны генерировать синтаксически корректные формальные утверждения, они часто не сохраняют смысловое содержание исходной задачи. Это ограничение возникает из-за того, что подходы на основе LLM рассматривают автоформализацию как упрощённую задачу перевода, в которой отсутствуют механизмы саморефлексии и итеративного уточнения, естественным образом используемые экспертами-людьми. Для решения этих проблем мы предлагаем ReForm — рефлексивный метод автоформализации, который тесно интегрирует оценку семантической согласованности в процесс формализации. Это позволяет модели итеративно генерировать формальные утверждения, оценивать их семантическую точность и самостоятельно исправлять выявленные ошибки путём прогрессивного улучшения. Для эффективного обучения этой рефлексивной модели мы вводим метод оптимизации последовательностей с перспективным ограничением (Prospective Bounded Sequence Optimization, PBSO), который использует различные функции вознаграждения на разных позициях последовательности, чтобы гарантировать, что модель развивает как точную автоформализацию, так и корректные семантические проверки, предотвращая поверхностную критику, которая подрывает цель рефлексии. Масштабные эксперименты на четырёх бенчмарках автоформализации демонстрируют, что ReForm достигает среднего улучшения на 17.2 процентных пункта по сравнению с сильнейшими базовыми методами. Для дальнейшего обеспечения надёжности оценки мы представляем ConsistencyCheck — бенчмарк из 859 элементов, размеченных экспертами, который не только валидирует LLM в качестве судей, но и показывает, что автоформализация сама по себе является сложной задачей: даже эксперты-люди допускают семантические ошибки вплоть до 38.5% случаев.

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: Рефлексивное автоформализация с перспективной оптимизацией ограниченных последовательностей

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

Аннотация

Support