ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization

AI summary

Overview

• Research area: Natural language processing, specifically autoformalization (translating natural-language mathematics into machine-verifiable formal statements such as Lean 4), combined with reinforcement learning for large language model training.
• Technical level: Intermediate. The paper is readable without deep Lean expertise, but assumes familiarity with reinforcement learning, reward design, and LLM training pipelines (SFT, GRPO).
• Scope: The paper proposes ReForm, an iterative reflect-and-refine autoformalization method; Prospective Bounded Sequence Optimization (PBSO), a reinforcement learning algorithm for heterogeneous rewards at different sequence positions; and ConsistencyCheck, an expert-annotated benchmark for measuring how reliable LLM judges are at evaluating semantic faithfulness.

What This Paper Is About

Autoformalization asks a model to turn a natural-language math problem into a formal statement that a proof assistant like Lean can check. Current systems are good at producing code that compiles but frequently distort the original problem's meaning — misreading quantifier scope, dropping implicit constraints, or mishandling edge cases. The paper's goal is to make autoformalization self-correcting: instead of one forward pass, the model generates a candidate statement, critiques its own semantic fidelity, and revises the statement based on that critique, repeating until the critique reports a faithful match.

Key Contributions

1. A reflective autoformalization paradigm (ReForm). Autoformalization is reframed from single-pass translation into an interleaved loop of statement generation and semantic self-validation, implemented as one continuous autoregressive generation so the cost stays close to one-pass methods.

2. Prospective Bounded Sequence Optimization (PBSO). A reinforcement learning algorithm that assigns a task reward at the end of a sequence and auxiliary rewards at intermediate critique steps, then computes "prospective bounded returns" — discounted backward-accumulated returns clipped to the reward range — to produce position-specific advantages for GRPO-style policy updates.

3. The ConsistencyCheck benchmark. A set of 859 expert-annotated items for binary classification of whether a formal statement preserves the original problem's meaning, used both to measure LLM judges and to quantify how hard autoformalization is.

4. Strong empirical results across four benchmarks. ReForm-8B and ReForm-32B, built on Qwen3, achieve an average of +22.6 percentage points in semantic consistency over the strongest baseline (ReForm-32B), with the gains concentrated on semantic fidelity rather than syntax.

Main Findings

• Large, consistent gains over strong baselines. ReForm-32B reaches 72.7% average semantic consistency versus 50.1% for Goedel-Formalizer-V2-32B, the best comparable baseline. ReForm-8B averages 64.3%, a +14.8pp improvement over the same-size Goedel-Formalizer-V2-8B.

• An 8B model outperforms a 32B one. ReForm-8B exceeds Goedel-Formalizer-V2-32B by +14.2pp in semantic consistency, indicating the reflective paradigm adds something beyond parameter scaling.

• Gains grow with problem difficulty. Improvements are +18.3pp on ProofNet and +14.4pp on PutnamBench for ReForm-8B, and +20.0pp on AIME2025. Semantic gains consistently exceed syntactic gains by roughly 2–3x, showing the method addresses the meaning-preservation bottleneck rather than compilation.

• Bounded returns and auxiliary rewards are both necessary. Removing the clipping in the return computation hurts hardest benchmarks severely (AIME2025 drops from 46.7 to 26.7). Removing the auxiliary critique reward also degrades performance, and the damage increases with problem difficulty.

• One-pass training collapses on hard problems. With identical training data, a one-pass variant scores 82.7/59.1/40.8/16.7 on miniF2F/ProofNet/Putnam/AIME2025 versus ReForm's 87.7/65.6/57.3/46.7 — the gap widens sharply as difficulty rises.

• Reflective behavior emerges without explicit length incentives. During RL, average response length grows from about 2,300 to 4,800 tokens (2.1x) purely from the heterogeneous reward signal, and held-out PutnamBench semantic consistency rises from 47% to 57%, tracking training reward.

• Human-written formalizations are themselves error-prone. 16.4% of miniF2F and 38.5% of ProofNet human-authored formal statements contain semantic errors, underscoring the intrinsic difficulty of the task.

• LLM judges are usable but imperfect. The best judge (Gemini-2.5-Pro) achieves 85.8% accuracy on ConsistencyCheck; open-source Qwen3-235B-A22B reaches 82.9%. The authors argue the gap between classification (86% ceiling) and generation explains why faithful formalization remains hard.

