NeurIPS 2026 Papers

Formal verification provides strong correctness guarantees, but proof development remains difficult because developers must diagnose coarse verifier errors and repair failed proof obligations. Recent approaches leverage language models (LMs) to improve proof automation through verifier-in-the-loop repair, but they often rely on hand-engineered prompts, retrieved examples, or sparse pass/fail feedback. We present \tool, an LM-based framework for Verus proof repair that internalizes counterexample-guided diagnosis as a model capability. Our key insight is to train counterexample generation not as a standalone validation task, but as a data-driven diagnostic objective: a counterexample is useful when conditioning on it helps the model produce a safe, verifier-passing proof. Given a failed Verus proof and verifier error, \tool generates a structured source-level counterexample, repair rationale, and repaired proof in one trajectory, optimized with reinforcement learning from Verus feedback and a proof-code safety gate. To address sparse and order-sensitive credit assignment, \tool introduces a topological graph reward that derives invariant dependencies from inductiveness tests and encourages counterexample generation following the same topological order as the invariant dependencies. Across seven Verus benchmarks with 471 problems, \tool achieves 61.6\%/72.2\% weighted-average Safe-Pass@1/Safe-Pass@3, outperforming the strongest baseline, Claude Sonnet 4.5, by 5.7/6.3 points. We also show that \tool's learned counterexample can directly augment the reasoning of existing LM-based proof repair approaches, improving their success rate by 64.3\% compared to using the chain-of-thought diagnostics.

AI systems operating near the limits of their capabilities can maximize utility while minimizing the risk of error by abstaining or deferring questions they are not confident about to a human or a stronger model. Recently, large language models (LLMs) have been post-trained to estimate confidence in their own answers. To achieve this, methods reinforce confidence scores based on the correctness signal to each question-answer pair \emph{individually}, with rewards that encourage assigning confidence 1 to correct answers and 0 to incorrect answers. However, estimating confidence scores is useful in that it enables selecting only the most confident answers, to maximize the share of solved questions while accommodating the user's risk tolerance. Assigning confidence 1 to correct answers and 0 to incorrect ones is theoretically optimal, but unattainable in practice and detrimental for selective prediction with a non-zero risk tolerance: confidences pushed to 0 and 1 carry no information about how answers compare to one another. We therefore introduce \ours (Cross-question Abstention Reward Estimation), which computes rewards over a set of question-answer pairs: At each of several risk tolerances, the confidences across the set induce an abstention threshold, and each confidence is rewarded for lying on the correct side of it. Since the threshold itself comes from the set, every verbalized confidence is reinforced relative to other questions' confidence, not against its own binary correctness label. On math, \ours increases the coverage at 5\% risk (C@5) across MATH-500, GSM8K, and Big-Math-Digits from 0.8\% to 42.4\%, compared to existing pointwise correctness-matching rewards. When trained on multi-hop Wikipedia QA from HotpotQA, \ours improves C@5 in out-of-distribution general-knowledge, reasoning, and math benchmarks (including CommonsenseQA, GPQA, SimpleQA, and TriviaQA) from 9.9\% to 23.6\%.

Reinforcement learning with verifiable rewards (RLVR) post-trains language models on multi-step reasoning by assigning a single outcome reward uniformly across all tokens in a trajectory, regardless of which steps contributed to success or failure. Improving credit assignment can address this limitation by enabling targeted refinement of faulty reasoning steps, rather than updating entire trajectories uniformly. Resets are one such simple mechanism, enabling more precise credit assignment by returning to an intermediate state and resampling its continuation, so that outcome differences can be attributed to decisions made at that point. We propose two such methods: Random-Reset Policy Optimization (RRPO), where reset states are drawn randomly from reasoning steps, and Self-Reset Policy Optimization (SRPO), where the model self-localizes the erroneous step in an incorrect trajectory and resets there. We analyze these methods within a Conservative Policy Iteration (CPI) framework. We extend it with a credit-assignment oracle that targets improvable states, defined as those whose advantage exceeds a threshold, and show that it yields provable improvements over random resets. Across models and reasoning benchmarks, SRPO consistently outperforms standard GRPO and RRPO by sampling multiple suffix continuations at a self-localized reset and learning from their rewards, using only the model itself with no external supervision.

