Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification

• URL: http://arxiv.org/abs/2606.01160v1
• Date: Sun, 31 May 2026 11:06:48 GMT
• Title: Expected Value Alignment for Generative Reward Modeling in Formal Mathematics Verification
• Abstract summary: We introduce Expected Value Alignment (EVA), a reward-modeling procedure that keeps the surface output discrete while extracting continuous scores from the model's token distribution.<n>We instantiate EVA in textitLeibniz, a reward model for Lean 4 formal verification, and evaluate it against zero-shot and reward-modeling baselines.
• Score: 12.08180258890855
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) are increasingly used with formal interactive theorem provers such as Lean 4. Scaling these systems with reinforcement learning or search methods requires process reward models (PRMs) that can evaluate intermediate reasoning steps. Existing reward-model designs expose a practical trade-off. Value-head models provide continuous scores but modify the generative model interface, while generative reward models preserve textual rationales but are poorly matched to continuous floating-point regression because numeric values are split across tokens. We introduce Expected Value Alignment (EVA), a reward-modeling procedure that keeps the surface output discrete while extracting continuous scores from the model's token distribution. The model emits integer scores in a structured JSON format, and EVA computes a continuous score as the expectation over the logits of the corresponding anchor tokens. Training combines the causal language modeling objective with an auxiliary mean squared error loss on these expected values. We instantiate EVA in \textit{Leibniz}, a reward model for Lean 4 formal verification, and evaluate it against zero-shot and reward-modeling baselines. The evaluation demonstrates that continuous logit-based scoring significantly reduces discretization artifacts while retaining the interpretability of generative critiques.

Related papers

• From Coarse to Fine: Benchmarking and Reward Modeling for Writing-Centric Generation Tasks [2.2483228605450956]
  Large language models have achieved remarkable progress in text generation but still struggle with generative writing tasks.<n>We propose a fine-grained evaluation pipeline WEval for writing reward models and a fine-grained reinforcement learning training framework WRL.<n>WRL constructs positive and negative samples by selectively dropping instruction requirements, allowing for more precise reward model training.
  arXiv  Detail & Related papers  (2026-04-30T05:49:29Z)
• Model Utility Law: Evaluating LLMs beyond Performance through Mechanism Interpretable Metric [99.56567010306807]
  Large Language Models (LLMs) have become indispensable across academia, industry, and daily applications.<n>One core challenge of evaluation in the large language model (LLM) era is the generalization issue.<n>We propose Model Utilization Index (MUI), a mechanism interpretability enhanced metric that complements traditional performance scores.
  arXiv  Detail & Related papers  (2025-04-10T04:09:47Z)
• Generalization is not a universal guarantee: Estimating similarity to training data with an ensemble out-of-distribution metric [0.09363323206192666]
  Failure of machine learning models to generalize to new data is a core problem limiting the reliability of AI systems.<n>We propose a standardized approach for assessing data similarity by constructing a supervised autoencoder for generalizability estimation (SAGE)<n>We show that out-of-the-box model performance increases after SAGE score filtering, even when applied to data from the model's own training and test datasets.
  arXiv  Detail & Related papers  (2025-02-22T19:21:50Z)
• Evaluating Generative Language Models in Information Extraction as Subjective Question Correction [49.729908337372436]
  We propose a new evaluation method, SQC-Score. Inspired by the principles in subjective question correction, we propose a new evaluation method, SQC-Score. Results on three information extraction tasks show that SQC-Score is more preferred by human annotators than the baseline metrics.
  arXiv  Detail & Related papers  (2024-04-04T15:36:53Z)
• RewardBench: Evaluating Reward Models for Language Modeling [100.28366840977966]
  We present RewardBench, a benchmark dataset and code-base for evaluation of reward models. The dataset is a collection of prompt-chosen-rejected trios spanning chat, reasoning, and safety. On the RewardBench leaderboard, we evaluate reward models trained with a variety of methods.
  arXiv  Detail & Related papers  (2024-03-20T17:49:54Z)
• Evaluating Representations with Readout Model Switching [19.907607374144167]
  In this paper, we propose to use the Minimum Description Length (MDL) principle to devise an evaluation metric. We design a hybrid discrete and continuous-valued model space for the readout models and employ a switching strategy to combine their predictions. The proposed metric can be efficiently computed with an online method and we present results for pre-trained vision encoders of various architectures.
  arXiv  Detail & Related papers  (2023-02-19T14:08:01Z)
• Consistent Diffusion Models: Mitigating Sampling Drift by Learning to be Consistent [97.64313409741614]
  We propose to enforce a emphconsistency property which states that predictions of the model on its own generated data are consistent across time. We show that our novel training objective yields state-of-the-art results for conditional and unconditional generation in CIFAR-10 and baseline improvements in AFHQ and FFHQ.
  arXiv  Detail & Related papers  (2023-02-17T18:45:04Z)
• Model Rectification via Unknown Unknowns Extraction from Deployment Samples [8.0497115494227]
  We propose a general algorithmic framework that aims to perform a post-training model rectification at deployment time in a supervised way. RTSCV extracts unknown unknowns (u.u.s) We show that RTSCV consistently outperforms state-of-the-art approaches.
  arXiv  Detail & Related papers  (2021-02-08T11:46:19Z)
• Positive-Congruent Training: Towards Regression-Free Model Updates [87.25247195148187]
  In image classification, sample-wise inconsistencies appear as "negative flips" A new model incorrectly predicts the output for a test sample that was correctly classified by the old (reference) model. We propose a simple approach for PC training, Focal Distillation, which enforces congruence with the reference model.
  arXiv  Detail & Related papers  (2020-11-18T09:00:44Z)
• Explaining and Improving Model Behavior with k Nearest Neighbor Representations [107.24850861390196]
  We propose using k nearest neighbor representations to identify training examples responsible for a model's predictions. We show that kNN representations are effective at uncovering learned spurious associations. Our results indicate that the kNN approach makes the finetuned model more robust to adversarial inputs.
  arXiv  Detail & Related papers  (2020-10-18T16:55:25Z)
• Goal-directed Generation of Discrete Structures with Conditional Generative Models [85.51463588099556]
  We introduce a novel approach to directly optimize a reinforcement learning objective, maximizing an expected reward. We test our methodology on two tasks: generating molecules with user-defined properties and identifying short python expressions which evaluate to a given target value.
  arXiv  Detail & Related papers  (2020-10-05T20:03:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.