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.</p>\n","updatedAt":"2026-09-11T15:57:09.937Z","author":{"_id":"6702352c547acbd64cddf31e","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6702352c547acbd64cddf31e/elkGeA8piG-K-mXspBOhi.png","fullname":"Vikash Singh","name":"optimusPrimeBee","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":3,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.7903549075126648},"editors":["optimusPrimeBee"],"editorAvatarUrls":["https://cdn-avatars.huggingface.co/v1/production/uploads/6702352c547acbd64cddf31e/elkGeA8piG-K-mXspBOhi.png"],"reactions":[],"isReport":false}}],"primaryEmailConfirmed":false,"paper":{"id":"2609.11085","authors":[{"_id":"6aa4243c7ba345d44ad142bd","user":{"_id":"6702352c547acbd64cddf31e","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6702352c547acbd64cddf31e/elkGeA8piG-K-mXspBOhi.png","isPro":false,"fullname":"Vikash Singh","user":"optimusPrimeBee","type":"user","name":"optimusPrimeBee"},"name":"Vikash Singh","status":"claimed_verified","statusLastChangedAt":"2026-09-11T16:45:04.572Z","hidden":false},{"_id":"6aa4243c7ba345d44ad142be","name":"Debargha Ganguly","hidden":false},{"_id":"6aa4243c7ba345d44ad142bf","name":"Aman Goel","hidden":false},{"_id":"6aa4243c7ba345d44ad142c0","name":"Ali Torkamani","hidden":false},{"_id":"6aa4243c7ba345d44ad142c1","name":"Xiaoxue Han","hidden":false},{"_id":"6aa4243c7ba345d44ad142c2","name":"Joseph Lilien","hidden":false},{"_id":"6aa4243c7ba345d44ad142c3","name":"Ferhat Erata","hidden":false},{"_id":"6aa4243c7ba345d44ad142c4","name":"Vipin Chaudhary","hidden":false}],"publishedAt":"2026-09-10T00:00:00.000Z","submittedOnDailyAt":"2026-09-11T00:00:00.000Z","title":"Beyond Solver Verdicts: Generative Reward Models for Autoformalization","submittedOnDailyBy":{"_id":"6702352c547acbd64cddf31e","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6702352c547acbd64cddf31e/elkGeA8piG-K-mXspBOhi.png","isPro":false,"fullname":"Vikash Singh","user":"optimusPrimeBee","type":"user","name":"optimusPrimeBee"},"summary":"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.","upvotes":1,"discussionId":"6aa4243c7ba345d44ad142c5","ai_summary":"Neurosymbolic reasoning is vulnerable to incorrect but verdict-matching formal translations, which are addressed by a generative verification method that scores reference equivalence without an oracle and improves downstream accuracy.","ai_keywords":["Verdict-Preserving-Unfaithfulness","Z3-equivalence oracle","Generative Verification","decision-projected logit lenses","sparse autoencoders","reference-equivalence verification"],"ai_summary_model":"thinkingmachines/Inkling-Small","organization":{"_id":"6058ec29102f61b42f65ae35","name":"AWS","fullname":"Amazon Web Services","avatar":"https://cdn-avatars.huggingface.co/v1/production/uploads/66f19ed428ae41c20c470792/wtuzZxWzijQ3do3zYoOFH.png"}},"canReadDatabase":false,"canManagePapers":false,"canSubmit":false,"hasHfLevelAccess":false,"upvoted":false,"upvoters":[{"_id":"6702352c547acbd64cddf31e","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/6702352c547acbd64cddf31e/elkGeA8piG-K-mXspBOhi.png","isPro":false,"fullname":"Vikash Singh","user":"optimusPrimeBee","type":"user"}],"acceptLanguages":["en"],"dailyPaperRank":0,"organization":{"_id":"6058ec29102f61b42f65ae35","name":"AWS","fullname":"Amazon Web Services","avatar":"https://cdn-avatars.huggingface.co/v1/production/uploads/66f19ed428ae41c20c470792/wtuzZxWzijQ3do3zYoOFH.png"},"markdownContentUrl":"https://huggingface.co/buckets/huggingchat/papers-content/resolve/2609/2609.11085.md","query":{}}">
Beyond Solver Verdicts: Generative Reward Models for Autoformalization
Abstract
Neurosymbolic reasoning is vulnerable to incorrect but verdict-matching formal translations, which are addressed by a generative verification method that scores reference equivalence without an oracle and improves downstream accuracy.
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.
Community
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.
Upload images, audio, and videos by dragging in the text input, pasting, or clicking here.
Tap or paste here to upload images
Cite arxiv.org/abs/2609.11085 in a model README.md to link it from this page.
Cite arxiv.org/abs/2609.11085 in a dataset README.md to link it from this page.
Cite arxiv.org/abs/2609.11085 in a Space README.md to link it from this page.
Discussion (0)
Sign in to join the discussion. Free account, 30 seconds — email code or GitHub.
Sign in →No comments yet. Sign in and be the first to say something.