NeurIPS 2026 Papers

Generalized planning (GP), where a single policy solves multiple instances from a common planning domain, remains a challenging problem in AI. Abstraction plays an important role in GP, and Qualitative Numerical Planning (QNP) provides a compact abstract model for GP. However, useful QNP abstractions are difficult to construct and require substantial manual effort and expertise. We study whether QNP abstractions can be generated from PDDL domains and training instances by coupling LLM generation with symbolic reasoning. We propose a generate--debug--repair framework in which an LLM proposes abstract features and constructs a candidate QNP abstraction over the initial states, actions, and goals of the training instances. To improve reliability, we introduce verification-guided repair based on approximate soundness. Given a candidate abstraction, we solve it, validate the induced abstract instances, and apply one of two checking branches: SRCB tests an $m$-simulation relation between induced abstract and concrete instances to target approximate soundness, while PRCB tests whether the induced abstract plan refines into valid concrete solutions. Detected failures are converted into structured feedback for iterative repair. Experiments on seven GP benchmark domains with five LLMs show that verification-guided repair improves LLM-generated QNP abstractions over both single-pass generation and LLM self-repair, and helps some models produce abstractions that transfer across instances. Our results suggest that LLMs can serve as generators of symbolic abstractions for GP when coupled with formal error detection and structured repair feedback.

Speculative decoding accelerates large language model inference by using a draft model to generate candidate tokens, which are verified by the target model in a single forward pass. Verification proceeds and discards every position from the first rejection onward, yet existing draft training relies on token-level cross-entropy with a fixed per-position weighting that does not reflect this process. We introduce Verification-Aware Training (VAT), a plug-in framework that simulates verification at every training step and turns the resulting accept and reject patterns into supervision. VAT consists of two components: (i) a verification head, a lightweight jointly-trainable binary classifier that validates per-position acceptance via an explicit prediction target; (ii) verification-adaptive weighting replaces the fixed weighting schedule with weights adapted to each sample's first rejection point during training. VAT is model-agnostic and can be layered on top of existing methods without changing the draft architecture, the target model, or the inference procedure, and trained jointly with the original loss. Applied to EAGLE-3 and DFlash on Qwen3-4B, Qwen3-8B and LLaMA3.1-8B, VAT improves average acceptance length by up to 11.4% and wall-clock speedup by up to 8.7%, with consistent gains across math, code, and chat benchmarks.

Evaluating machine-learning-based vulnerability detectors requires datasets that pair accurate labels with realistic code. Existing benchmarks satisfy at most one. Real-world collections rely on noisy commit-based labels because manual curation by security experts does not scale, while verified synthetic collections generate code from scratch that is too simple to resemble production software. The rapid advance of code LLMs adds a third pressure, since their training corpora absorb public CVE data and most widely cited vulnerability benchmarks, leaving static evaluations of such models prone to measuring memorisation rather than analysis. As model knowledge cutoffs continue to move forward, any fixed dataset risks becoming part of the next generation's training set. We present VeriVul, a framework that produces formally verified vulnerability data on demand. Given a CVE-fixing commit, it applies a vulnerability-aware backward program slicer to isolate the fragment relevant to the vulnerability, prompts a code LLM to expand the fragment into a self-contained program, and certifies the resulting program with the ESBMC bounded model checker, recording the verified label together with the trace that triggers the violation. Each verified program is paired with an ESBMC-verified counterpart that flips the label. We characterise the synthesised programs along vulnerability-relevant structural dimensions (e.g., control-flow density, pointer and array operations, struct-field access, and identifier diversity) and show that VeriVul dataset samples lie distributionally closer to real-world vulnerable code than the prior verified synthetic baseline, while remaining sufficiently complex to challenge state-of-the-art LLM-based detectors. In a prompted evaluation, Claude Opus 4.7 reaches only 52.6 percent accuracy on VeriVul dataset despite being given the full self-contained program. Because each sample carries the ESBMC counterexample and the violating statement, VeriVul also supports evaluation beyond binary classification, including root-cause identification and trace-grounded explanation. We release the framework, the slicer, the verification harness, and the generated dataset to support contamination-resilient evaluation of code LLMs as vulnerability analysts.

