NeurIPS 2026 Papers

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.

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.

Software requirements are usually written in natural language, which is essential for human communication but insufficient as a target for machine-checked correctness. While natural-language descriptions can state intended functionality, verification requires formal specifications with explicit types, relations, quantifiers, guards, witnesses, and edge cases. To bridge this divide, we study the Formal Specification Synthesis task: given a natural-language programming requirement and fixed formal signatures, synthesize a proof-assistant specification for the intended input-output relation. This task is difficult for two primary reasons. First, a large representation gap separates informal natural language from the rigorous structures needed by a proof assistant. Second, generated formal specifications are notoriously hard to evaluate, as proving full equivalence between specifications is often too complex to serve as routine feedback. To address these intertwined challenges, we propose SpecBridge, a reconstruction-guided formalization framework. At its core, SpecBridge introduces a Natural-Language Formalization Plan (NLFP), a semi-structured, readable intermediate representation that captures key formalization choices before decoding to a target specification language. Through reconstruction-guided pattern mining, SpecBridge learns these NLFPs by reconstructing formal specifications to discover reusable patterns, ultimately transferring them to improve natural-language task generation. Furthermore, to tackle the evaluation bottleneck, we introduce a multi-layer evaluation protocol for formal-specification correctness. This protocol utilizes LLM Specification Alignment as an LLM-based judge, alongside Test-Driven Computable Validation and Test-Driven Proof Validation, which approximate "running" testcases on formal specifications by translating propositions into executable pre/post checks and proving testcase obligations in Lean. In our experiments, SpecBridge outperforms the few-shot + CoT baseline by 6.1% on LLM Specification Alignment, 15.2% on Computable Validation Pass Rate, and 28.4% on Proof Validation Pass Rate. These results demonstrate that the NLFP bridge and our multi-layer evaluation protocol make formal specification synthesis significantly more reliable.

Probabilistic logical models are a core component of neurosymbolic AI and are important in their own right for tasks that require high explainability. Unlike neural networks, logical theories that underlie the model are often handcrafted using domain expertise, making their development costly and prone to errors. While there are algorithms that learn logical theories from data, they are generally prohibitively expensive, limiting their applicability in real-world settings. Here, we introduce precision and recall for logical rules and define their composition as rule utility -- a measure of the predictive power of logical theories that can be computed in linear time. We then present SPECTRUM, a linear-time framework for learning logical theories from relational data, that mines recurrent patterns in the data, and subsequently, using our utility measure, evaluates and ranks rules derived from these patterns. Finally, we prove theoretical guarantees on the utility of the learnt logical theory. As a result, we demonstrate across various tasks that SPECTRUM scales to larger datasets, often learning more accurate logical theories on CPUs in < 1% of the runtime of SOTA neural network approaches on GPUs.

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present L$^2$EAP (LLM-in-Lean Environment Agentic Prover), an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. L$^2$EAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, L$^2$EAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models; on Lean-IMO-Bench, L$^2$EAP raises the one-shot formal solve rate of general-purpose LLMs from below 10\% to 70\%. It also compares favorably to the best baseline performance of 48\% attained by a specialized system with dedicated ATP components that achieved gold-medal-level performance at the 2025 IMO.

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.

Large language models can now generate complex, multi-step mathematical proofs, but reliably determining their correctness and localizing early logical errors remains a critical challenge. Existing evaluation approaches largely depend on model-based natural-language judgments, which often overlook local reasoning gaps. While formal theorem provers like Lean offer a path to rigorous verification, using them to evaluate informal text requires solving locality and semantic mismatches: a prover might bypass a local flaw by proving an overly broad target, or validate an auto-formalized statement that drifts from the original mathematical intent. To address this, we introduce FaithSieve, a Lean-assisted framework for fine-grained evaluation of natural-language mathematical proofs. FaithSieve decomposes coarse proof steps into local reasoning units, extracts typed proof obligations, and verifies them through a formal evaluation agent. Formal validation is gated by semantic alignment scoring, so Lean evidence is incorporated only when the formal statement faithfully preserves the context, objects, and logical form of the original claim. We construct two expert-verified datasets, ProofLoc-Olympiad and ProofLoc-University, to benchmark first-error localization. On the 350-problem Olympiad dataset, FaithSieve using a GPT-5.4 backbone achieves 81.43\% exact first-error accuracy, outperforming the direct-judging baseline of 72.29\%. Furthermore, on the 200-problem ProofLoc-University benchmark spanning six advanced domains, FaithSieve reaches 84.5\% exact accuracy, compared to 75.0\% for the direct judge. Our work demonstrates that decomposing proofs into fine-grained units and grounding them with faithful formal evidence significantly improves reliable evaluation of natural-language reasoning.

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge lies in designing efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. To ensure correctness, we need robust methods to compare formulations. However, existing approaches evaluate formulations numerically and fail to reason about the behavior on general problem instances. We resolve this limitation by introducing a constructive notion of MILP *reformulation* that can be formalized in Lean and *machine-checked*. We develop `FLARE`, a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference. To evaluate our approach, we introduce *FormulationBench*, a challenging dataset of 20 problems and 116 formulations. `FLARE` outperforms existing methods with **96.9%** accuracy. For cases where formal guarantees aren't necessary, we introduce `FLARE-NL` , an LLM proxy that achieves **99.3%** accuracy. These methods enable reliable verification in automated optimization modeling.

Mathematical autoformalization can fail before proof generation, when an informal concept is grounded to the wrong Lean/Mathlib object. Multilingual terminology makes this step non-monotonic: aliases can recover missing concepts, but under collision stress they can also pull retrieval toward nearby, non-interchangeable anchors. We introduce FACBench, a targeted dependency-light benchmark and audit protocol for multilingual formal-anchor grounding before proof generation. FACBench combines a five-language concept inventory with controlled collision queries, Mathlib-graph stress tests, no-label ablations, theorem-like probes, and Lean-facing anchor checks. In controlled collision settings, naive multilingual alias union can place the expected anchor in the candidate list while ranking a nearby distractor first. A simple rule-based source/context guard improves top-1 anchor accuracy over naive multilingual retrieval by about 11 percentage points on controlled collisions and 28 percentage points on a Mathlib-graph-mined controlled holdout. Less scaffolded and theorem-like probes show where this guard stops helping and point to the need for role-aware grounding. FACBench provides reusable collision-focused evaluation and regression-test scenarios for retrieval-augmented autoformalization systems.

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.

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.