Found first: a primary source the press has not covered yet.
A paper by Vikash Singh, Debargha Ganguly, Aman Goel, Ali Torkamani, Xiaoxue Han, Joseph Lilien, Ferhat Erata, and Vipin Chaudhary introduces Verdict-Preserving-Unfaithfulness (VPU), a class of autoformalization failure in which an incorrect formal encoding executes successfully and returns the expected solver verdict. The paper proves that structural, verdict-only verification is mathematically bounded to chance-level detection of such errors and proposes a generative replacement that scores 0.961 AUROC.
What the source says
VPU describes the case where an AI-generated formal encoding is semantically wrong but syntactically valid and solver-compliant, defeating every check built on whether a proof succeeds or fails. The authors prove theoretically that any verifier relying on solver verdicts or structural heuristics cannot reliably detect VPU traces. Their method, Generative Verification (GenV), distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score using the language model's native vocabulary. GenV+HN achieves 0.961 AUROC on reference-equivalence verification and an 11.3-point downstream accuracy gain in agentic test-time compute allocation. It generalizes zero-shot to unseen translators and divergent formal styles, and mechanistic analysis via decision-projected logit lenses and sparse autoencoders shows it locates spatial error coordinates without explicit localization training.
Why it matters
Passing solver checks has been treated as the reliable signal that an AI-generated proof is correct. VPU shows that signal is structurally broken for an entire class of errors: a proof can be semantically wrong and still pass every verdict-based check. The theoretical proof of this bound means improving verdict-only verifiers within the existing paradigm cannot close it. This bears directly on active disputes between AI labs and mathematicians over whether AI-assisted proofs are genuinely valid or merely verdict-compliant. GenV is a concrete fix, and the larger result is that the verification layer assumed to be sound is, on VPU traces, no better than chance.