Beyond Solver Verdicts: Generative Reward Models for Autoformalization

Neurosymbolic systems typically trust formal solvers to guarantee correctness, yet solvers remain blind to whether a translation accurately captures the original problem—a failure mode termed Verdict-Preserving-Unfaithfulness (VPU). This paper introduces Generative Verification (GenV), distilling an offline Z3 equivalence oracle into a reference-free, continuous scoring mechanism within a language model's native vocabulary space. Mechanistic analysis reveals it localizes translation errors without explicit supervision, while empirical benchmarks demonstrate a 0.961 AUROC in equivalence verification and an 11.3-point downstream accuracy gain during agentic test-time compute allocation.