Large language models (LLMs) are increasingly used in hardware-oriented coding workflows, yet open resources for evaluating first-pass RTL beyond execution remain limited. We present VeriScope, an open benchmark and evaluation suite of 568 problems spanning basic combinational gates through module-level designs and a 95-task L4+ top-end slice (92 L4 system tasks plus 3 L5 stress tests). A developer agent receives a natural-language task brief, returns a single RTL draft, and that artifact is evaluated through objective execution plus RTL-level and artifact-level review incorporating waveform and circuit evidence. Across 26 public models plus two 32B calibration baselines, the best systems reach about 84/100 combined score on the full benchmark but drop to the high 70s on L3–L4+. The 60/40 combined leaderboard largely tracks functional execution (Spearman 0.998 with a functional-only ranking), while artifact scores are most useful as a post-simulation screening signal: 29.6% of L3–L4+ simulation-passing submissions receive artifact score below 6 and therefore need additional verification evidence. A 100-sample manual taxonomy of such disagreements finds 70% testbench coverage gaps, 12% real RTL defects, and 18% judge hallucinations (Wilson 95% intervals reported in the analysis), showing that artifact review surfaces both under-tested passes and model defects, but should not be treated as a standalone leaderboard refinement.

Large language models (LLMs) have made misinformation inexpensive to produce but not to verify, creating a growing asymmetry in the information ecosystem. Under tight time, labor, and budget constraints, media organizations, platforms, and fact-checkers rely on screening to prioritize which content to verify. We introduce **VEX-Bench**, a unified benchmark for evaluating the *verification complexity* of LLM-generated misinformation, as perceived during screening, across models and generation methods. Verification complexity is assessed along multiple dimensions derived from journalistic and fact-checking practices, capturing checkability, harm potential, source credibility signals, imposter legitimacy, and expected verification effort. We define the $\mathrm{VEX}$ score as an integrated measure combining elicitation yield and verification complexity to quantify how generated content consumes limited verification capacity. We construct a benchmark spanning two misinformation categories, 6 high-stakes domains, and 60 real-world topics, and evaluate 7 frontier LLMs and 7 generation methods, yielding 5,880 articles. We employ an LLM-as-judge for scalable evaluation and validate it using content-analysis methodology, including ordinal Krippendorff~$\alpha$ for inter-annotator reliability, complemented by fact-checking agents for verification. Our findings show that no single method dominates all dimensions, underscoring the need for multi-dimensional evaluation. LLMs can generate high-$\mathrm{VEX}$ misinformation at 3$\times$ to 169$\times$ lower cost than agent-based verification. Such content is often prioritized during screening, consuming scarce verification resources and introducing a systematic risk of misallocation in resource-constrained verification systems.

Self-improvement at scale has been a longstanding goal for reasoning models, and there are two natural places to do it: at test time, through verification-refinement (V-R) loops; and at training time, through self-training methods. Both are gated by the same bottleneck: the verifier. V-R loops stall when verifier scores inflate over rounds while accuracy stagnates, and when feedback is too generic to act on; self-training fails similarly when bad self-generated data are added to training. Better verifiers would unlock both, but the capability we want to train, i.e., catching errors the generator cannot detect in its own work, has neither finetuning data nor a verifiable reward. To address this challenge, we propose *self-trained verification* (STV). Our key observation is that, while a model cannot catch these errors alone, it can when shown the reference solution. We turn this asymmetry into a supervision target and train the verifier to imitate a more informed version of itself. At test time, STV substantially improves V-R loops on hard problems, while standard alternatives (e.g., SFT, RL on verifier scores, and even meta-verifiers) do not. STV roughly doubles accuracy on hard DAPO math and lifts it 14x on the hardest SciKnowEval problems (1.5% to 21%). At training time, starting from an RL-converged generator, putting the STV verifier in the loop yields a further 33% relative gain in test-time pass@1. More notably, the generator's standalone pass@1, with no verifier at inference time, climbs 30% relative past where continued RL had converged. Hence, the next frontier in reasoning may lie in how we train verifiers.

