Beyond Solver Verdicts: Generative Reward Models for Autoformalization
Researchers introduce Generative Verification (GenV), a generative reward model achieving 0.961 AUROC in detecting unfaithful autoformalization that preserves solver verdicts.
The paper formalizes Verdict-Preserving-Unfaithfulness (VPU), a failure mode in neurosymbolic autoformalization where an incorrect encoding executes successfully and matches the expected solver verdict, and proves verdict-only verification is bounded to chance-level detection. The proposed Generative Verification (GenV) distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score within the language model's vocabulary space. The oracle-mined verifier (GenV+HN) achieves 0.961 AUROC, generalizes zero-shot across unseen translators and formal styles, and yields an 11.3-point downstream accuracy gain in agentic test-time compute allocation. Mechanistic analysis with decision-projected logit lenses and sparse autoencoders shows the generative readout extracts precise spatial error coordinates without explicit localization training.
- GenV distills an offline Z3-equivalence oracle into a reference-free verification score
- GenV+HN reaches 0.961 AUROC and generalizes zero-shot across translators
- Delivers an 11.3-point downstream gain in agentic test-time compute allocation
- Mechanistic analysis shows spatial error localization without explicit training
Full article150 words · extracted from huggingface.co · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://huggingface.co/papers/2609.11085