2026-09-24·★ MEMBER·PAPER·9 min read

Paper Explained: Beyond Solver Verdicts — When the Solver Says Yes but the Translation Is Wrong

An LLM translates a problem into logic and Z3 solves it. This paper names the failure where the solver's verdict is right but the translation is wrong (VPU), and distills Z3's equivalence check into a Yes/No next-token verifier called GenV. Explained from zero.

Key points

Verdict-Preserving-Unfaithfulness (VPU) is a failure where an encoding returns the same verdict as the reference but is not logically equivalent to it.
A solver only certifies what follows from the encoding it is given; it does not certify that the encoding faithfully represents the problem.
Any score depending only on the solver verdict ties correct and VPU candidates, so AUROC comes out at exactly 0.5.
The authors propose Generative Verification (GenV), which distills an offline Z3 equivalence oracle into a continuous score needing no reference at inference time.
The hard-negative-mined variant, GenV+HN, reaches 0.961 AUROC on reference-equivalence.

#autoformalization #reward-model #verifier #smt #z3 #evaluation #neurosymbolic

ModalitytextTaskevaluation

Beyond Solver Verdicts: Generative Reward Models for Autoformalization

Primary source — what this article is built on

undefined2026-09-10→undefined2026-09-24same month

Beyond Solver Verdicts: Generative Reward Models for AutoformalizationVikash Singh, Debargha Ganguly, Aman Goel et al. · 2026-09-10 · v2arXiv:2609.11085Paper page·PDF

undefined

Neurosymbolic systems rely on mathematical solvers to guarantee reasoning correctness, yet solvers are fundamentally blind to whether a formal translation maintains strict reference-equivalence to a designated formalization. We formalize this vulnerability as Verdict-Preserving-Unfaithfulness (VPU): a failure mode where an incorrect encoding executes successfully and matches the expected verdict. We theoretically prove that structural, verdict-only verification heuristics are mathematically bounded to chance-level detection on these deceptively valid traces. To resolve this, we introduce Generative Verification (GenV), which distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score by repurposing the language model's native vocabulary space. Mechanistic analysis via decision-projected logit lenses and sparse autoencoders shows this generative readout natively extracts precise spatial error coordinates without explicit localization training. Empirically, our oracle-mined verifier (GenV+HN) achieves 0.961 AUROC in reference-equivalence verification, generalizes zero-shot across unseen translators and divergent formal styles, and yields an 11.3-point downstream accuracy gain in agentic test-time compute allocation.

What this paper claims

The paper is "Beyond Solver Verdicts: Generative Reward Models for Autoformalization" (Singh et al., arXiv:2609.11085, September 2026), a collaboration between Case Western Reserve University and Amazon Web Services.

Here is the abstract in plain terms. Neurosymbolic systems lean on mathematical solvers to guarantee that reasoning is correct. But a solver can't tell whether the translation from natural language into formal logic is strictly equivalent to a designated reference formalization. The authors call this blind spot Verdict-Preserving-Unfaithfulness (VPU): a wrong encoding runs without error and still returns the expected verdict. They prove that structural checks which look only at the verdict can detect such cases no better than chance. Their fix is Generative Verification (GenV), which distills an offline Z3 equivalence oracle into a continuous score that needs no reference at inference time. It does this by reusing the language model's own vocabulary output. Analysis with logit-lens-style probes and sparse autoencoders shows that this readout carries information about where the error sits, even though it was never trained to localize. The hard-negative-mined variant, GenV+HN, reaches 0.961 AUROC on reference-equivalence, transfers zero-shot to unseen translators and formal styles, and adds 11.3 points of downstream accuracy when used to allocate test-time compute in an agent.

An analogy: the calculator is right, the copied equation is not

Think of a word problem that says "there are more than five apples." While copying it into an equation you write "fewer than five." The calculator (the solver) evaluates your equation flawlessly. If you're unlucky, the wrong equation even gives the same yes/no conclusion as the right one.

A grader who only checks the final conclusion will never catch that copying mistake, and that is the situation this paper studies. The solver is sound; it doesn't lie. But it only certifies what follows from the encoding you handed it. It does not certify that the encoding faithfully represents the problem (§1).

VPU: same verdict, different meaning

Let's make this precise. Let $x$ be the natural-language problem, $s$ a candidate encoding in SMT-LIBv2 written by an LLM, and $s^\star$ the designated reference formalization. $A(s)$ is the conjunction of all assertions in $s$ .

\mathrm{Eq}(s,s^\star)=\mathbf{I}\big[\,A(s)\wedge\neg A(s^\star)\ \text{is unsat and}\ A(s^\star)\wedge\neg A(s)\ \text{is unsat}\,\big]

(1)

In words: the two encodings are equivalent when there is no situation where $s$ holds but $s^\star$ doesn't, and no situation the other way around. $\mathbf{I}[\cdot]$ is 1 if the bracket is true and 0 otherwise. Checking only one direction isn't enough, so Z3 checks both (§3).

With that, VPU is defined as:

\mathrm{VPU}(s;s^\star)=\mathbf{I}[v(s)=v(s^\star)]\cdot\big(1-\mathrm{Eq}(s,s^\star)\big)

(2)

Here $v(s)$ is the solver's verdict (sat = a solution exists, unsat = none exists). In words: VPU means "same verdict as the reference" and "not logically equivalent to it." In the paper's Figure 1, flipping a single $>$ comparison yields a candidate that returns the same sat as the reference.

Why verdicts alone can never catch this

Proposition 1 (§3) is a very short argument. Build an evaluation set of pairs, each with a correct candidate $s^+$ and a VPU candidate $s^-$ that share the same verdict. Any score $g(s)=h(v(s))$ that depends only on the verdict gives both members of a pair the same value, whatever $h$ you choose:

$g(s_i^+)=h(v(s_i^+))=h(v(s_i^-))=g(s_i^-)$

Same input, same output, so every pair ties. Under the usual convention that a tie gets half credit, AUROC (the probability of scoring the correct one higher) comes out at exactly 0.5, the same as a coin flip.

The authors are careful about scope. The result limits schemes that read only the binary verdict. Whether a verifier that reads the problem, the code, execution traces, or hidden states can detect VPU is left as an empirical question (§1, §3).

How GenV works: compare the odds of "Yes" and "No"

At deployment the reference $s^\star$ is gone, so the system has to learn a function $f_\theta(x,s)$ that estimates the probability of equivalence from $(x,s)$ alone (the paper's Eq. 3).

GenV's key choice is not to bolt on a new classification layer. It gives the model a referee prompt, "Is this encoding faithful to the problem? Answer with exactly one word, Yes or No," and reads the next-token probabilities directly (§4).