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,<j}]\right)\tag{5}$$

Context tokens condition the forward pass but their loss is masked out, preventing catastrophic forgetting.

3. Oracle-Guided Hard Negative Mining

To address the sparsity of deceptive false positives, the framework bootstraps the training manifold with programmatic hard negatives. Targeted mutation operators $\mu(\cdot)$ (e.g., flipping relational operators, perturbing constants, reversing implications) are applied to gold references. A mutated candidate is retained if and only if it is syntactically correct and satisfies the VPU criteria from Definition 1, with Z3 serving as the deterministic adjudicator.

---

Empirical Validation / Results

RQ1: Representation vs. Structure in Equivalence Verification

Table 1: Reference-faithfulness AUROC

Table 2: Matched supervision and readout ablation

Key findings:

• The vocabulary-space readout provides an additional improvement over the two-class head under matched supervision.
• Ablations confirm robustness to target token choice (e.g., "Yes/No" vs. "A/B" or "X/Y"), indicating the model genuinely tracks the equivalence target rather than exploiting linguistic biases.

RQ2: Zero-Shot Generalization

Table 3: Zero-shot AUROC across out-of-domain formal styles

GenV+HN maintains consistent margins across all OOD formal styles, while token-head reward models suffer severe degradation.

RQ3: Diagnostic Alignment with Human Intent

Table 4: Reference-equivalence vs. panel-majority intent on a contested slice

GenV+HN's advantage is specific to strict reference-equivalence; the gap on subjective human intent highlights an open challenge in resolving informal ambiguity.

RQ4: Test-Time Agentic Utility

Table 5: Mechanism attribution by replay on identical recorded pools

The integration of GenV+HN drives total system accuracy from 0.655 to 0.768 (+11.3 points), with the dynamic verification gate (not static re-ranking) being the superior deployment mechanism.

---

Theoretical and Practical Implications

Theoretical Contributions

1. Formal characterization of VPU: Provides a rigorous, operational definition of reference-relative unfaithfulness that is deterministic and trainable.
2. Information-theoretic limits: Proves that binary verdict-only scoring is mathematically bounded to chance-level detection on verdict-matched pairs.
3. Separation of supervision from deployment: Establishes a clean distinction between privileged oracle information (used only in training) and reference-free inference inputs.

Practical Implications

1. Deployable verification: GenV+HN requires only the source problem and candidate encoding at inference time—no reference formalization needed.
2. Agentic compute allocation: The verifier effectively governs test-time compute, providing gains across diverse backends (from +2.3 to +42.6 points depending on generator capability).
3. Architecture-agnostic: The generative readout works within the model's native vocabulary space, requiring no architectural changes.

Mechanistic Insights

The paper demonstrates that VPU and error-position information are diagnostically recoverable from intermediate representations:

• Decision-projected gradient lens: The margin $g = \mathrm{logsumexp}_{u \in Y} z_u - \mathrm{logsumexp}_{u \in N} z_u$ combined with gradient-times-activation attribution $q_{\ell,t} = \left\langle \frac{\partial g}{\partial h_{\ell,t}}, h_{\ell,t} \right\rangle$ localizes mutations without explicit localization training.
• Sparse autoencoder probes: A TopK SAE on layer-48 activations recovers 0.960 AUROC for GenV+HN, showing that PRM and ORM hidden states contain substantially more VPU information than their deployed output scores expose.

---

Conclusion

GenV+HN resolves the critical vulnerability of Verdict-Preserving-Unfaithfulness in neurosymbolic systems by distilling offline Z3-equivalence into a reference-free generative readout. Key takeaways:

1. Structural checks are fundamentally insufficient for detecting VPU—only learned, reference-equivalence-aware verification can bridge this gap.
2. Generative readouts outperform classification heads under matched supervision, and hard-negative mining provides additional robustness.
3. The verifier generalizes zero-shot across unseen translators and divergent formal styles, though severe OOD shifts can degrade calibration.
4. Reference-equivalence serves as an uncompromising, reproducible target for formal evaluation, but subjective human intent remains an open challenge.

Future Directions

• Bridging the semantic gap between strict reference-equivalence and subjective human intent via human-labeled benchmarks
• Extending diagnostic internal representations to causally steer multi-error repair pipelines
• Handling naturally occurring correlated, multi-error distributions (current mining uses synthetic single-edit mutations)
• Addressing the vacuous-equivalence limitation for unsatisfiable reference formulas

Limitations

• Supervision is bounded by SMT decidability limits and assumes a fully specified gold reference
• Advisory feedback does not yield measurable accuracy improvements without expanding the sampling budget
• The logical equivalence guarantee applies only to satisfiable formal specifications (two unsatisfiable formulas are vacuously equivalent under standard Z3 model checking)