NeurIPS 2026 Papers

Conference on Neural Information Processing Systems

Decision breakdown

6,437papers

Counted from the official paper list; may differ slightly from the number the conference announced.

  • Oral
    991.5%
  • Spotlight
    2403.7%
  • Poster
    6,09894.7%

Browse all papers

Topic: Reasoning Models · 361 papers · Reset filters

Efficiently Representing Algorithms With Chain-of-Thought Transformers

Yanhong Li, Anej Svete, Ashish Sabharwal, Will Merrill

Expand abstract

The increasing popularity of *reasoning* models---language models that output a series of reasoning or thought tokens before producing an answer---is justified, in part, by theoretical results showing that chain-of-thought (CoT) transformers can simulate Turing machines, and thus perform arbitrary computation. However, the Turing machine, while suitable for a complexity theoretic analysis, isn't convenient, intuitive, or efficient when discussing algorithms. Algorithms are typically designed and analyzed at a higher level of abstraction, captured by the *Word RAM* model with random-access memory and unit-cost operations on $O(\log n)$-bit words. As a result, Word RAM algorithms can be substantially more efficient than their Turing machine counterparts, raising the question: *Can CoT transformers efficiently simulate Word RAM algorithms?* For instance, can they sort $n$ items in $O(n \log n)$ steps or run Dijkstra's algorithm in $O(E + V \log V)$ steps? We answer affirmatively, up to poly-logarithmic overhead. We first establish this for finite-precision transformers with poly-logarithmic width and rightmost unique hard attention, then strengthen the result to two more practical settings with finite width and log-precision: *continuous* CoT, where reasoning takes the form of vectors rather than tokens, and a *hybrid* architecture in which transformer layers sit atop a recurrent (linear RNN) layer. In all three cases, we find that CoT *can* efficiently simulate any Word RAM algorithm with only a poly-logarithmic overhead in $n$. This overhead reduces to log-square when the Word RAM has a ``flat'' instruction set, and only logarithmic for multiplication-free flat instructions---in stark contrast to known CoT simulations of Turing machines, which require quadratic overhead over Word RAM.

Poster
Efficient Reasoning via Constrained Optimization in Latent Space

Zhinan Hou, Xingchen Li, Keyou You

Expand abstract

Large Reasoning Models (LRMs) have shown remarkable reasoning capabilities, yet they still suffer from overthinking, generating redundant reasoning steps which incur substantial token consumption. Existing methods, such as suppressing reflective keywords or forcing shorter reasoning lengths, attempt to mitigate this issue but inevitably truncate necessary steps and induce underthinking, thereby compromising performance. To address this dilemma, we investigate the latent representations and observe that efficient reasoning steps naturally cluster into a concentrated region in latent space, while those deviating from this region tend to produce verbose sequences. To leverage this, we keep reasoning focused within this region via a quadratic program which projects deviating hidden states back into the region. Then we propose a novel training-free framework to achieve efficient reasoning that reduces token generation costs without sacrificing performance. Extensive experiments conducted on four models ranging from 1.5B to 14B, and across six benchmarks in math reasoning, coding, and scientific QA, validate the effectiveness of our method, up to a 13.4\% improvement in accuracy while reducing generated tokens by 11.8\% to 52.8\%. Code and models will be publicly available.

Poster
Early Signals, Strong Decisions: Prefix-Guided Sampling for Parallel Test-Time Scaling

Jie Ren, Jonathan S Rosenfeld, Neil Thompson

Expand abstract

Parallel test-time scaling (TTS) has been shown to enhance reasoning in large language models by generating and aggregating multiple independent reasoning paths. Internal confidence scores can further improve this process by identifying paths of varying quality. However, existing methods remain computationally inefficient, as low-quality paths are fully expanded before being evaluated. In this work, we aim to improve the use of internal confidence signals for better model performance and computational efficiency. We begin by offering a new perspective on the role of confidence in aggregation, showing that it is most impactful for questions near the decision boundary. Notably, when amplified by multi-sample aggregation, even small confidence signals derived from short prefixes can meaningfully influence outcomes in these boundary cases. Building on this insight, we introduce Prefix-Guided Sampling (PreG), a method that reallocates computation by first generating short prefixes, ranking them using internal confidence scores, and then completing only the most promising candidates. This strategy reduces token usage while maintaining gains in path quality. We provide theoretical analysis demonstrating that, under a fixed compute budget, PreG strengthens the effective signal by widening the decision boundary margin. Empirically, our method consistently outperforms standard parallel TTS approaches across benchmarks, while significantly improving token efficiency and reducing overall computation.