Building hydrogen station networks, electric vehicle (EV) charging grids, or vaccine distribution systems requires coordinating two separately operated graphs - demand-side facilities and the supply-side networks they depend on - where each operator's payoff depends on the other's choices. We formalize this as the Co-Evolving Graph Game (CEGG), a setting that sits between facility location, interdependent-network analysis, and graph-based multi-agent reinforcement learning (MARL) but is not jointly addressed by any of them. We propose Cross-Graph Attention with Policy Mirror Descent (CGA-PMD), pairing cross-graph attention - which lets each agent read only the partner-graph nodes structurally coupled to its own - with a policy mirror descent update for stable training. Across three reward domains and a range of practical network scales, we find that the structure of the coupling selects which method wins: at small scale most methods are competitive, but as scale grows or coupling becomes irregular, only CGA-PMD remains productive while own-only, unmasked-attention, and Proximal Policy Optimization (PPO)-based variants all fail in distinct ways. Our theoretical analysis explains why: PMD's Kullback-Leibler (KL) regularization admits an iteration-uniform cumulative drift bound while PPO's clip update does not, predicting CGA-PMD's stability in the hard regime where PPO-based methods collapse.

Reinforcement learning has rapidly become the dominant paradigm for training software engineering (SWE) agents on long-horizon, multi-turn tasks such as resolving real-world GitHub issues. Yet existing pipelines suffer from a fundamental credit-assignment bottleneck: rewards arrive only at the end of trajectories that may span dozens of file edits, shell commands, and test invocations, leaving every intermediate decision indistinguishable from luck. We observe that containerised SWE tasks provide a particularly useful form of environment forkability: a commit hash plus a container image specifies a real executable software state that can be restored cheaply and exactly, with auditable provenance and without a simulator-to-reality gap. We exploit this property by introducing Counterfactual Rollout Replay (CRR), a training-time procedure that re-executes the environment from selected decision points with alternative actions and assigns each selected step an advantage equal to the sampled on-policy versus counterfactual return differential. CRR requires no learned process reward model, no human rubric annotation, and no oracle hindsight signal; it is free of auxiliary process labels and reward-model training, while still incurring extra environment-replay compute. Applied to a 14B base model on SWE-Gym and evaluated on SWE-bench Verified and SWE-rebench, CRR-trained agents reach higher resolution rates with substantially fewer trajectories than outcome-only GRPO and complement orthogonal advances such as PRM-based scoring and trajectory search.

