PaperlayerView exact revision on arXiv

Source-linked AI summary

ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

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

arXiv:2510.24592v3cs.CL

TL;DR

Autoformalization models often generate syntactically correct statements that fail to preserve mathematical intent. ReForm uses iterative semantic self-validation trained with PBSO, achieving a 22.6-percentage-point average improvement across four benchmarks while exposing substantial difficulty even for human experts.

  • Problem

    LLMs often produce Lean-verifiable formal statements without faithfully preserving the original problem’s semantic intent.

  • Method

    ReForm iteratively generates formal statements, critiques their semantic fidelity, and refines them using PBSO’s position-specific heterogeneous rewards.

  • Results

    22.6 percentage points: ReForm improves over the strongest baselines across four autoformalization benchmarks.

  • Takeaways & Limitations

    ConsistencyCheck broadens evaluation beyond model performance by testing LLM judges and documenting the difficulty of semantic formalization.

  • Takeaways & Limitations

    Human-written formalizations contain semantic errors in 16.4% of miniF2F items and 38.5% of ProofNet items.

Abstract

from arXiv · show

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 22.6 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.

1 INTRODUCTION

Autoformalization systems often produce syntactically valid statements that fail to preserve mathematical meaning. REFORM addresses this gap through iterative semantic self-validation, PBSO training, and evaluation across four benchmarks.

  • REFORM: REFORM reframes autoformalization as iterative generation, semantic evaluation, and self-correction rather than one-pass translation.The loop is designed to detect and correct semantic discrepancies during generation.
  • PBSO: PBSO assigns final-task rewards to formalization correctness and intermediate rewards to semantic-validation quality.This heterogeneous supervision targets both accurate final statements and reliable critiques.
  • Evaluation: ConsistencyCheck contains 859 expert-annotated items for assessing the reliability of LLM-based semantic-consistency judges.Its analysis addresses whether automated evaluators reliably determine if formal statements preserve problem intent.
  • Results: 22.6 percentage points: REFORM improves over the strongest baselines across four challenging autoformalization benchmarks.The contribution summary reports this average improvement while maintaining computational efficiency.

2 RELATED WORKS

Related work shows that formal reasoning progress has not eliminated semantic errors in autoformalization. Existing reinforcement-learning approaches also rely mainly on terminal rewards, leaving intermediate validation quality insufficiently supervised.

  • Autoformalization: Autoformalization research has improved syntactic correctness, but recent studies identify persistent weaknesses in semantic fidelity.The central distinction is between producing machine-acceptable code and preserving the original problem’s meaning.
  • Reinforcement Learning: Terminal-only reinforcement-learning rewards provide little supervision for intermediate validation in multi-objective reflective tasks.This can lead to superficial or hallucinated critiques that undermine self-correction.

3 METHODOLOGY

REFORM implements autoformalization as a history-aware refinement loop that alternates statement generation and semantic critique. Heterogeneous rewards and prospective bounded returns jointly train final correctness and intermediate validation quality.

  • 3.1 REFLECTIVE AUTOFORMALIZATION PARADIGM: REFORM maintains previous statement–critique pairs so later formalizations can address identified semantic errors.Each iteration generates a statement conditioned on the question and accumulated history, then produces a critique.
  • 3.1 REFLECTIVE AUTOFORMALIZATION PARADIGM: The self-correction loop continues until critique indicates satisfactory semantic fidelity, after which the model produces the final statement.The implementation unfolds as one continuous autoregressive sequence rather than separate forward passes.
  • 3.1 REFLECTIVE AUTOFORMALIZATION PARADIGM: REFORM interweaves generation and self-validation so both capabilities can reinforce one another while targeting syntactically valid and semantically faithful statements.The method contrasts with one-pass approaches by making semantic critique part of refinement.
  • 3.2 PROSPECTIVE BOUNDED SEQUENCE OPTIMIZATION: PBSO addresses the credit-assignment problem created by jointly optimizing final formalization correctness and intermediate critique quality.Terminal success alone cannot explicitly supervise whether critiques accurately diagnose semantic issues.
  • 3.2.1 HETEROGENEOUS REWARD MECHANISM: Task rewards require final statements to be syntactically and semantically correct, while auxiliary rewards directly supervise each semantic critique.The two signals provide complementary supervision for outputs and the validation process.
  • 3.2.2 PROSPECTIVE BOUNDED RETURN: Prospective bounded returns accumulate future task and critique rewards for each iteration while clipping values to the reward range.This provides fine-grained credit assignment and prevents gradient instability from unbounded accumulation.

