# Beyond Solver Verdicts: Generative Reward Models for Autoformalization > Generative verification, which distills an offline Z3-equivalence oracle into a reference-free, continuous score, detects verdict-preserving-unfaithful formalizations with 0.961 AUROC, beating structural and solver-only methods. - **Source:** [arXiv](https://arxiv.org/abs/2609.11085) - **Published:** 2026-09-12 - **Permalink:** https://picx.dev/p/CMOZUV - **Whiteboard:** https://picx.dev/p/CMOZUV/image ## Summary # Beyond Solver Verdicts: Generative Reward Models for Autoformalization **Authors:** Vikash Singh, Debargha Ganguly, Aman Goel, Ali Torkamani, Xiaoxue Han, Joseph Lilien, Ferhat Erata, Vipin Chaudhary (Case Western Reserve University & Amazon Web Services) --- ## Summary (Overview) - **Formalizes Verdict-Preserving-Unfaithfulness (VPU)**: A critical failure mode in neurosymbolic systems where an incorrect formal encoding executes successfully and matches the expected solver verdict despite being logically non-equivalent to the reference formalization. - **Proves theoretical limits of structural verification**: Demonstrates that any scoring function depending only on binary solver verdicts achieves chance-level (0.5) AUROC on verdict-matched pairs. - **Introduces Generative Verification (GenV)**: A novel approach that distills an offline Z3-equivalence oracle into a reference-free, continuous verification score by repurposing the language model's native vocabulary space for next-token prediction. - **Achieves state-of-the-art results**: GenV+HN reaches 0.961 AUROC in reference-equivalence verification, generalizes zero-shot across unseen translators and formal styles, and yields an 11.3-point downstream accuracy gain in agentic test-time compute allocation. - **Provides mechanistic interpretability**: Gradient-based lenses and sparse autoencoders demonstrate that VPU and error-position information are natively recoverable from the verifier's hidden states without explicit localization training. --- ## Introduction and Theoretical Foundation ### Background and Motivation Neurosymbolic systems promise a clean division of labor: a language model translates natural language problems into formal logic, and a sound solver (e.g., Z3) performs deduction. However, the resulting guarantee is **conditional**—a solver certifies what follows from the supplied encoding, but does *not* certify that the encoding accurately represents the source problem. The translation step is therefore an independent point of failure. ### Formal Definition of VPU The paper studies this failure relative to a designated reference formalization $s^{\star}$. Reference-equivalence is defined by mutual implication: $$ \operatorname{Eq}(s, s^{\star}) = \mathbf{I}\left[\begin{array}{l} A(s) \wedge \neg A(s^{\star}) \text{ is unsat}, \\ A(s^{\star}) \wedge \neg A(s) \text{ is unsat} \end{array}\right]\tag{1} $$ where $A(s)$ denotes the logical conjunction of assertions in candidate encoding $s$. **Definition 1 (Reference-relative Verdict-Preserving-Unfaithfulness):** Relative to a designated reference $s^{\star}$, a candidate $s$ is VPU when it is syntactically valid, has the same solver verdict as the reference, and is not reference-equivalent: $$ \mathrm{VPU}(s; s^{\star}) = \mathbf{I}[v(s) = v(s^{\star})][1 - \mathrm{Eq}(s, s^{\star})]\tag{2} $$ ### Theoretical Impossibility Result **Proposition 1 (Binary verdict-only indistinguishability):** For any paired evaluation set where $s_i^+$ is reference-equivalent and $s_i^-$ is VPU with $v(s_i^+) = v(s_i^-)$ for every pair, any scoring function $g(s) = h(v(s))$ that depends only on the binary solver verdict assigns tied scores to both members of every pair, yielding an empirical AUROC of **0.5**. > *Proof sketch:* Because both members of every pair share the same verdict, $g(s_i^+) = h(v(s_i^+)) = h(v(s_i^-)) = g(s_i^-)$. The positive and negative score multisets are identical, so every comparison is a tie, giving AUROC = 0.5 under the half-credit convention. This result isolates a narrow information limit but does **not** preclude verifiers that inspect the source problem, candidate program, execution traces, or internal model states. --- ## Methodology ### 1. Verification via Next Token Prediction Rather than appending a randomly initialized classification head (which can disrupt pre-trained representations), GenV repurposes the frozen vocabulary head as a generative classifier. The model receives a context $c(x, s)$ (source problem + candidate encoding) and outputs a single token judgment ("Yes" for faithful, "No" for unfaithful). The continuous verification score is computed in a single forward pass by renormalizing probability mass over target classes: $$ f_{\theta}(x, s) = \frac{\sum_{u \in Y} \pi_u}{\sum_{u \in Y} \pi_u + \sum_{u \in N} \pi_u + \varepsilon}\tag{4} $$ where $\varepsilon = 10^{-9}$ is a stabilization constant, $Y$ and $N$ are vocabulary token ID sets for positive/negative answers, and $\pi = p_{\theta}(\cdot \mid c(x, s))$. ### 2. Supervised Fine-Tuning with Oracle Labels Training data $\mathcal{D} = \{(x_i, s_i, y_i)\}_{i=1}^{m}$ uses binary labels $y_i = \mathrm{Eq}(s_i, s_i^{\star})$ pre-computed by the exact Z3-equivalence oracle. The model is fine-tuned with causal cross-entropy loss over the answer sequence only: $$ \mathcal{L}(\theta) = -\frac{1}{m}\sum_{i=1}^{m}\sum_{j=1}^{M_i} \log p_{\theta}\left(a_{i,j} \mid [c_i; a_{i,