Poster
EVA-0: Test-Time Model Evolution with Only Two Forward Passes per Sample

Guohao Chen, Shuaicheng Niu, Geng Li, Yunbei Zhang, Shilin Shan, Chunyan Miao, Jianfei Yang

Expand abstract

Test-time model evolution offers a promising way for deployed models to improve from unlabeled test-time experience, yet most existing methods depend on backpropagation (BP), which incurs substantial memory overhead and makes them difficult to deploy on edge devices, quantized models, specialized accelerators, or black-box models. In this work, we study test-time model evolution under a strict two-forward budget, a setting that pushes adaptation toward highly efficient real-world deployment. We reveal three key obstacles in zeroth-order test-time optimization: susceptibility to shortcut solutions, uncontrolled weight drift, and ineffective update direction estimation. To overcome them, we propose EVA-0, a minimal zeroth-order adaptation framework that: 1) keeps the loss scale-invariant to prevent shortcut solutions; 2) devises an anchor-guided optimization strategy to alleviate weight drift; 3) uses sample-wise symmetric two-sided perturbation for update direction estimation and inference. EVA-0 requires no BP and performs both inference and adaptation within only two forward passes per sample. Results on ImageNet-C\&ViT-Base show that EVA-0 outperforms both BP-based DeYO and BP-free FOA, while achieving a 14$\times$ speed-up over FOA.

Poster
ESENSC: A Polynomial-Time Axiomatic Alternative to SHAP

Kazuhiro Hiraki, Shinichi Ishihara, Takumi Kongo, Junnosuke Shino

Expand abstract

We propose ESENSC, a computationally efficient and theoretically grounded alternative to SHAP. ESENSC is a polynomial-time attribution rule with a deterministic, closed-form representation that satisfies the null-player property and admits an axiomatic characterization based on efficiency, a restricted form of differential marginality, and explicit computational constraints. Empirically, ESENSC closely replicates the attribution patterns of exact SHAP by preserving its essential structural properties, while maintaining a fraction of the cost. Across neural network and XGBoost models, it achieves lower deviation and higher rank agreement than widely used sampling-based SHAP approximations. While the computational cost of exact SHAP grows exponentially with the number of features, ESENSC scales linearly, enabling reliable feature attribution in regimes where exact SHAP is intractable. These results demonstrate that ESENSC achieves near-SHAP attribution accuracy while reducing computational complexity from exponential to linear in the number of features, providing a practical and theoretically rigorous alternative for feature attribution in high-dimensional applications.

Poster
ECG-Reasoning-Benchmark: A Benchmark for Evaluating Clinical Reasoning Capabilities in ECG Interpretation

Jungwoo Oh, Hyunseung Chung, Junhee Lee, Min-Gyu Kim, Hangyul Yoon, Ki Seong Lee, Youngchae Lee, Muhan Yeo, Edward Choi

Expand abstract

While Multimodal Large Language Models (MLLMs) show promising performance in automated electrocardiogram interpretation, it remains unclear whether they perform actual step-by-step reasoning or just rely on superficial visual cues. To investigate this, we introduce **ECG-Reasoning-Benchmark**, a novel multi-turn evaluation framework comprising over 6,400 samples to systematically assess step-by-step reasoning across 17 core ECG diagnoses. Our comprehensive evaluation of state-of-the-art models reveals a systematic shortfall in executing multi-step logical deduction. Although models possess the medical knowledge to retrieve clinical criteria for a diagnosis, they exhibit consistently low success rates in maintaining a complete reasoning chain, primarily failing to ground the corresponding ECG findings to the actual visual evidence in the ECG signal. These results demonstrate that current MLLMs bypass actual visual interpretation, highlighting a limitation in their visual grounding capabilities and motivating robust, reasoning-centric medical AI. The code and data are available at https://anonymous.4open.science/r/ecg-reasoning-benchmark-anonymized-BB3C.

Poster
Does This Gradient Spark Joy?

Ian Osband

Expand abstract