4 EXPERIMENT

Across four autoformalization benchmarks, REFORM improves semantic consistency over strong baselines, with gains especially pronounced on harder problems. Additional analyses examine ablations, training dynamics, evaluator reliability, human evaluation, and robustness across evaluators.

  • 4.2 MAIN RESULTS: +14.8pp semantic consistency and +8.2pp syntactic correctness over Goedel-FormalizerV2-8B, with REFORM-8B also exceeding the 32B model by +14.2pp in semantic consistency.Gains reached +18.3pp on ProofNet, +14.4pp on PutnamBench, and +20.0pp on AIME2025 compared with Goedel-V2-8B.
  • 4.2 MAIN RESULTS: REFORM’s semantic gains exceed syntactic improvements by 2-3× on harder benchmarks, addressing the gap between Lean-compilable statements and faithful formalizations.Baseline systems commonly produce syntactically correct code without preserving the original problem’s semantic intent.
  • 4.3 ABLATION STUDIES: Removing bounded clipping severely degrades harder benchmarks, while auxiliary validation rewards become more important as problem complexity increases.RL training consistently improves performance across datasets, with larger gains on harder problems than SFT.
  • 4.4 TRAINING DYNAMICS OF PBSO: PBSO training rewards rose from 0.30 to 0.47 over 400 steps while response length expanded from 2,300 to 4,800 tokens, indicating stable optimization and emergent reflective behavior.The response-length increase was attributed to heterogeneous reward signals without explicit length supervision.
  • 4.5 RELIABILITY OF SEMANTIC CONSISTENCY EVALUATION: ConsistencyCheck contains 859 expert-annotated items, while human formalizations contain semantic errors in 16.4% of miniF2F and 38.5% of ProofNet cases.These findings establish evaluation difficulty and reveal fallibility in existing expert-written formalizations.
  • 4.6 ROBUSTNESS ANALYSIS ON MAIN RESULT EVALUATED BY CRITICLEAN-14B: Under CriticLean evaluation, REFORM-8B improves over Goedel-V2-8B by +18.0pp on average, including +33.3pp on AIME2025 and +18.8pp on PutnamBench.REFORM-8B reaches 70.3% average semantic consistency under CriticLean, with rankings remaining largely consistent across evaluators.

5 CONCLUSION

The paper introduces REFORM, a reflective autoformalization paradigm trained with Prospective Bounded Sequence Optimization to jointly improve formalizations and semantic critiques. Experiments show effectiveness across four benchmarks, while ConsistencyCheck highlights the difficulty of autoformalization for humans and LLM judges.

  • REFORM combines iterative semantic self-validation with Prospective Bounded Sequence Optimization to optimize final formalizations and intermediate critiques.The approach uses heterogeneous rewards and prospective bounded returns to prevent degenerate or hallucinated self-validations.
  • 22.6% average improvement across four benchmarks demonstrates REFORM’s effectiveness.
  • ConsistencyCheck shows that autoformalization challenges human experts while supporting the reliability of LLM-based evaluation metrics.

ETHICS STATEMENT