• Results hold under a second, independent judge. Evaluated with CriticLean-14B, ReForm-8B still improves +18.0pp on average over the comparable baseline and +33.3pp on AIME2025, confirming the gains are not artifacts of one evaluator.

• Human evaluation aligns with automated scores. Manual review found 86.1% of ReForm-8B's miniF2F outputs and 69.4% of its ProofNet outputs correct, close to the corresponding LLM-judged semantic consistency scores of 87.7% and 65.6%.

Methodology in Plain English

The model is given a natural-language math problem and produces a Lean statement. It then immediately critiques that statement — does this formalization actually capture the problem's meaning? That critique becomes part of the context for producing a revised statement, and the cycle repeats within a single generation.

To train this behavior, the authors use two kinds of reward. A task reward is given at the very end of the sequence, worth 1 only if the final statement both compiles in Lean and is judged semantically consistent with the original problem. Auxiliary rewards are given at each critique step, worth 1 if the critique faithfully diagnoses whether the current statement matches the problem — penalizing false alarms, missed errors, and premature declarations of success.

Rewards at different sequence positions are combined by computing, for each step, a discounted sum of all future rewards. This sum is clipped to the reward range so it cannot accumulate without bound. The clipped "prospective bounded returns" are then normalized across the sampled trajectories to yield an advantage for every position. Early iterations that spot critical errors can receive higher advantages than later iterations making small refinements. These position-specific advantages are fed into GRPO to update the policy, so the model learns both to write better statements and to write better critiques — with each skill reinforcing the other.

Why This Matters

Autoformalization is the entry point to the entire formal mathematical reasoning pipeline. If the formal statement does not mean what the original problem means, proving it is worthless, so improving semantic fidelity at this stage has downstream leverage on theorem proving, verification, and any application that depends on trustworthy formalization.

Real-world applications:

• Mathematical education. Automatically checking that a student's or teacher's formulation of a problem is correct, or generating verified formal versions of textbook exercises at scale.
• Software and hardware verification. Translating natural-language requirements or specifications into machine-checkable formal statements, where subtle semantic drift is a safety issue.
• Formal math library curation. Helping populate and audit libraries like Mathlib by converting informal results into faithful formal statements, with automated flagging of likely misformalizations.
• Agentic and tool-augmented reasoning systems. Serving as a component that converts informal user requests into precise formal objectives that verifiers or solvers can act on.
• Benchmark and evaluation infrastructure. ConsistencyCheck and the reliability analysis provide a template for validating LLM-as-judge pipelines in domains beyond math.

Industry relevance: the work is directly applicable to AI labs building theorem-proving or formal-verification products, to tooling companies integrating Lean or similar assistants, and to any organization that relies on LLM judges and needs a defensible way to measure judge reliability. The PBSO algorithm is also a general-purpose contribution to reinforcement learning for multi-objective, multi-step generation, which extends beyond mathematics.

Future Directions

• Extending reflection from statements to proofs. The current loop validates and revises formal statements only. Whether the same reflective mechanism can be applied jointly to statement and proof, or integrated with an automated theorem prover in an outer loop, remains open.
• Richer or more reliable reward signals. Both the task reward and the auxiliary reward depend on LLM-based judges with roughly a 14% error rate. Replacing or augmenting these with stronger verifiers, or training specialized critics, could raise the ceiling.
• Adaptive iteration control. The model currently decides when to stop via its own critique. Learning when further refinement is not worth the compute — or how many iterations are optimal per problem difficulty — is an unresolved efficiency question.
• Generalizing PBSO beyond autoformalization. Prospective bounded returns are designed for any sequential task with objectives that must be evaluated at different positions. Applying them to agentic tasks, multi-stage reasoning, or code generation is a natural extension.
• Closing the classification-generation gap. Since even binary semantic judgment plateaus at 85.8%, understanding what makes generation harder than recognition — and whether that gap can be narrowed — is a foundational question for the field.

Target Audience

Researchers and engineers working on formal mathematical reasoning, autoformalization, or theorem proving will find the core contribution most directly useful. The paper also benefits reinforcement learning researchers interested in multi-objective or position-specific reward design, since PBSO is presented as a general algorithm. Practitioners building LLM-as-judge evaluation pipelines will value the ConsistencyCheck benchmark and the reliability analysis. Finally, graduate students entering the intersection of LLMs and formal methods will find the paper accessible as an entry point to the autoformalization literature.

Authors’ abstract

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.