Policy gradient computes a backward pass for every sample, even though the backward pass is expensive and most samples carry little learning value. The Delightful Policy Gradient (DG) provides a forward-pass signal of learning value: \emph{delight}, the product of advantage and surprisal (negative log-probability). We introduce the \emph{Kondo gate}, which compares delight against a compute price and pays for a backward pass only when the sample is worth it, thereby tracing a quality--cost Pareto frontier. In bandits, zero-price gating preserves useful gradient signal while removing perpendicular noise, and delight is a more reliable screening signal than additive combinations of value and surprise. On MNIST and transformer token reversal, the Kondo gate skips most backward passes while retaining nearly all of DG's learning quality, with gains that grow as problems get harder and backward passes become more expensive. Because the gate tolerates approximate delight, a cheap forward pass can screen samples before expensive backpropagation, suggesting a speculative-decoding-for-training paradigm.

Poster
Do Thinking Tokens Help with Safety?

Narutatsu Ri, Abhishek Panigrahi, Sanjeev Arora

Expand abstract

Today's reasoning models use thinking tokens to attain stronger performance on benchmarks than their instruction-tuned counterparts. It is also generally believed that this more "deliberative" mode should improve alignment and safety, by providing the model a safe space to consider whether its planned answer to the request violates its safety principles. We present evidence that this intuition is not always correct. Across frontier open-weight reasoning models spanning GPT-OSS, Phi, OLMo, and Qwen model families, we find that the model's decision is already strongly encoded at the beginning of thinking, with a probe on the first token's hidden representation predicting refusal/compliance with $\ge0.85$ AUROC and $\sim90$\% balanced accuracy. We also find little evidence that current models can use their thinking trace to deliberate about safety, as additional thinking after the first 20\% of the trace rarely moves the final decision. While sentence-level inspection of thinking traces may show signs of oscillation between refusal- and compliance-leaning rationales, we find that in $\geq 85$\% of thinking traces, such oscillations exert limited to no influence on the final response. We also examine the effect of existing inference-time and training-based safety interventions and find that they largely alter thinking behavior by shifting models toward more refusal-leaning reasoning while substantially reducing helpfulness on benign prompts. Our results suggest that safety behavior in current reasoning models is much less deliberative than commonly assumed, highlighting the need for training methods that more effectively utilize thinking traces for safety-critical decision making.

Spotlight
Do Reasoning LLMs Refuse What They Infer in Long Contexts?

Yu Fu, Haz Sameen Shahgir, Zhipeng Wei, Huanli Gong, N. Benjamin Erichson, Yue Dong

Expand abstract

Long-context LLMs can infer objectives that are not stated explicitly. This capability is useful for reasoning over documents, code, retrieved evidence, and tool traces, but it also creates a safety risk: harmful intent can be distributed across a context and become visible only after the model composes the relevant pieces. Existing safety evaluations mostly test explicit harmful requests, and therefore miss this failure mode. We introduce compositional reasoning attacks, a long-context threat model in which harmful requests are decomposed into semantically incomplete fragments and embedded in long contexts. The final query is neutral; the harmful objective emerges only if the model retrieves the fragments, composes them, and infers the implied goal. We instantiate this setting using AdvBench requests, varying the required reasoning from Direct Retrieval to Single-hop Aggregation, Chain Reasoning, and Multi-hop Deductive Reasoning, and evaluate 15 frontier LLMs on contexts up to 64k tokens. Models usually refuse harmful requests when they are directly retrievable. However, refusal rates drop sharply when the same objectives must be reconstructed compositionally, often with larger failures in longer contexts. Benign reconstruction and fragment-position analyses indicate that these failures are not mainly retrieval errors: models often infer the harmful objective and then comply. Increasing inference-time reasoning improves refusal but remains incomplete and costly. Our results reveal a long-context safety gap: current models are better at refusing harmful requests they see than harmful objectives they infer.

Poster
Do Deep Networks Forget Initialization? A Forgetting-Time View of Practical Inductive Bias

Mohua Das, Pierfrancesco Beneventano, Shibshankar Dey, Gareth H McKinley, Tomaso Poggio

Expand abstract