AI agents are governed by hundreds of natural language criteria---yet existing verifiers cannot efficiently evaluate an agent's output against a large set of such criteria and report which are satisfied, violated, or inapplicable. We introduce the VFM, a tree-attention verifier that encodes the shared context and target text, and scores $N$ natural language criteria in parallel, returning independent per-criterion ternary verdicts. The VFM is pretrained on CriteriaBank, an open corpus of 357K (context, target, criterion, verdict) tuples spanning over 285K distinct criterion strings. A finetuned VFM-4B reaches 88.3\% accuracy on a synthetic governance benchmark, surpassing larger generative judges, and on real insurance-compliance calls it is competitive with GPT-5.4 with synthetic finetuning alone. On the DynaBench multi-criterion benchmark, a finetuned VFM-4B reaches $0.85$ F1 on trace-level failure detection versus DynaGuard-4B's $0.72$; the VFM additionally localizes the violated rule as its top-1 prediction in $98.4\%$ of failing traces, and a top-3 cascade to a 26B Gemma 4 chain-of-thought judge reaches $0.94$ F1. CriteriaBank pretraining improves cross-domain transfer on four additional benchmarks, particularly in the low-data regime. On an H100, VFM-4B evaluates 1000 criteria against a 4K-token context in under 2s at $<$10GB VRAM, making it suitable for runtime verification. We will release CriteriaBank, trained checkpoints, and evaluation code.

Safe reinforcement learning (RL) aims to learn policies that optimize rewards while satisfying constraints. Predominant approaches rely on soft-constrained policy optimization, which has achieved empirical success but does not provide formal safety guarantees for the learned policy. In contrast, methods with strict guarantees typically rely on explicit certificate functions, whose construction requires the direct synthesis and verification of control-invariant sets, a process that scales poorly with state dimension and often yields overly conservative behavior. In this paper, we present the Provably Safe, yet Performant RL (PSP-RL) framework, a novel two-phase architecture for learning provably safe policies in a scalable manner, designed to overcome the key bottlenecks of prior methods. Rather than explicitly computing invariant sets, PSP-RL leverages a learned backup policy to forward-integrate the system dynamics, generating an implicit control-invariant set online. In the first phase, the backup policy is trained with our proposed safe-arrival value function, which characterizes the optimal backup policy for invariant-set construction. In the second phase, an RL policy is trained end-to-end through a differentiable projection layer that strictly enforces the safety guarantees induced by the learned backup policy. By maximizing the volume of the implicit control-invariant set in the first phase, the resulting PSP policy from the second phase is performant and scalable, while maintaining provable safety. Crucially, PSP-RL imposes no restrictions on the underlying RL algorithm and can be plugged into any existing training pipeline. We establish theoretical guarantees for the proposed framework and evaluate it on robotic control tasks with state dimensions up to 10, a regime in which prior provably safe RL methods struggle or become impractical.

Deep search capabilities have become an indispensable competency for frontier large language model (LLM) agents, yet training high-performance deep search agents remains constrained by three key challenges: as synthesized reasoning graphs grow in complexity, verifying answer correctness and uniqueness becomes increasingly difficult to scale; heavy dependence on online search APIs makes data synthesis costly and hard to scale; and the lack of fully open synthesis pipelines severely hinders reproducibility.To bridge this gap, we introduce OpenSearcher, the first deep search agent training pipeline with zero online API dependency throughout the entire data synthesis and model training process, built upon two core technical innovations: (1) \textit{Distinguishing Set-grounded QA synthesis with programmatic verification}: we compute minimal Distinguishing Sets on Wikidata to uniquely identify target entities, recursively expand them into reasoning DAGs, and transform the structured graphs into natural language questions via progressive generation and fuzzification. Answer uniqueness is deterministically verified through SPARQL conjunctive queries, complemented by lightweight LLM filtering for linguistic quality. (2) \textit{Fully offline training pipeline}, which builds an offline corpus of tens of millions of documents from publicly downloadable Wikidata, Wikipedia, and Web Crawl Dumps, and completes trajectory synthesis, SFT cold start, and reinforcement learning entirely offline. Experimental results demonstrate that OpenSearcher achieves strong performance across deep search benchmarks, establishing a new state of the art among fully offline methods, for example, achieving 32.3\% on BrowseComp and 72.8\% on GAIA. We fully open-source the complete data synthesis pipeline to democratize offline deep search agent research and foster a more transparent, collaborative ecosystem.