Large language models are increasingly deployed as autonomous agents that plan and act over long-horizon interactions, learning from both final outcomes and rich environmental feedback. However, optimizing from such interaction experience remains challenging, as feedback is heterogeneous and rarely carries explicit reward information. Existing post-training approaches rely on outcome-driven methods, such as reinforcement learning with verifiable rewards (RLVR), which primarily exploit final success signals while leaving interaction experience and feedback underutilized. In sparse-reward, long-horizon tasks, this often results in **distribution sharpening**: the policy reinforces a narrow set of already-successful behaviors, without substantially improving the feedback-grounded agency needed for broader problem-solving capacity (e.g., Pass@$k$). We propose ***Counterfactual Distillation***, a framework that converts exploration-derived experience into trainable policy supervision. Specifically, we organize exploration as a tree-structured search process, where the agent reflects on past decision points and makes new experience-guided decisions to form alternative branches. These corrections are then distilled as counterfactual targets: we train the model to predict the revised action from the original history without explicitly providing the experience, thereby introducing out-of-distribution behavior patterns and expanding exploration capacity. Across diverse interactive coding and agentic tasks, our method outperforms outcome-driven baselines such as GRPO and experience-based methods such as Early Experience, with gains of up to **14%** on Pass@128. When interleaved with reinforcement learning updates, it further raises the performance ceiling, yielding over **10%** improvement in Pass@1. We provide an [anonymized implementation](https://anonymous.4open.science/r/Counterfactual-Distillation-0E71).

We consider the problem of Cost-Aware Learning, where sampling different components of a finite-sum objective incurs different costs. The objective is to reach a target error while minimizing the total cost. We propose Cost-Aware SGD, which uses a distribution based on gradient norms and costs to sample components. We provide a thorough analysis of this algorithm, including cost-improvement bounds over baselines, a characterization of distribution proxy sub-optimality, and a lower bound. We apply our theoretical insights to reinforcement learning with language models, where the computational cost of sequence-level policy gradients varies with length. We find that the advantage magnitude serves as a high-fidelity proxy for gradient norms, and use this to introduce Cost-Aware GRPO. Empirical results on 1.5B, 4B, and 8B LLMs demonstrate that this algorithm significantly reduces the tokens used in policy optimization while matching or exceeding baseline accuracy.

In tool-integrated reinforcement learning with verifiable rewards (RLVR), sequence-level verifier signals are issued for trajectories whose outcomes are determined by a sparse subset of tokens—tool names, argument keys, and argument values. Standard RLVR assigns the same advantage to every token in a rollout, diluting credit at precisely the positions that matter. We propose **Correctable Fork Tokens (CFT)**, which decomposes selective credit assignment into two subproblems: *where* to update, and *how much* to update at those positions. To this end, CFT introduces a training-only answer-conditioned branch sharing parameters with the student policy. The key insight is that conditioning on the ground-truth answer concentrates the model's distribution at decision-fork positions, providing hindsight localization without additional parameter capacity or imitation targets. Critically, this benefit requires accurate answer information: a larger-capacity teacher without the answer fails to replicate these gains, confirming that privileged answer information—not teacher capacity—is the active ingredient. CFT uses this entropy reduction ($IG_t$) to identify correctable fork positions, then rescales token-level credit at those positions while preserving the verifier advantage as the sole signal for update direction. On BFCL v3/v4, CFT improves multi-turn accuracy by **4.2/6.5** pp and overall accuracy by **3.1/2.2** pp over GRPO; it further surpasses On-policy distillation—which employs a larger Expert Model as teacher—by **3.6/6.7** pp on multi-turn, confirming that answer-conditioned fork localization rather than teacher capacity drives the improvement. On Tau3, the average score improves by **8.3** pp. We additionally present a three-level structured verifier for tool-call settings; ablations confirm that finer-grained verifier feedback and selective token credit are complementary. Our reproducible implementation is available at [https://anonymous.4open.science/r/CFT](https://anonymous.4open.science/r/CFT).

Human labels are important supervisory signals for preference-based reinforcement learning, but their collection is often constrained by practical considerations that standard training objectives tend to ignore. For instance, Direct Preference Optimization (DPO) usually treats observed preference labels as clean, even though real annotation pipelines rely on heterogeneous annotators whose reliability varies across individuals and with the difficulty of each comparison. This setting introduces three challenges: (1) Noisy labels introduce systematic bias into the preference optimization objective and need to be rigorously corrected. (2) The allocation of pairwise comparisons to different annotators is a design problem that directly affects the statistical efficiency of the training pipeline. (3) Non-random routing creates selection bias in annotator evaluation, complicating downstream decisions such as compensation. We address these challenges within a unified framework for DPO that combines annotator-aware posterior correction with information-guided annotator routing. Posterior correction leverages an instance-dependent noise model to infer latent ground-truth preferences from noisy labels, mitigating bias in the DPO objective. Annotator routing is formulated as an optimal experimental design problem that allocates comparisons to annotators according to their expected statistical information under a fixed annotation budget. To support reliable annotator evaluation under non-random routing, we introduce a doubly robust estimator that corrects for selection bias. Semi-synthetic experiments on the UltraFeedback dataset show that our approach improves ground-truth preference recovery and downstream AlpacaEval 2 performance over baselines, with consistent gains across multiple open-source LLM model architectures. Annotator reliability-estimation experiments further show that the doubly robust estimator substantially reduces mean squared error relative to other baselines, demonstrating its value for annotator evaluation.

While recent work in Reinforcement Learning with Verifiable Rewards (RLVR) has shown that a small subset of critical tokens disproportionately drives reasoning gains, an analogous token-level understanding of On-Policy Distillation (OPD) remains largely unexplored. In this work, we investigate high-loss tokens, a token type that—as the most direct signal of student-teacher mismatch under OPD's per-token KL objective—should progressively diminish as training converges according to existing studies; however, our empirical analysis shows otherwise. Even after OPD training reaches apparent saturation, a substantial subset of tokens continues to exhibit persistently high loss; these tokens, which we term Rock Tokens, can account for up to 50\% of the tokens in generated outputs. Our investigation reveals two startling paradoxes. First, despite their high occurrence frequency providing a disproportionately large share of total gradient norms, Rock Tokens themselves remain stagnant throughout training, resisting teacher-driven corrections. Second, through causal intervention, we find that these tokens provide negligible functional contribution to the model's actual reasoning performance. These findings suggest that a vast amount of optimization bandwidth is spent on structural and discourse residuals that the student model cannot or need not internalize. By deconstructing these dynamics, we demonstrate that strategically bypassing these "stumbling blocks" can significantly streamline the alignment process, challenging the necessity of uniform token weighting and offering a more efficient paradigm for large-scale model distillation.

Mode connectivity studies reveal that high-performing neural networks are often connected by low-loss paths in parameter space. We investigate the analogue of this phenomenon in cooperative multi-agent reinforcement learning (MARL), where a solution is not a single model but a team of decentralized policies. We introduce coordination connectivity, a diagnostic evaluating whether linear interpolation between the actor parameters of two trained policy teams preserves high team return. The resulting coordination barrier measures whether two successful teams are separated by a performance cliff along the joint-policy path. We evaluate this diagnostic on the StarCraft Multi-Agent Challenge (SMAC) across five controlled training histories, isolating the effects of shared initialization, continued training, parameter decoupling, and HAPPO-style separate-actor specialization. Across three SMAC maps and four seeds, policy teams derived from a shared MAPPO checkpoint exhibit near-zero interpolation barriers, even after non-shared specialization. In contrast, interpolation paths involving independently trained HAPPO teams exhibit substantially larger barriers. Mixed-team assembly, single-agent hot-swap, clone-all, role-swap, and weight-space probes further indicate that shared-initialized agents specialize into distinct roles while remaining within a low-barrier coordination component. These results suggest that shared initialization implicitly structures the joint-policy space of cooperative MARL, providing a mode-connectivity-inspired lens for analyzing coordination, specialization, and same-source cross-version team compatibility.

Multi-Agent Reinforcement Learning (MARL) is a powerful approach to large-scale systems control, such as power grids and traffic networks, where dozens to hundreds of agents must coordinate effectively. Furthermore, such systems often operate in digital or simulated settings, which allows for inference-time search to significantly improve upon zero-shot performance. A current leading approach in this setting is COMPASS, which builds a continuous family of policies conditioned on latent vectors that can be efficiently searched at test time, but requires all agents to share a single latent vector, limiting the space of reachable joint policies. We introduce ATLAS, a simple extension in which each agent conditions on its own latent vector while still optimising a joint objective. This expands the searchable policy space at negligible computational cost and requires no additional training. ATLAS consistently sets a new state-of-the-art on a benchmark of 14 scenarios across three environments, scaling to teams of up to 200 agents, widely out of distribution. Crucially, its lead sharpens with team size and compute, reaching up to a 45% performance gain at scale.

Discovering cooperative behavior in multi-agent reinforcement learning (MARL) is challenging due to the combinatorial complexity of joint state-action spaces, which hinders the emergence of coordinated behaviors from trial-and-error alone. Intrinsic rewards are often used to aid discovery, but naively combining them with team objectives can distort the learning signal, compromising task performance. In this paper, we propose EFXPLORER, a constrained exploration framework that maximizes exploration objectives subject to a constraint that preserves established task performance. We solve it via an epigraph reformulation that introduces adaptive exploration budgets. This approach separates intrinsic rewards from task objectives and regulates exploration through task feasibility. To further encourage diverse and temporally extended exploration, we incorporate a successor distance-based intrinsic reward that captures long-horizon dependencies. Empirically, our method outperforms strong baselines and induces novel cooperative strategies across SMAX, VMAS, and MPE benchmark suites.

The rapid growth of video-based social media has increased users’ exposure to harmful content, creating a need for reliable automated video safety detection. Although recent Vision-Language Models (VLMs) show strong video understanding capabilities, existing harmful video detection systems face two key limitations: they typically reduce safety detection to binary classification, overlooking the inherently multi-label nature of unsafe videos, and they rely on static training objectives that do not support controllable precision-recall trade-offs, though the desired operating point may vary across moderation pipelines and unsafe categories. To address these gaps, we propose Adaptive Tversky Policy Optimization (ATPO), a reinforcement learning framework for Multi-label Video Safety Detection (Multi-VSD). ATPO introduces the Adaptive Tversky Reward (ATR), which dynamically adjusts false-positive and false-negative penalties during training to enable controllable precision–recall trade-offs. Experiments on SafeWatch-Bench and XD-Violence show that ATPO substantially improves multi-label performance, increasing the Jaccard Index from 40.66 to 75.44 on SafeWatch-Bench-Real. Moreover, ATR enables reliable steering of the precision–recall operating point, supporting deployment scenarios with heterogeneous policy requirements.

Despite the success of foundation models in language and vision, molecular graph generation still lacks a unified framework for heterogeneous design tasks with reliable controllability. While reinforcement learning (RL) offers a natural post-training mechanism for task-specific optimization, applying it to graph generative models is hindered by the vast atom-wise action spaces and chemically invalid intermediate states. We propose \textbf{Co}ntrollable \textbf{Mole}cular Generative Foundation Models (CoMole), built with a unified motif-aware graph diffusion pipeline. By learning a motif-aware graph space, CoMole transfers pretrained structural priors into controllable generation, where RL optimizes conditional reverse policies over chemically meaningful decisions. We theoretically characterize the bottleneck of atom-level RL and justify motif-aware policy optimization. Across three heterogeneous benchmarks spanning materials and drug discovery, CoMole ranks first in controllability on all nine targets, reduces MAE by up to 48.2\% relative to the strongest baselines, and maintains validity above 0.94 without rule-based correction or post-hoc filtering. We further show that CoMole transfers controllability to unseen properties by optimizing only task embeddings with the generator frozen, achieving performance competitive with strong task-specific baselines.

Visual reinforcement learning (RL) is promising for real-world problems such as autonomous driving, robotic locomotion, and manipulation, but remains highly vulnerable to visual distribution shifts between training and deployment. Existing methods improve robustness through Q-consistency regularization, masking, and auxiliary objectives, yet most of them follow a coupled representation learning paradigm in which control-oriented and robustness-oriented representation learning are jointly optimized within the same training framework. We argue that this coupled structure can introduce harmful interference between control learning and robustness learning, degrading original-environment control performance and limiting generalization under visual shifts. To address this issue, we propose Separate Then Align Representations (STAR), which reformulates visual RL generalization as a problem of decoupled representation learning. Specifically, we first learn a control-relevant reference representation through online RL under weak augmentation, and then perform an offline post-representation alignment stage that maps strongly augmented inputs back to this reference representation. Experiments on RL-ViGen benchmarks spanning DMControl and Robosuite show that STAR achieves strong generalization under visual distribution shifts while better preserving performance in the original environment than prior coupled approaches. Our source codes are available in the supplementary material.

In-context reinforcement learning (ICRL) has emerged as an effective paradigm for test time adaptation to unseen tasks without parameter updates. However, existing ICRL methods can exhibit brittle and unstable adaptions, and the mechanisms underlying such adaptions remain poorly understood. We provide a policy-gradient view of ICRL and argue that relying on trajectory-level return feedback can lead to high-variance updates when test time rollout is limited. Motivated by the actor--critic principle, we propose **Context Value Informed ICRL (CV-ICRL)**, which equips the in-context policy with an explicit *context value*: the expected discounted return conditioned on the current state and accumulated interaction context. CV-ICRL trains a value head and writes its prediction back into the context as a value token, enabling TD-style return targets for lower-variance policy updates. Experiments on the Dark Room, Minigrid, and Procgen testbeds show that CV-ICRL substantially improves the stability of test time adaptation and achieves higher returns across tasks and environments. The source code and data of this paper are available at https://anonymous.4open.science/r/CV-ICRL-D161.

Planar graphs are central to applications across science and engineering, yet existing generators provide limited support for goal-directed generation under hard structural and geometric feasibility constraints. We propose a dataset-free method for generating planar graph embeddings by combining parametric graph grammars with safe reinforcement learning to optimize generic task-specific objectives while satisfying constraints during construction. We formulate the generation process as a constrained Markov decision process, where the graph grammar defines the state and action spaces. We further introduce an action projection that maps sampled actions toward state-dependent safe sets, improving constraint satisfaction during training. In contrast to classical graph generators and deep generative models, which typically offer limited goal-directed control or rely on weak constraint satisfaction, our method constructs feasible planar graph embeddings directly during generation. We also introduce a benchmark suite for constrained and goal-directed planar graph generation, together with classical and deep generative baselines. Across all benchmark tasks, our method consistently outperforms baselines while satisfying the formulated constraints.

Offline multi-objective optimization aims to identify high-quality trade-off designs using only a fixed dataset of previously evaluated candidates. Existing methods often cast this problem as guided generative sampling, producing a finite candidate pool by steering a diffusion or flow model toward Pareto-preferred regions. We study a different interface: deterministic Pareto set amortization. Our method, Offline Pareto Set Learning (OffPSL), trains a preference-conditioned map $h_\pi:\Delta^{m-1}\rightarrow \mathcal{X}$ that returns one design for each requested trade-off direction. Because offline data contain no preference–solution labels, OffPSL trains this map using two offline-only signals: a coordinate-wise pessimistic surrogate scalarization and a diffusion-style denoising-residual support regularizer learned from offline designs. The denoising model is used only as a frozen support prior and is not used to sample candidates. At inference, OffPSL produces exactly one candidate per reference direction with no iterative sampling, test-time optimization, or filtering from a larger generated pool. On standard offline MOO benchmarks, OffPSL is competitive with recent guided generative baselines while keeping the learned preference-to-design map directly queryable and diagnosable.