Randomly initialized neural networks induce a prior over functions, but the predictor used in practice is produced only after training. We ask how much of this initial bias survives the training pipeline. To make the question measurable, we introduce *initialization memory*: the dependence of the validation-selected predictor on the scale of the random initialization. We perform controlled CIFAR-10 experiments on ResNets where initialization memory already sharply separates training regimes. Low-learning-rate SGD can interpolate while still remembering its initialization: on ResNet-9 with batch size $b=128$, test accuracy varies by $26.5$ percentage points across initialization scales despite $\ge99.5\%$ training accuracy. This is not undertraining: extending the same low-learning-rate regime to $5{,}000$ epochs leaves the spread essentially unchanged. In contrast, Adam-family methods largely erase the dependence. SGD can also be made to forget when larger learning rates are paired with explicit $L_2$ norm control. We interpret these findings in terms of the time scale of forgetting: gradient-flow-like dynamics can preserve initialization memory, whereas stochastic finite-step effects, explicit norm decay, and adaptive preconditioning erase it on scales governed by the size of explicit or implicit regularization. The practical inductive bias of a trained network is therefore not the architectural prior alone, but the architectural prior after being filtered by the forgetting dynamics of the training pipeline; and the same regularizers that improve generalization are precisely those that erase memory of initialization.

Poster
Distilling LLM Feedback for Lean Theorem Proving

Gaëtan Narozniak, Gerard Biau, Remi Munos, Ahmad Rammal, Pierre Marion

Expand abstract

Post-training for reasoning models typically combines supervised fine-tuning with reinforcement learning from verifiable rewards, most commonly with GRPO. However, this algorithm suffers from sparse rewards, limited exploration, and mode collapse. Building upon recent works on self-distillation, we propose Feedback Distillation, a training method where the model is trained to match, at the token level, its own distribution conditioned on privileged feedback produced by a language model. Feedback Distillation offers token-level supervision and can inject external knowledge. Evaluating our method for Lean 4 theorem-proving, we find that Feedback Distillation maintains greater diversity in generated trajectories than GRPO, yielding higher policy entropy and better pass@$k$ scaling. The two methods are complementary: initializing GRPO from a Feedback Distillation checkpoint outperforms either method alone. All in all, our results suggest a promising avenue to improve post-training for complex reasoning.

Poster
Diffusion Thinking for Fast Long-Form Spatial Reasoning in Vision--Language Models

Zhitao Zeng, Weitao Du, Yueming Jin

Expand abstract

Long-form spatial reasoning in vision--language models (VLMs) is often bottlenecked by autoregressive chain-of-thought (CoT) decoding, where intermediate reasoning traces and final answers are generated token by token. This sequential decoding path makes high-quality spatial reasoning expensive in latency-sensitive embodied and interactive settings. We propose \emph{Diffusion Thinking}, a post-training framework that converts pretrained autoregressive VLMs into diffusion-style reasoners for fast long-form spatial inference without changing the visual encoder or language backbone. Diffusion Thinking partitions each CoT trace into blocks and refines tokens within the current block in parallel through discrete denoising, while preserving causal dependence across blocks and reusing KV cache for streaming generation. This creates a high-speed operating point, but aggressive parallel refinement can weaken fine-grained reasoning. To address this, we introduce \emph{Diffusion Rethinking}, a cached test-time scaling mechanism that reallocates part of the saved latency budget to self-correction rounds, yielding a controllable speed--accuracy frontier. We construct a 561K-instance Long-CoT Spatial Reasoning dataset with verified final answers and generated CoT traces across six spatial task types. Across Qwen2.5-VL and InternVL3 backbones, Diffusion Thinking with block size $D=32$ achieves 38.18--41.81$\times$ effective wall-clock speedup over autoregressive Long-CoT decoding. With eight rethinking rounds, it retains 4.20--4.60$\times$ speedup and matches or surpasses autoregressive Long-CoT accuracy on the largest backbones. These results show that diffusion-style compute reallocation is a practical path toward fast, accurate long-form spatial reasoning in VLMs.

Poster
Detect What You Need: Chain-of-Causal Reasoning for 3D Intent Grounding

Zihao Zhang, Aming WU, Yang Li, Yahong Han

Expand abstract