The ethics statement addresses responsible development, annotation labor, intellectual property, and possible effects of automating mathematical formalization. It emphasizes fair expert compensation, proper dataset attribution, and potential augmentation of human mathematical work.

  • ConsistencyCheck uses expert annotation with fair compensation and reasonable working conditions.
  • The benchmark builds on miniF2F and ProofNet under their licenses with attribution to the original resources.
  • The work acknowledges that automating mathematical formalization could reduce demand for some mathematical verification work.
  • The authors expect the technology primarily to augment mathematicians and support higher-level creative and conceptual work.

A MORE IMPLEMENTATION DETAILS

This section indicates that implementation details are provided comprehensively, with additional intricate information deferred to the supplementary materials.

  • Implementation details are presented in the section, with additional insights and intricacies available in supplementary materials.

A.1 IMPLEMENTATION DETAILS

The implementation trains REFORM through supervised reflective trajectories and reinforcement learning, using iterative validation and refinement to construct training data. The pipeline includes compiler and semantic checks, stratified RL data selection, and specified inference settings.

  • Implementation Configuration: Tables 5 and 6 summarize key hyperparameters for supervised fine-tuning and reinforcement learning, respectively.
  • Supervised Fine-tuning Phase: The supervised pipeline generates formalizations, checks Lean4 compilation and semantic consistency, then refines inconsistent statements for up to three rounds.
  • Supervised Fine-tuning Phase: 447,508 training trajectories provide supervision for reflective autoformalization, with 83.1% of problems resolved within one iteration.
  • Reinforcement Learning Phase: The RL dataset contains 2048 stratified items selected from eight sampled formalizations per problem using compiler and semantic checks.
  • Inference Phase: Inference uses temperature 0.6, top-p 0.95, and a maximum generation length of 40,960 tokens.

A.2 IMPACT OF RL TRAINING ON ITERATIVE REFINEMENT BEHAVIOR

RL training changes ReForm’s refinement behavior from mostly one-step termination to exploration of additional iteration depths. The authors interpret this pattern as evidence that heterogeneous rewards preserve self-validation while encouraging productive iteration.

  • A.2 IMPACT OF RL TRAINING ON ITERATIVE REFINEMENT BEHAVIOR: Figure 4 compares iteration distributions for REFORM-SFT and RL across four benchmarks to assess changes in refinement behavior.The analysis reports striking behavioral changes after RL training.
  • A.2 IMPACT OF RL TRAINING ON ITERATIVE REFINEMENT BEHAVIOR: 0.7% and 0.3% of REFORM-RL samples extend to 4 and 5 iterations, respectively, beyond depths seen during SFT training.REFORM-SFT has 86.3% of samples terminate after one iteration, while remaining samples use 2–3 iterations.
  • A.2 IMPACT OF RL TRAINING ON ITERATIVE REFINEMENT BEHAVIOR: The heterogeneous reward mechanism is reported to prevent degeneration of self-validation while encouraging productive iteration when needed.The authors connect this behavior to improved semantic consistency through iterative self-correction.

B THE CONSISTENCYCHECK BENCHMARK

ConsistencyCheck evaluates semantic consistency with expert annotations and exposes errors in formalizations, including examples from ProofNet and miniF2F. Its annotation process uses expert comparison, multi-annotator review, and senior adjudication.

  • B THE CONSISTENCYCHECK BENCHMARK: Each statement receives two independent annotations followed by review from a third senior annotator to resolve discrepancies and produce the final judgment.The annotation team comprises researchers with mathematics and Lean expertise, supported by dedicated training and standardized handling of edge cases.
  • B THE CONSISTENCYCHECK BENCHMARK: ConsistencyCheck uses expert annotators to compare natural-language problems with machine-verifiable formal statements and judge semantic fidelity.The benchmark draws items from miniF2F and ProofNet and presents them in anonymized form.
  • B THE CONSISTENCYCHECK BENCHMARK: The benchmark identifies semantic errors such as changing a constant term or replacing a degree bound of ≤80 with <80.These discrepancies make the formalization mathematically inequivalent to the original statement.
  • B THE CONSISTENCYCHECK BENCHMARK: LLMs are evaluated on whether formal statements preserve the original problem’s intent using the benchmark’s semantic-consistency assessment procedure.The benchmark is used to investigate model performance in semantic consistency evaluation.
  • B THE CONSISTENCYCHECK BENCHMARK: MiniF2F examples include problems asking for a numerical result, such as finding ⌊100r⌋, alongside their formal statements and supporting context.The benchmark includes representative ProofNet and miniF2F examples for consistency assessment.

