Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.21881

Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Lazar Milikic·Etienne Bamas·Emmanuel Abbe·Viktor Kunčak
View original source ↗Read source document ↗Export metadata ↓

Abstract

Training language models for formal theorem proving requires large numbers of verifier calls. Slow checks and timeouts often leave GPUs waiting and withhold rewards from potentially correct proofs. We train neural evaluators to predict Lean 4 verdicts and compiler feedback on GPUs using 4.84M labelled programs. We compare two validity classifiers with a feedback model that annotates proof attempts with predicted goal states and error messages. A two-stage evaluator that screens candidates with a classifier and scores its positive predictions with the feedback model reaches 87.8% accuracy in predicting whether Lean accepts a candidate proof, evaluated on a 68,932-program benchmark collected from public provers. The combined evaluator processes 3.5 candidates per second on one H100, 4.2x the throughput of our 64-worker Lean baseline with environment reuse. Finally, we combine our evaluator with Lean verdicts to obtain a hybrid reward system that shortens GRPO training steps by approximately 31%. After one GRPO epoch with hybrid rewards, the prover achieves nearly the same miniF2F pass@1 as with Lean-only rewards (62.2% versus 62.4%) and a pass@32 of 72.4% versus 71.3%.

Explore related subjects

cs.LG

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Lazar Milikic, Etienne Bamas, Emmanuel Abbe, Viktor Kunčak. 2026-10-15. Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs. https://arxiv.org/abs/2610.21881

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Heterogeneous Sheaf Neural Networks

Heterogeneous graphs, whose nodes and edges can belong to different types and feature spaces, arise in many real-world domains, including biology, recommendation, social networks, and computer systems. Existing heterogeneous graph neural networks typically handle this heterogeneity at the architectural level through relation-specific modules, meta-path machinery or type-aware attention, which often leads to increasingly specialised parameter-heavy designs. In this work, we propose HetSheaf, a framework for learning heterogeneous graphs through cellular sheaves. Instead of encoding heterogeneity solely in the architecture, HetSheaf represents it directly in the underlying data structure by assigning type-aware local feature spaces and learning restriction maps conditioned on node features, node types, and edge types. To support graph-level prediction, we further introduce SheafPool, a universal stalk-space readout that aggregates node representations while being invariant to local changes of basis, thereby making graph classification with sheaf networks well-defined and achieving an F1 Score up to 42 percentage points higher than mean pooling. Across a diverse suite of benchmarks (node classification, link prediction and graph classification). HetSheaf consistently achieves up to 2 percentage points higher performance (up to 94.97% Macro F1 Score on node classification and up to 99.62% on link prediction) on the Heterogeneous Graph Benchmark (HGB) framework against homogeneous (GCN, GAT, GIN, GraphSAGE), heterogeneous (R-GCN, HAT, HGT) and type-agnostic sheaf baselines, while reducing the number of parameters by up to 10$\times$.

cs.LG↗
arXiv2026

Risk-averse learning with delayed feedback

In real-world scenarios, risk-averse learning is valuable for mitigating potential adverse outcomes. However, the delayed feedback makes it challenging to assess and manage risk effectively. In this paper, we investigate risk-averse learning using Conditional Value at Risk (CVaR) as risk measure, while incorporating feedback with random but bounded delays. We develop two risk-averse learning algorithms that rely on one-point and two-point zeroth-order optimization approaches, respectively. The dynamic regrets of the algorithms are analyzed in terms of the cumulative delay and the number of total samplings. In the absence of delay, the regret bounds match the established bounds of zeroth-order stochastic gradient methods for risk-averse learning. Furthermore, the two-point risk-averse learning outperforms the one-point algorithm by achieving a smaller regret bound. We provide numerical experiments on a dynamic pricing problem to demonstrate the performance of the algorithms.

cs.LG↗
arXiv2026

On the Value of Cross-Modal Misalignment in Multimodal Representation Learning

Multimodal representation learning, exemplified by multimodal contrastive learning (MMCL) using image-text pairs, aims to learn powerful representations by aligning cues across modalities. This approach relies on the core assumption that the exemplar image-text pairs constitute two representations of an identical concept. However, recent research has revealed that real-world datasets often exhibit \emph{cross-modal misalignment}. There are two distinct viewpoints on how to address this issue: one suggests mitigating the misalignment, and the other leveraging it. We seek here to reconcile these seemingly opposing perspectives and to provide a practical guide for practitioners. Using latent variable models, we thus formalize cross-modal misalignment by introducing two specific mechanisms: \emph{selection bias}, where some semantic variables are absent in the text, and \emph{perturbation bias}, where semantic variables are altered---both leading to misalignment in data pairs. Our theoretical analysis shows that, under suitable assumptions, population global minimizers of an alignment--entropy surrogate yield representations that depend only on the semantic variables unaffected by selection and perturbation biases and locally identify this subset almost surely. Extensive empirical studies on synthetic data and real image-text datasets further examine how cross-modal misalignment shapes semantic predictability and downstream performance, shedding light on its nuanced impact on multimodal representation learning.

cs.LG↗