Researchers introduce Generative Reward Models to address Verdict-Preserving-Unfaithfulness (VPU) in neurosymbolic systems, where incorrect formal translations may still produce correct solver verdicts. The paper demonstrates that structural and verdict-only verification heuristics are insufficient, proposing a new approach to ensure reference-equivalence in autoformalization. This work enhances reliability in mathematical reasoning systems by targeting a critical gap in current verification methods.