Chain-of-Thought reasoning improves the explainability of large language models, yet verifying such reasoning remains difficult when intermediate steps express epistemic uncertainty rather than deterministic entailment. Neuro-symbolic verifiers typically translate reasoning steps into rigid first-order or SMT-style constraints. This forces each proposition into a binary truth regime and creates a Rigidity--Ambiguity Mismatch: uncertainty-marked claims such as may, likely, or suggests are either over-hardened into deterministic assertions or rejected as unverifiable. We propose ProbVeri, a probabilistic soft-logic framework for formal verification under uncertainty. The key idea is to represent uncertainty-marked reasoning steps as weighted soft logical constraints over continuous truth assignments, so that partial evidential support remains expressible. Building on this soft-logic representation, we formulate verification as a contrastive energy minimization problem: a step is considered supported when its natural interpretation has lower verification energy than its negated counterpart under the same evidence, soft rules, and assumption regularization. Probabilistic Soft Logic defines the logical energy through weighted hinge-loss constraints. We introduce a support-grounded assumption penalty that discourages unsupported latent bridge assumptions between context and claim. The resulting energy gap provides a confidence-scored verification signal that separates unsupported steps from weakly but consistently supported inferences. Experiments on ProofWriter, BioASQ, and LegalBench-SARA show that ProbVeri recovers more verified-correct reasoning traces than rigid verifiers while reducing over-acceptance compared with soft-only PSL. These results suggest that uncertainty-aware verification benefits from soft logical formalization and contrastive comparison between natural and negated interpretations.

Multimodal large language models (MLLMs) have made rapid progress in general visual understanding, yet they still struggle with fine-grained instance-level consistency verification, where the goal is to determine whether two images depict the exact same physical object under varying viewpoints, illumination, and backgrounds. This task requires both a global understanding of the target instance and a precise examination of subtle local evidence, since semantically similar objects may differ only in small discriminative regions. To address this challenge, we propose \textbf{LocalAgent}, a collaborative agentic framework that integrates the complementary strengths of large and small models. Specifically, the MLLM first reasons from a global instance-level perspective to identify suspicious local regions that may determine the final verification result. These accurately localized regions are then delegated to a lightweight Local Evidence Verifier (LEV) toolkit for fine-grained appearance and geometric matching. The LEV toolkit consists of \textbf{Local Appearance Consistency (LAC)}, which provides illumination- and color-robust similarity estimation, and \textbf{Local Geometric Correspondence (LGC)}, which establishes reliable spatial correspondence under viewpoint changes. Rather than directly replacing the MLLM's reasoning, LEV returns structured similarity scores and comparative evidence in a form that the MLLM can effectively interpret for final decision-making. This design enables a coordinated large-small model collaboration: the MLLM contributes global semantic reasoning and region-level suspicion localization, while specialized local verifiers provide precise, invariant, and interpretable evidence for ambiguous cases. We further introduce an answer-dominant reinforcement fine-tuning (RFT) strategy that enables the policy to learn when verification is necessary. Experiments show that LocalAgent achieves a \textbf{+4.8\%} average improvement over direct-inference baselines, effectively narrowing the gap with closed-source models, while preserving the general multimodal capabilities of the underlying MLLM.