Accurately matching human intentions in 3D space is an important goal of artificial intelligence. Recently, 3D Intention Grounding (3D-IG) has emerged, aiming to localize target 3D objects given a natural-language intent. Unlike conventional visual grounding with descriptive referring expressions, 3D-IG intents are abstract and non-descriptive, making object localization substantially more challenging. This requires inferring latent functional requirements from non-descriptive intents and aligning them with object-level 3D representations. However, existing methods largely rely on implicit intent–object matching, leading to logical gaps and limited interpretability, robustness, and generalization. To address these challenges, we propose Chain-of-Causal Reasoning (CoCR), a causality-inspired functional dependency reasoning framework that explicitly bridges abstract intentions and candidate objects through intermediate functional requirements. Specifically, CoCR progressively decomposes complex intents into ordered functional requirements, thereby forming an explicit intent–function–object reasoning chain that links abstract intentions to object suitability. Building on this chain, we construct a causality-inspired functional dependency graph to model requirement--attribute relationships and introduce a causal-visual alignment module that aligns function-aware representations with the geometric-semantic features of 3D point clouds, enabling bidirectional verification between structured functional reasoning and visual evidence. Extensive experiments on 3D Intention Grounding and 3D Visual Grounding demonstrate that our method enhances intent-aware object localization.

Poster
Depth-Recurrent Attention Mixtures: Giving Latent Reasoning the Attention it Deserves

Jonas Knupp, Jan Metzen, Jeremias Bohn, Georg Groh, Kristian Kersting

Expand abstract

Depth-recurrence promises improved latent reasoning by sharing parameters across depths. However, prior work still relies on partially fixed layer stacks and overlooks the bottleneck of constant hidden-size; moreover, it largely lacks rigorously resource-matched ablations. To address this, we introduce depth-recurrent attention mixtures (Dreamer), a modular architecture with a single recurring layer. Concretely, we mix sequence attention, depth attention, and sparse expert attention. This alleviates the hidden-size bottleneck, decouples scaling dimensions, and achieves effective yet efficient depth-recurrence. Across natural language reasoning benchmarks at up to ~2B parameters, Dreamer requires on average ~3x fewer training tokens for the same accuracy as FLOP-, parameter-, and memory-matched modern Transformers, and outperforms ~2x larger Transformers given same training tokens. Analysis further reveals 2-11x greater expert selection diversity than conventional MoEs, highlighting the flexible knowledge sharing across depths.

Poster
Deployment-Memory LLM Test-Time Training Should Require Behavioral Evidence Beyond Perplexity

Xiangchen Song, Zhenhao Chen, Lingjing Kong, Shaoan Xie, Xinshuai Dong, Guangyi Chen, Kun Zhang

Expand abstract

Large language model test-time training (TTT) is often evaluated through local proxy metrics: models are updated on recent tokens, retrieved context, target-domain data, or verifiable task attempts, and then judged by perplexity, future-token loss, long-context performance, or reward. These metrics are well matched to claims about stream adaptation, domain adaptation, context compression, and reward-backed test-time improvement. This position paper argues that TTT has a distinct claim-calibration problem: proxy evidence for local adaptation can migrate into stronger claims about deployed assistant memory, personalization, or sparse post-deployment learning. Such claims require behavioral evidence: later recall, paraphrase robustness, retention, locality, conflict handling, and use in downstream actions after the original support context is removed. We propose a claim-calibrated evidence ladder for LLM TTT, audit recent work through this lens, and provide a diagnostic counterexample in which proxy losses improve without behavioral recall. Our goal is to give authors and reviewers a standard for aligning TTT memory claims with the evidence actually reported.

Poster
DeltaPrompts: Escaping the Zero-Delta Trap in Multimodal Distillation

Jaehun Jung, Hyunwoo Kim, Brandon Cui, Ximing Lu, David Acuna, Prithviraj Ammanabrolu, Yejin Choi

Expand abstract

Distillation enables compact Vision-Language Models (VLMs) to obtain strong reasoning capabilities, yet the prompts driving this process are typically chosen via simple heuristics or aggregated from off-the-shelf datasets. We reveal a critical inefficiency in this approach: up to 69\% of the prompts in standard chart / document reasoning datasets are effectively $\textit{zero-delta}$, meaning the teacher and student already induce the exact same answer distribution. Training on these prompts provides minimal learning signal, causing student improvement to rapidly saturate regardless of data scale. To escape the zero-delta trap, we return to first principles: distillation fundamentally minimizes distributional divergence, and thus a prompt is valuable only if it exposes a functional capability gap between the teacher and student. We quantify this gap through $\textit{answer divergence}$ ($\Delta$), demonstrating that non-zero divergence is critical for effective scaling. Building on this insight, we propose a staged synthesis pipeline that repurposes existing datasets as seeds, actively targeting student failure modes to produce better prompts. The result is $\textbf{DeltaPrompts}$, a diverse dataset of 200k synthetic, high-divergence reasoning problems. We evaluate $\text{DeltaPrompts}$ across three distinct settings: on-policy distillation with the target teacher-student pair, transfer to a novel model family without regenerating the data, and off-policy fine-tuning of a non-reasoning model. Across all scenarios, $\text{DeltaPrompts}$ drives substantial gains, yielding up to 15\% relative improvement even on top of a highly-optimized reasoning model ($\textit{e.g.,}$ Qwen3-VL-8B-Thinking)---averaged over 10 benchmarks spanning chart, document and perception-centric reasoning.

