Beyond Solver Verdicts: Generative Reward Models for Autoformalization

The Problem

Imagine a system that translates a natural-language math problem into a formal logic language that a theorem prover like Z3 can understand. The system then asks Z3 to check if the problem has a solution. In a perfect world, Z3’s "yes" or "no" answer tells you everything you need to know.

But this paper identifies a subtle and dangerous failure mode. They call it Verdict-Preserving-Unfaithfulness (VPU).

Here is the scenario: A translator changes a "greater than" sign to a "less than" sign in the formal code. Mathematically, this changes the problem's meaning entirely. However, if the translator also tweaks other numbers to compensate, the formal problem might still have a solution. Z3 will happily say "SAT" ( satisfiable) for both the original and the modified code. To an outside observer—and to simple verification scripts—everything looks correct because the solver’s verdict is identical.

The paper proves that any system relying only on the solver’s verdict (the binary "sat/unsat" output) is fundamentally blind to these errors. Mathematically, such systems are bounded at 0.5 AUROC—essentially flipping a coin—when trying to distinguish a faithful encoding from a VPU encoding that flies under the solver’s radar.

For a smart user outside academia, the stakes are real. In safety-critical applications, automated reasoning systems are often assumed to be "correct" because the solver runs without error. VPU represents a class of bugs where the system appears healthy but is actually reasoning about the wrong problem. This undermines the "neurosymbolic" promise of combining LLMs' flexibility with solvers' rigor.

How It Works (The Technical Mechanics)

The authors propose Generative Verification (GenV) to solve this. The core idea is to move beyond the solver’s binary verdict and use the language model's own "instinct" for faithfulness.

The Mechanics: Teaching the Model to Judge

The system does not add a new neural network head. Instead, it repurposes the language model's existing vocabulary. Here is the step-by-step:

1. The Prompt: The model is given a fixed prompt asking: "Is this encoding faithful to the problem? Answer Yes or No."
2. The Score: The model outputs a probability distribution over its vocabulary. GenV takes the probability of the "Yes" tokens and renormalizes it against the "Yes" and "No" tokens.
   • Mathematically: $f_\theta(x, s) = \frac{\sum_{u \in Y} \pi_u}{\sum_{u \in Y} \pi_u + \sum_{u \in N} \pi_u + \epsilon}$
   • Where $\pi$ is the model's next-token distribution, $Y$ are the "Yes" tokens, $N$ are the "No" tokens, and $\epsilon$ is a tiny stabilizer.
3. Training: The model is fine-tuned on data labeled by Z3. Z3 acts as the "ground truth" oracle. If Z3 says two encodings are logically equivalent, the label is "Yes"; if not, "No."
4. Hard Negative Mining: To make the model good at spotting tricky errors, the authors programmatically mutate the reference encodings (e.g., flipping operators) and force the model to label these as "No." This is done via Z3, which acts as an automated judge to ensure the mutations are truly deceptive (they pass the solver but fail the logic).

The Analogy: The Code Reviewer

Think of a senior software engineer (the LLM) reviewing a pull request. The "solver verdict" is like a CI/CD pipeline that checks if the code compiles and runs without crashing. A junior dev could submit code that compiles and runs, but does the wrong calculation.

GenV is not the compile check; it is the senior engineer reading the code. They don't just check if it runs; they check if it solves the actual problem stated in the ticket. The "hard negative mining" is like the senior engineer practicing on deliberately tricky bug reports to sharpen their instincts.

Key Results & Benchmarks

The results are compelling, especially the gap between the proposed method and previous approaches.

Detection Power (AUROC) The paper reports an AUROC of 0.961 on their main benchmark. To a technical audience, AUROC measures how well a model ranks faithful encodings above unfaithful ones. A score of 0.961 is excellent—it means that if you pick one faithful and one unfaithful encoding at random, GenV+HN will correctly identify the faithful one 96.1% of the time.

For contrast, the "solver-only" approach scores exactly 0.500 (chance). Previous learned reward models (Process RM and Outcome RM) manage only 0.756 and 0.762 respectively. The paper’s base model (GenV) without the "hard negative mining" still hits 0.956, showing the core idea is strong, but the mining pushes it over the top.

Generalization (Zero-Shot) The model generalizes well to new types of formal logic. It achieves high AUROC (0.842–0.964) across diverse datasets like ProverQA and FOLIO, demonstrating it isn't just memorizing specific problem styles.

Downstream Impact (The 11.3-Point Gain) This is perhaps the most practical result. The authors integrate the verifier into an "agentic" system (Proof of Thought), where the system can decide to spend more computation on a hard problem.

The result is an 11.3-point gain in downstream accuracy. How does this work in plain language?

• Baseline: A system that just generates answers gets 65.5% accuracy.
• With GenV+HN: Accuracy jumps to 76.8%.
• The Breakdown: The gain comes from three stages:
  1. Best-of-N voting: Simply running the model 5 times and voting gives +9.3 points.
  2. Gated Escalation: The verifier decides when to trigger a more expensive "thinking" phase, adding +1.2 points.
  3. Verifier Selection: Picking the best encoding from the pool based on the verifier's score adds +0.9 points.

Essentially, the verifier acts as a smart gatekeeper. It doesn't just grade the answers; it tells the system when to work harder, leading to a significant boost in the final score.

Why It Matters (Key Takeaways)

Here are the four critical takeaways from this paper:

1. The Solver's Blind Spot: Solvers are necessary but not sufficient. A "SAT" verdict from Z3 guarantees the code can run, but it does not guarantee the code represents the user's intent. We need explicit equivalence checks.
2. Generative Verification is Practical: You don't need to build a specialized neural network from scratch to check logical equivalence. By repurposing the LLM's next-token prediction with a simple "Yes/No" prompt and Z3 labels, you get a deployable verifier that hits near-perfect AUROC (0.961).
3. The 11.3-Point Payoff: This isn't just an academic metric. Integrating this verifier into agentic systems (systems that think and then check their work) yields a massive 11.3% improvement in accuracy. This is a tangible productivity boost for anyone using LLMs for reasoning.
4. Diagnosability: The paper includes fascinating "mechanistic" analysis. They show that the model's internal activations actually contain information about where the error is (which assertion is wrong), even though the model wasn't explicitly trained to point that out. This means the system not only detects the error but potentially localizes it for debugging.

What to watch for next: The authors acknowledge a limitation: the model optimizes for "strict reference-equivalence" as defined by the Z3 oracle, which may differ from "subjective human intent." As we deploy these systems, we will need to balance the rigor of formal logic with the nuances of how humans actually phrase problems. Additionally, the system currently works best when the formal problem is "satisfiable"; handling inconsistent or unsatisfiable references remains a technical edge case.