C CASE STUDY OF OUR REFORM

The ReForm case study shows a model detecting that an initial Lean statement captures a minimum-value inequality but omits the minimizer, then correcting the statement through self-validation. The revised formalization states both global minimality and uniqueness.

  • C CASE STUDY OF OUR REFORM: The case study describes ReForm as generating a formalization, performing structured semantic self-validation, and using the critique to produce a corrected statement.The validation checks variable types, constraints, logical relationships, completeness, and alignment with intent.
  • C CASE STUDY OF OUR REFORM: The case study includes successive Lean attempts, revisions, explicit casting considerations, and a final theorem expressing the minimum and uniqueness conditions.The displayed code and discussion illustrate the progression from the incomplete first statement to the refined formulation.
  • C CASE STUDY OF OUR REFORM: The example formalizes that 7 minimizes x² − 14x + 3, whose minimum value is −46.The algebraic analysis identifies the minimum at 7 and supports the corresponding Lean relationship.
  • C CASE STUDY OF OUR REFORM: The initial theorem is judged incorrect because it asserts f(7) ≤ f(x) without explicitly identifying x=7 as the minimizer.The critique distinguishes capturing the inequality from stating the minimizer and its uniqueness.
  • C CASE STUDY OF OUR REFORM: The model’s second iteration defines f : R → R and states both global minimality at 7 and uniqueness of the minimizer.The subsequent validation reports that the function, domain, quantifiers, and logical claims align with the problem.

D PROMPT

The prompts define a reflective workflow that generates Lean statements, evaluates their semantic consistency, and revises failed formalizations using prior critiques. They specify structured comparison criteria, strict judgments, and consistency outputs used in training and evaluation.

  • D.1 INSTRUCTION FOR COLLECTING SFT TRAJECTORIES: The SFT trajectory prompt converts a natural-language problem into Lean 4 while conditioning revisions on previous formal statements and consistency comments.It instructs the model to analyze ambiguities, missing assumptions, type signatures, and required imports before revising.
  • D.1 INSTRUCTION FOR COLLECTING SFT TRAJECTORIES: The prompt operationalizes learning from mistakes by requiring targeted corrections based on a failed statement and its diagnosis.The authors describe this as structured self-reflection rather than generating unrelated new attempts.
  • D.2 INSTRUCTION FOR SEMANTIC CONSISTENCY CHECK: The consistency-check prompt compares natural-language and Lean statements across variables, types, quantifiers, constraints, logic, and semantic correspondence.It requires explicit mathematical and Lean analyses before comparative verification.
  • D.2 INSTRUCTION FOR SEMANTIC CONSISTENCY CHECK: The consistency-check output supplies the IsConsistent reward, benchmark evaluation, and validation of both initial and reflective SFT outputs.The same checking process supports training and evaluation uses.
  • D.2 INSTRUCTION FOR SEMANTIC CONSISTENCY CHECK: The evaluator must return a structured XML object containing analysis, a conclusion, and an exact Correct or Incorrect consistency judgment.Correct is reserved for cases where 100% mathematical equivalence is confirmed.
  • D.3 INSTRUCTION FOR ISFAITHFULCRITIQUE IN RL: A separate IsFaithfulCritique prompt reviews whether prior consistency comments and judgments are themselves correct and sufficiently reasoned.It asks the reviewer to identify errors in previous critiques and reassess the mathematical comparison.
Loading 2510.24592v3…