Spotlight
Decoupled Descent: Exact Test Error Tracking Via Approximate Message Passing

Max Lovig

Expand abstract

In modern parametric model training, full-batch gradient descent (and its variants) suffers due to progressively stronger biasing towards the exact realization of training data; this drives the systematic ``generalization gap'', where the train error becomes an unreliable proxy for test error. Existing approaches either argue this gap is benign through complex analysis or sacrifice data to a validation set. In contrast, we introduce decoupled descent (DD), a novel theory-based training algorithm that satisfies a train-test identity---enforcing the train error to asymptotically track the test error for stylized Gaussian mixture models. Within this specific regime, leveraging approximate message passing theory, DD iteratively cancels the biases due to data reuse, rigorously demonstrating the feasibility of zero-cost validation and $100\%$ data utilization. Moreover, DD is governed by a low-dimensional state evolution recursion, rendering the dynamics of the algorithm transparent and tractable. We validate DD on XOR classification, yielding superior performance compared to GD; additionally, we implement noisy MNIST and non-linear probing of CIFAR-10, demonstrating that even when our stylized assumptions are relaxed, DD narrows the generalization gap compared to GD.

Poster
Decoding the Critique Mechanism in Large Reasoning Models

Hoang Phan, Nguyen Hung-Quang, Thanh Quoc Hung Le, Xiusi Chen, Heng Ji, Khoa D Doan

Expand abstract

Large Reasoning Models (LRMs) exhibit backtracking and self-verification mechanisms that enable them to revise intermediate steps and reach correct solutions, yielding strong performance on complex logical benchmarks. We hypothesize that such behaviors are beneficial only when the model has sufficiently strong “critique” ability to detect its own mistakes. This work systematically investigates how current LRMs recover from errors by inserting arithmetic mistakes in their intermediate reasoning steps. Notably, we discover a peculiar yet important phenomenon: despite the error propagating throughout the entire chain-of-thought (CoT) without any verbalized correction, the model still reaches the correct final answer after the thinking process finishes. This recovery implies the existence of an internal mechanism helping the model to detect errors and trigger self-correction, which we refer to as the hidden critique ability. Building on feature space analysis, we identify a highly interpretable critique vector representing this behavior. Extensive experiments across multiple model scales and families demonstrate that steering latent representations with this vector improves the model’s error detection capability and enhances the performance of test-time scaling at no extra training cost. Our findings provide a valuable understanding of LRMs’ critique behavior, suggesting a promising direction to control and improve their self-verification mechanism.

Poster
Data Diversity Drives the Emergence of Symbolic Mechanisms Supporting Abstract Reasoning

Melody Li, Taylor Webb

Expand abstract

Recent work has identified a set of emergent symbolic mechanisms that support abstract reasoning in large language models, but it remains unclear what factors drive the emergence of these mechanisms. To address this question, we trained neural networks from scratch on abstract sequence tasks, varying both architectural and data distributional factors, and investigated the effects of these factors on the emergence of symbolic mechanisms. Using a combination of representational, attentional, and casual mediation analyses, we first confirmed that transformer language models trained from scratch on our task developed symbolic mechanisms, partially capturing the set of mechanisms learned by large-scale pretrained models. We then investigated the effect of data diversity, operationalized as vocabulary size, on the emergence of these mechanisms, finding that mechanistic and behavioral signatures of emergent symbol processing scaled with data diversity, including downstream measures of systematic (i.e., out-of-distribution) generalization. Surprisingly, we found that the emergence of symbolic mechanisms was not driven by architectural inductive biases, as the same mechanistic and behavioral signatures emerged in modified transformer architectures and even multilayer perceptrons. These results suggest that data diversity, rather than architectural inductive biases, is the primary driver of emergent symbolic computation in neural networks.

Poster
Curriculum proof repair with learned counterexamples

Yuechun Sun, Jun Yang, Kexin Pei

Expand abstract

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.

Poster