Generative Reward Models Solve Verdict-Preserving-Unfaithfulness in Autoformalization

To address failures where incorrect formal encodings pass solver verification, GenV introduces a generative verification method that distills a Z3-equivalence oracle into a continuous reference-equivalence score. Mechanistic analysis shows this method uses the model's native vocabulary space to extract precise spatial error signals.