NeurIPS 2026 Papers

Recent progress in neural theorem proving has been driven largely by mathematics-oriented and, more recently, by verification-condition and repository-scale benchmarks. These settings are valuable, but they do not directly test whether a model can synthesize machine-checkable proofs about concrete low-level implementations under an industrial proof-engineering stack. We address this gap with *s2n-bignum-bench*, a benchmark derived from AWS *s2n-bignum*, a formally verified library of hand-tuned big-integer assembly routines for ARM and x86. The current corpus packages $\mathbf{2{,}301}$ HOL Light proof obligations as standalone `setup.ml`/`query.txt` tasks spanning big-integer arithmetic, elliptic-curve routines, ML-KEM, SHA-3/Keccak, and shared ISA infrastructure. Each task reproduces the relevant proving environment, exposes the theorem statement to be proved, and expects a tactic expression that is accepted by HOL Light within a fixed timeout. The benchmark spans five categories so that one can separate generic HOL Light fluency from ISA-specific reasoning. We release the extraction pipeline, retrieval utilities, an offline evaluator with syntax/type pre-checking and integrity checks based on axiom-difference and forbidden-tactic detection, paired verbatim and obfuscated query variants, and a checkpointed assessment workflow to support iterative feedback-driven $\operatorname{pass}@K$ studies and future step-level proof construction workflows. Initial zero-shot baselines using GPT-5.3-based and other frontier models solve at most $\mathbf{6.35}$% of the problem set (when provided only with the goal term), highlighting the difficulty of HOL Light tactic synthesis for low-level verification obligations under trusted ISA semantics. The code to set up and use the benchmark is available at [s2n-bignum-bench](https://github.com/kings-crown/s2n-bignum-bench).

Millimeter-wave (mmWave) radar provides core sensing capabilities to traditional vision, particularly under occlusion, low-light, and privacy-constrained conditions. Recent efforts have explored integrating radar signals with large language models (LLMs) for high-level semantic reasoning over the received radar data. However, existing approaches typically project radar inputs into borrowed vision or LiDAR embedding spaces, which are not tailored to radar-specific physical cues such as Doppler and reflection intensity. This design introduces a representational bottleneck, hindering the extraction of informative radar semantics. To overcome this limitation, we propose \textbf{mmLIP}, a novel radar-language interactive pretraining framework that learns radar-specific alignment without relying on external embedding spaces. Our approach directly aligns radar representations with the text embedding space via a point-level contrastive objective, enabling fine-grained correspondence between radar points and textual tokens. In addition, we introduce a confidence-aware contrastive learning mechanism that adaptively reweights radar tokens based on their semantic relevance, promoting informative signals while suppressing clutter. Supported by our newly curated radar-text pairs, mmLIP captures structured radar semantics. Extensive experiments demonstrate that mmLIP successfully integrates with diverse LLMs or vision-language models, achieving state-of-the-art performance on zero-shot bidirectional retrieval as well as text generation tasks, including captioning and question answering.

Higher-order learning exploits compositional features whose predictive value arises from nonlinear interactions beyond pairwise relations among variables, scales, or modalities. To address the complexity of modeling higher-order interactions in modern large-scale deep learning models, a kernelized Volterra Neural Network (kVNN) is proposed in this paper. Specifically, the proposed learnable multi-kernel representation models different interaction orders using distinct polynomial-kernel components with compact learnable centers, thereby yielding an order-adaptive parameterization. The resulting kVNN layers are composed of parallel order-specific branches and can readily replace standard convolutional kernels in existing learning architectures. Theoretical results are supported by experiments on video action recognition, image denoising, and image classification. The results show marked performance-efficiency trade-offs: kVNN consistently reduces model (parameters) and computational (GFLOPs) complexity while achieving competitive and often improved performance, even when trained from scratch without large-scale pretraining. In summary, structured kernelized higher-order layers offer a practical path to balancing expressivity and computational cost in modern deep networks.

Deep Equilibrium Models (DEQs) are an established framework for image restoration that learn a problem-adapted regularization by solving a fixed-point (i.e. equilibrium) problem. While flexible and expressive, DEQs are often hindered by high computational cost and training instability. We propose an inertial DEQ (i-DEQ) that learn an explicit nonconvex regularization within the DEQ formulation. By using momentum within the fixed-point iterations, i-DEQ has convergence guarantees and accelerated rates. Moreover, we observe that i-DEQ is significantly more stable during the training and robust to rough initialization than DEQs. Numerical experiments on various linear and nonlinear inverse problems demonstrate that i-DEQ achieves reconstruction quality comparable to state-of-the-art methods, while reducing DEQ's inference time by a factor of two.

Influence functions are a popular tool for measuring the impact of a training point on a model's prediction; in particular, self-influence, which quantifies the influence of a training point on itself, has found many uses such as data selection and outlier detection. However, the use of influence functions has been severely limited in modern models such as LLMs due to their low accuracy or high computational cost: most existing algorithms are either highly inaccurate, or require computing gradients or approximations to inverse Hessians, which can be prohibitive for large models. In this work, we introduce a highly efficient zeroth-order approximation to data influence that requires only a fraction of the time and memory footprint of previous methods and is applicable to both differentiable and non-differentiable loss functions. We demonstrate that in addition to its computational advantage, our method delivers superior accuracy in estimating self-influence and comparable or better accuracy in estimating train-test influence for fine-tuned large language models, paving the way for broader and more practical application of influence-function techniques in state-of-the-art AI systems.

Self-supervised image denoisers such as Blind2Unblind excel when clean targets are unavailable but noisy observations are plentiful. We ask: can widely available source-domain data, such as RGB images, improve these denoisers when noisy observations are also limited? We introduce XMNoise2Clean, a framework that learns a noisy target generator from limited paired source/target data, applies it to abundant source images, and trains the denoiser on the union of real and generated noisy samples. We define a cross-modal predictability metric Γ ∈ [0, 1] that measures what fraction of target signal variance the source can explain. When Γ ≈ 1 (no scene properties hidden from the source), generated samples are in-domain and help substantially: using a generator calibrated on 500 paired examples, XMNoise2Clean improves Blind2Unblind by about 3.6 dB with only 50 downstream denoiser-stage real target images, nearly matching the 1000-real denoiser baseline. When Γ is moderate (one hidden scene property, such as sub-frame temporal dynamics in event cameras), the method helps but less reliably. When Γ is low (two or more hidden scene properties, such as the temperature and emissivity fields that determine thermal infrared intensity but are invisible to RGB), generated samples hardly help and can suppress real target structure. Controlled synthetic experiments with known Γ confirm that augmentation benefit generally increases with source-target predictability, and three real-world modality settings plus a controlled proxy experiment support the pattern.

Semi-dense local feature matching commonly aggregates contextual information before coarse-to-fine correspondence estimation. However, intra-image and inter-image aggregation serve different roles: the former should propagate spatial evidence within each image while retaining structured two-dimensional dependencies, whereas the latter should gather information from plausible corresponding regions while limiting noise from unrelated locations. We propose WovenAnchor Matcher (WAM), a semi-dense matching framework based on role-specialized context aggregation. WAM introduces two complementary operators. WovenMamba performs intra-image aggregation through horizontal-then-vertical state-space propagation, allowing vertical updates to operate on horizontally contextualized features and thereby encouraging a structured two-dimensional receptive-field bias. AnchorCrossAttention performs inter-image aggregation by using cross-attention to gather context from plausible corresponding regions across the image pair. To make this retrieval robust, it operates on local representative anchors rather than dense point-wise tokens, reducing sensitivity to noisy affinities that can otherwise lead to incorrect correspondence propagation. On MegaDepth, WAM achieves 66.1 pose AUC@5$^\circ$ with a runtime of 35.4 ms on a single H100 GPU, improving over JamMa, which achieves 64.1 pose AUC@5$^\circ$ at 43.8 ms under the same setup. Ablations show that removing or replacing either specialized component reduces accuracy, providing evidence that intra-image propagation and inter-image retrieval benefit from role-specific aggregation designs.

Vision-Language-Action (VLA) models have emerged as a promising paradigm for building embodied agents that ground perception and language into action. However, most existing approaches rely on direct action prediction, lacking the ability to reason over long-horizon trajectories and evaluate their consequences, which limits performance in complex decision-making tasks. In this work, we introduce $\textbf{World-Value-Action (WAV)} $ model, a unified framework that enables implicit planning in VLA systems. Rather than performing explicit trajectory optimization, WAV model learn a structured latent representation of future trajectories conditioned on visual observations and language instructions. A learned world model predicts future states, while a trajectory value function evaluates their long-horizon utility. Action generation is then formulated as inference in this latent space, where the model progressively concentrates probability mass on high-value and dynamically feasible trajectories. We provide a theoretical perspective showing that planning directly in action space suffers from an exponential decay in the probability of feasible trajectories as the horizon increases. In contrast, latent-space inference reshapes the search distribution toward feasible regions, enabling efficient long-horizon decision making. Extensive simulations and real-world experiments demonstrate that the WAV model consistently outperforms state-of-the-art methods, achieving significant improvements in task success rate, generalization ability, and robustness, especially in long-horizon and compositional scenarios.

Aerial vision-language navigation requires agents to follow natural-language instructions through closed-loop perception and action in 3D environments. We argue that aerial VLN can be formulated as a prediction-driven world-action problem: the agent should anticipate latent world evolution and act according to the predicted consequences. To this end, we propose WorldVLN, the first autoregressive world action model for aerial VLN. Unlike full-sequence video-generation world models that generate an entire visual clip, WorldVLN adapts a latent autoregressive video backbone to predict short-horizon world-state transitions and directly decodes them into executable waypoint actions. After each action segment is executed, newly received observations are encoded back into the autoregressive context, enabling closed-loop world-action prediction. We further introduce a two-stage training framework that first grounds the video prior in instruction-conditioned navigation dynamics and then develops Action-aware GRPO, the first reinforcement learning method tailored to autoregressive WAMs, to optimize waypoint decisions through their downstream rollout consequences. On public outdoor and indoor benchmarks, WorldVLN consistently outperforms existing Vision-Language-Action baselines with $12\%+$ success-rate gains and larger advantages on challenging cases. It further transfers zero-shot to real drone deployment, suggesting that the proposed WorldVLN offers a promising route for spatial action tasks. Demos and code are available at \url{https://worldvln.com} (anonymous).

Generative-prior-based super-resolution (SR) methods leverage implicit knowledge learned from large-scale models to enhance low-resolution inputs. However, such priors are inherently stochastic and optimized for diverse generation, conflicting with the deterministic, high-fidelity reconstruction required for SR. It is also tied to the base model, costly to update, and prone to hallucinations as real-world data evolves. To address these limitations, we introduce WorldSR, a novel framework that augments SR with explicit, entity-aligned visual world knowledge. WorldSR automatically decomposes the input into semantic entities and performs entity-wise retrieval of structurally and semantically aligned images from a large-scale external corpus. For efficiency and reliability, we incorporate a memory mechanism to reuse previously retrieved results and a multi-step filtering process to refine candidate references. The selected references as world knowledge are then integrated through a novel multi-reference super-resolution model, which provides fine-grained constraints for detail synthesis and structural recovery. Experiments on real-world SR benchmarks show that WorldSR consistently improves structural fidelity and visual quality, outperforming existing generative super-resolution methods. Our results suggest that entity-level grounding in external visual world knowledge provides a simple and effective complement to model-bound generative priors.

Large language models (LLMs) trained purely on text ostensibly lack any direct perceptual experience, yet their internal representations are implicitly shaped by multimodal regularities encoded in language. We test the hypothesis that explicit sensory prompting can surface this latent structure, bringing a text‑only LLM into closer representational alignment with specialist vision and audio encoders. When a _sensory prompt_ tells the model to 'see' or 'hear', it cues the model to resolve its next‑token predictions as if they were conditioned on latent visual or auditory evidence that is never actually supplied. Our findings reveal that lightweight prompt engineering can reliably activate modality‑appropriate representations in purely text‑trained LLMs.

Vision-language model (VLM) unlearning is often treated as an objective-design problem: given multimodal forget data, the goal is to optimize a loss that removes undesirable behavior while preserving retained capabilities. We argue that this view overlooks an equally important data-centric question: how should each forget example be represented before optimization? Existing methods typically keep image-conditioned failures in their original image-text form, implicitly assuming that pixels are the right route for unlearning whenever pixels appear in the input. We challenge this assumption by constructing modality-decomposed versions of VLM benchmarks, enabling controlled comparisons among image-only, text-only, and multimodal representations of the same examples. Our modality-mixing experiments show that, for many examples, textual renderings carry the actionable forget signal more directly than the image alone, while purely text-only unlearning can still weaken visual grounding when the target behavior depends on visual evidence. Motivated by this trade-off, we introduce ModRoute, a gradient-guided per-sample modality routing strategy that selectively converts high visual-pressure examples to text-only form while keeping the remaining examples multimodal. Notably, on VLGuard with LLaVA-1.5-7B, ModRoute has the strongest composite unlearning--utility score of $0.847$ at $\gamma=0.5$, a $2.5$% improvement over the best random-switching score and $\geq46$% better than pure multimodal or text unlearning. Overall, our results show that effective VLM unlearning depends not only on the objective, but also on the composition and per-sample modality routing of the unlearning data.

Open-weight models are often released, fine-tuned, aligned, merged, and re-released, making provenance audits ask not only whether checkpoints are related, but also which checkpoint came first. Many existing model-provenance methods are designed for a base-known audit setting: given a victim or source model, they test whether a suspect model is related to it. Although these audits are framed as source-to-suspect tests, their underlying evidence is often symmetric, relying on representation similarity, weight similarity, behavioral fingerprints, or correlation statistics. Symmetric pairwise comparisons can detect relatedness, but they cannot by themselves orient A versus B. We therefore introduce a local geometric comparison: instead of comparing two checkpoints directly, we add a third same-family checkpoint as a witness and compare the geometry around A with the geometry around B. Direction is inferred by asking which candidate behaves more like a branching parent. Motivated by this idea, and by the empirically observed asymmetry between parent-anchored and child-anchored witness-overlap distributions, we propose Witness Overlap, a prompt-free, training-free white-box test for directional provenance. On 176 LLM checkpoints from 16 families, our one-witness test orients 95.3\% of parent–child decisions using Frobenius cosine. We further evaluate root identification, sibling discrimination, generalizations to VLM and diffusion families, and chain-structured ordering. The signal is robust to weight noise and sparse pruning, with a proposed SVD weight reduction variant showing greater robustness than Frobenius cosine.

Oscillations and synchronization are widely believed to play a fundamental role in representation and computation. However, existing machine learning approaches based on synchronization dynamics have largely been confined to specialized settings such as object discovery, with limited evidence of scalability to standard vision benchmarks or logic reasoning tasks. We propose the \emph{Winfree Oscillatory Neural Network} (\emph{WONN}), a dynamical neural architecture based on generalized Winfree dynamics. \emph{WONN} evolves representations on the torus $(S^1)^d$ through structured oscillatory interactions, combining phase-based inductive biases with flexible and hierarchical interaction mechanisms instantiated as either fixed trigonometric mappings or learnable neural networks. We evaluate \emph{WONN} on image recognition and complex reasoning tasks, including CIFAR, ImageNet, Maze-hard, and Sudoku. Across these domains, \emph{WONN} achieves competitive or superior performance with strong parameter efficiency. \textbf{In particular, \emph{WONN} is, to our knowledge, the first synchronization-based oscillatory architecture to scale competitively to ImageNet-1K.} Furthermore, on Maze-hard, \emph{WONN} achieves \textbf{80.1\% accuracy using only 1\% of the parameters of prior state-of-the-art models}. These results suggest that structured oscillatory dynamics provide a scalable and parameter-efficient alternative to conventional neural architectures.

We present MaskGen, a theoretically grounded and deliberately simple approach for domain generalization in 3D biomedical image segmentation. Modern segmentation models degrade sharply under shifts in modality, disease severity, clinical sites, and more, limiting their reliable adoption. Existing generalization methods address this using extreme augmentations, hand-engineered domain statistics mixing, or architectural redesigns that add significant implementation overhead while yielding inconsistent performance across biomedical settings. MaskGen instead presents a principled learning strategy with marginal overhead that utilizes both source-domain image intensities and domain-stable foundation model representations to train robust segmentation models. As a result, MaskGen achieves strong gains in both fully supervised and few-shot segmentation across broad clinical shifts in biomedical studies. Unlike prior approaches, MaskGen is architecture- and loss-agnostic, compatible with standard augmentation pipelines, easy to implement, and tackles arbitrary anatomical regions.

A solid understanding of the predictive success of deep neural networks (DNNs) remains elusive. For example, while many data-dependent metrics exist that seek to predict model quality of DNNs, these metrics may be expensive to compute for large datasets and/or may be impossible to compute when training datasets are not released. A practical and effective predictor of model quality involves analyzing DNN weight matrices, as it is known that a heavy-tailed spectral distribution often correlates with strong model quality. As such metrics lack a rigorous statistical derivation, in this work we aim to understand why they perform well, by employing a probabilistic framework to derive the marginal likelihood for the trained weights of a DNN. Across large-scale convolutional DNNs and LLMs, we find that this marginal likelihood predicts model quality. To understand the role heavy-tailed spectra play in predictive performance, we derive the limiting log-marginal likelihood for spectra that follow the heavy-tailed High-Temperature Marchenko-Pastur (HTMP) distribution. We show that this limiting quantity is convex in a *heaviness* parameter, and we derive an optimal *heaviness* that empirically predicts over-fitting for large-scale DNNs during training.

Recent advances in diffusion transformers (DiTs) have enabled promising single-turn image editing capabilities. However, multi-turn editing often leads to progressive semantic drift and quality degradation. In this work, we study this problem from a latent-space frequency perspective by decomposing the editing process into two functional components: VAE and DiT. Through systematic analysis in the VAE latent space, we uncover that the DiT introduces dominant low-frequency drift that accumulates as semantic misalignment across editing rounds, while the VAE contributes comparatively stable reconstruction bias. Based on this insight, we propose **VAE-LFA** (Low Frequency Alignment), a training-free, plug-and-play method that performs alignment in VAE latent space. VAE-LFA decomposes latent discrepancies across editing rounds via low-pass filtering, and aligns low-frequency statistics to an exponential moving average of previous rounds, effectively suppressing accumulated semantic drift while preserving high-frequency details. Our method requires *no retraining, ground-truth priors, or access to diffusion parameters*, making it applicable to both white-box and black-box DiT editors. For white-box models, VAE-LFA is seamlessly integrated into the editing pipeline by eliminating redundant VAE round trips; for black-box models, it operates via an off-the-shelf VAE to perform inter-round latent alignment. Extensive experiments demonstrate that VAE-LFA improves semantic consistency and visual fidelity across diverse multi-turn editing scenarios, including both controlled and in-the-wild images.

Modern large language models (LLMs) often exhibit overconfident errors, assigning high confidence to incorrect predictions and thereby undermining reliability in real-world use. Existing calibration methods typically rely on post-hoc adjustment or retraining, operating at the output level without addressing the underlying causes of miscalibration. We propose CoCHI (Class-oriented Causal Head Intervention), a framework that improves calibration by identifying and intervening on internal components responsible for distinct confidence behaviours. By analysing predictions through correctness–confidence patterns, CoCHI enables targeted intervention on model internals, reducing overconfident errors while preserving correct predictions. Our approach provides a mechanistic perspective on calibration, linking reliability to identifiable structures within the model rather than treating it as an output-level issue. Experiments across multiple LLMs show consistent improvements in calibration metrics, including Expected Calibration Error, Negative Log-Likelihood, and Brier Score, while maintaining accuracy on five multiple-choice question answering benchmarks. These results suggest that effective calibration requires not only adjusting outputs, but also addressing the underlying causal mechanisms within the model. Implementation details and code are provided in the supplementary material.

Current Audio-Visual LLMs (AVLLMs) struggle with reasoning over videos featuring multi-speaker dialogues. In such videos, resolving "who says what" is crucial, which necessitates trimodal (text-audio-visual) binding. Motivated by these challenges, we systematically investigate how this trimodal binding is achieved in AVLLMs. Specifically, we identify emergent symbolic trimodal binding mechanisms in AVLLMs that utilize modality-specific symbolic variables. By encoding auditory and visual components into symbolic variables-capturing temporal utterance sequences and spatial entity coordinates, respectively-the model establishes cross-modal linking within this abstract space. Crucially, we reveal that when trimodal binding fails, the breakdown predominantly stems from misaligned audio-visual connections. To overcome this bottleneck, we introduce an audio-visual prompting method utilizing an off-the-shelf Active Speaker Detection (ASD) model. By simply overlaying visual bounding boxes on active speakers, this training-free approach yields immediate performance gains across three conversation-centric benchmarks. Moreover, lightweight fine-tuning of fewer than 300 steps on these ASD-prompted-videos extends these gains to three general AV benchmarks, suggesting the generalizability of our method.