Verifying the local robustness of neural networks under $\ell_0$ perturbations is inherently combinatorial: a verifier must reason over all sparse subsets of perturbed pixels. This paper presents FocusBranch, a combinatorial branch-and-bound framework for $\ell_0$ robustness verification. The key insight is to decompose the $\ell_0$-ball using nodes, where each node consists of a focus pixel set $\mathcal{S}$ and a level $l$, requiring at least $l$ perturbed pixels to lie in $\mathcal{S}$. This abstraction unifies two branching mechanisms: concrete nodes branch through upper shadows to fix additional perturbed locations, while super nodes branch through covering designs to cover many perturbation cases with fewer child nodes. FocusBranch proves node safety by concretizing linear relaxations over node-constrained $\ell_0$-balls and recursively branches on unknown nodes. Rather than relying on a fixed verification strategy, it samples nodes across levels to estimate success rates and costs, then selects a starting level and branching strategy predicted to minimize verification time. Experiments on fully connected and convolutional classifiers for MNIST, Fashion-MNIST, and CIFAR-10 show that FocusBranch verifies $\ell_0$ local robustness effectively across architectures and outperforms state-of-the-art verifiers.

As large generative models become widely deployed and customized, federated learning is increasingly used to adapt them while keeping user data local. Because clients repeatedly receive up-to-date adapters, a malicious client can copy a dispatched adapter, use it offline, and monetize generated images without exposing the stolen weights or a queryable service. Existing federated watermarking and traitor-tracing methods usually assume white-box access to suspect weights or black-box query access to the deployed model. In realistic generative-model theft, however, the defender may only observe images that have already circulated. We propose \emph{FedTrace}, a generated-content-based watermark verification framework that attributes leaked federated models from suspicious generated images alone. FedTrace couples three designs: a round-wise watermark lifecycle that separates client identity distribution from global utility aggregation, a low-drift reliable-bit carrier that embeds identity in watermark positions stable under local adaptation, and anti-collision coding with soft subset verification for distinguishing singleton and collusive leakage. These components enable post-local, collusion-aware attribution from generated outputs alone, without suspect weights or online query interfaces. Extensive experiments across customized diffusion datasets, base models, and federated settings show that FedTrace preserves detectable client identities under local adaptation and strengthens subset-aware tracing against collusive leakage.

Neuro-symbolic systems for sequence classification couple a neural perception network with a finite automaton over abstract events. Certifying their trajectory-level decisions under input perturbations is critical for safety-sensitive deployment. We address the open problem of end-to-end formal robustness certification for such Neurosymbolic Automata (NeSyA) under norm-bounded input perturbations. Naive layerwise linear bound propagation fails on this composition: per-step relaxation slack compounds through the temporal recurrence (interval explosion), and the standard log-space transition score subtracts two log-sum-exp terms over overlapping coordinate sets that independent relaxations cannot tighten. To address both, we introduce contrastive logit-gap (CLG), a reparameterization whose two log-sum-exp heads act on disjoint coordinates and admit substantially tighter linear bounds, coupled with a fused temporal operator that yields corner-tight bounds from a single linearization. On NeSyA sequence benchmarks, our formulation scales significantly beyond recursive baselines, maintaining tight safety certificates at long horizons while reducing verification wall time by up to ${\sim}6{\times}$. To our knowledge, this is the first end-to-end formal verification framework for temporal neuro-symbolic systems.

