# Beyond Solver Verdicts: Generative Reward Models for Autoformalization

arXiv: https://arxiv.org/abs/2609.11085 · HTML: https://mlsanity.com/paper/2609.11085/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Process reward models for reasoning, one of 10 directions in LLM alignment / RLHF / preference optimisation.
- Builds on 5 of its 10 references that are in the map.
- First posted on arXiv 10 Sep 2026.

## Placed in

- LLM alignment / RLHF / preference optimisation / [Process reward models for reasoning](https://mlsanity.com/alignment/process-reward-models-for-reasoning/)
- Mechanistic interpretability / [Steering and interpreting LLM reasoning](https://mlsanity.com/mechinterp/steering-and-interpreting-llm-reasoning/)

## Builds on (most cited first, 5 of 5)

- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning](https://mlsanity.com/paper/2601.20055/) (2026)

## Abstract (arXiv)

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.