Paper defines 'VPU': solver-verified AI math can hide errors

Neurosymbolic systems use formal solvers to check AI-generated math translations by running them and seeing whether the verdict matches. But an incorrect encoding can execute successfully, return the expected result, and pass verification anyway. A preprint on arXiv from Vikash Singh and colleagues formalizes this failure mode and gives it a name: Verdict-Preserving-Unfaithfulness, or VPU.

The paper's central claim is that the blindspot is provable, not empirical. "We theoretically prove that structural, verdict-only verification heuristics are mathematically bounded to chance-level detection on these deceptively valid traces," the authors write. A verifier that only checks whether the answer came out right, in other words, does no better than chance at catching a VPU case.

The proposed fix, GenV, sidesteps the verdict. It reuses a Z3-equivalence oracle to train a language model into what the paper calls a "reference-free, continuous reference-equivalence score", a graded similarity check against a designated formalization rather than a pass/fail run. The oracle-mined variant, GenV+HN, reaches 0.961 AUROC on reference-equivalence verification and yields an 11.3-point downstream accuracy gain when it steers test-time compute in an agentic setup. The abstract publishes no per-model breakdown of how often VPU trips up specific frontier systems.