Multimodal geometry reasoning requires models to jointly perceive diagrams and perform symbolic derivations. Test-time verification methods such as majority voting assume voter errors are roughly independent, but in geometry this assumption breaks down: all candidates perceive the same diagram, so perceptual biases cascade into correlated errors that produce confident but wrong consensus. We observe that neuro-symbolic candidates contain compositional structure that can serve as a verification resource. We introduce SKETCH, a format decomposing each candidate into a neural pathway (natural-language claim) and a symbolic pathway (visual grounding → typed DSL → deterministic execution). These pathways are governed by different error processes—symbolic errors are correlated across candidates through shared perception, while neural errors are more dispersed. Our method, Compositional Consensus Verification (CCV), gates consensus on cross-channel agreement: because the two pathways fail for different reasons, accidental agreement is rare, making each concordant vote far more precise than a raw majority vote. Across four geometry benchmarks, CCV achieves 81.0% accuracy (+10.4 pp over majority voting) without external scorers or additional inference. Seven non-compositional baselines—including trained PRMs—cluster at 70–71%, while compositional cross-layer features jump to 79–81%, confirming that structural diversity is the core verification resource, and that a principled gating algorithm effectively unlocks its potential.

With the increasing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become very important in safety-critical and legal compliance settings. However, model parameters are often commercial secrets that cannot be disclosed to auditors or end users. To this end, we present PANDA, a scalable system that uses Zero-Knowledge Proofs (ZKPs) to prove robustness and fairness properties of a model without revealing private model parameters. PANDA is built on top of CROWN an efficient robustness certification framework that is used in many state-of-the-art formal verification tools for neural networks. The core contribution of PANDA is a novel algorithm for proving linear relaxation bounds on non-linear activation layers, achieving simple and lightweight proofs. Remarkably, our system can generate proofs of local robustness for neural networks with more than 2.9M parameters in about 4 minutes, and can verify them in under 7.5 seconds. Prior ZKP-based robustness systems are based on exponential-time algorithms that cannot scale to nontrivial networks. In contrast, PANDA scales polynomially with the number of neurons in a network, allowing us to support neural networks 3 to 4 orders of magnitude larger than prior works with significantly reduced prover overhead.

Hosted LLM services increasingly expose model identity as a product claim, but external users and auditors often cannot inspect which model configuration served a request. We study an auditor-assisted regime in which a trusted auditor enrolls claimed identities and prepares verification material before deployment, while audit-time verification uses only the claimed identity and released output, without runtime access to model internals, inference logs, routing decisions, or provider metadata. We propose SumMark, a *summary-channel watermarking* framework that uses user-visible reasoning summaries as a keyed audit surface. During setup, SumMark constructs identity-specific vocabulary carriers, trains lightweight summary adapters, and calibrates per-identity thresholds. At deployment time, a keyed statistical test assesses whether the released summary is consistent with the claimed identity and, when needed, attributes the most likely enrolled identity. Across model families, scales, and task domains, SumMark reliably detects cross-family and cross-scale substitutions at low false-positive rates while preserving task-facing answer quality. We further study FP16$\rightarrow$INT8/INT4 precision-consistency diagnostics and robustness under bounded post-processing, rewriting stress tests, and text-only spoofing, revealing both strong performance and clear failure boundaries.

While bound propagation methods are highly effective for certifying neural network robustness against $\ell_{\infty}$ adversaries, scalable verification for $\ell_{2}$ perturbations remains a significant open challenge. Existing approaches suffer from severe geometric loss: elementwise bounding methods like $\alpha$-CROWN relax Euclidean balls to bounding boxes, losing a factor of $\sqrt{n}$ in radius, while the recently proposed SDP-CROWN rounds deformed ellipsoids back into balls, losing a factor proportional to the condition number of the weights. Consequently, tight $\ell_{2}$ verification is currently restricted to near-isometric or Lipschitz-regularized networks where these approximations are not vacuous. In this paper, we introduce affine-image propagation, a novel CROWN-compatible framework that exactly propagates the affine geometry of $\ell_{2}$ balls and $\ell_{\infty}$ boxes through the network. To bypass the prohibitive computational cost of exact Semidefinite Programming (SDP) constraints required by this representation, we derive highly scalable, SDP-based bounds utilizing diagonal-dominance surrogates. Our approach effectively eliminates the geometric bottlenecks of prior work, yielding the first large-scale, SDP-style bound propagation method capable of tight $\ell_{2}$ verification for general, non-Lipschitz-regularized neural networks.