k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics
This paper introduces k-inductive neural barrier certificates (k-NBCs) for safety verification of partially unknown nonlinear dynamical systems. The approach relaxes strict conventional barrier conditions by allowing temporary function increases up to k-1 times, and combines neural networks with a CEGIS-SMT verification framework. To handle unknown dynamics, it leverages a data-driven representation via Willems et al.'s fundamental lemma from a single state trajectory, avoiding the need for explicit system models. The method is validated on three nonlinear case studies.
Related guides (1)
Related events (8)
Verifiable Belief-Space Neural Safety Filters for Interactive Robotics via Conformal Prediction
This paper proposes an algorithmic framework to certify high-probability safety of belief-space safety filters (BeliefSF) in interactive robotics, addressing the challenge that neural approximations and runtime inference errors make formal guarantees difficult. The approach uses conformal prediction focused on regions where inference is reliable, preserving standard sample complexity while certifying a less conservative filter. Evaluation on a simulated human-vehicle interaction benchmark demonstrates the method produces significantly more permissive safety guarantees than a standard conformal prediction baseline.
KAFFEE: Addressing the Dynamic-Probabilistic Consistency Gap in Chaotic Surrogate Modeling
This paper identifies a 'dynamic-probabilistic consistency (DPC) gap' in dynamical systems reconstruction (DSR), where optimizing finite-horizon probabilistic objectives can degrade learned dynamics or decouple predictive uncertainty from local tangent dynamics. Three failure mechanisms are isolated: core collapse, noise masking, and blind uncertainty. The authors propose KAFFEE, a differentiable extended Kalman filter-based training framework that evaluates likelihood on local predictive residuals while transporting covariance through learned Jacobians, reducing these failure modes on stochastic hyperchaotic Lorenz-96 and across 13 chaotic systems when adapting a DSR foundation model.
Neuronal Stochastic Attention Circuit (NSAC) for Probabilistic Representation Learning
Researchers introduce NSAC, a biologically-inspired continuous-time attention architecture that models attention logits as solutions to an Ornstein-Uhlenbeck stochastic differential equation, drawing on C. elegans Neuronal Circuit Policy wiring to induce Gaussian distributions over attention weights. The architecture enables joint quantification of aleatoric and epistemic uncertainty via a two-term objective combining Gaussian negative log-likelihood with an epistemic-separation regularizer. Empirical evaluation spans irregular time-series function approximation, multivariate regression, long-range forecasting, Industry 4.0 tasks, and autonomous vehicle lane-keeping, showing competitive accuracy with well-calibrated uncertainty estimates.
IA-VQC-DPC: Intervention-aware quantum predictive control with safety attribution for learned policies
A new arXiv preprint introduces Intervention-Aware Variational Quantum Differentiable Predictive Control (IA-VQC-DPC), a framework that trains variational quantum circuit policies under a primal-dual intervention budget to penalize over-reliance on downstream safety filters (Control-Barrier-Function projections). The work also proposes a safety-attribution protocol that decomposes trajectory corrections into policy-level versus filter-level contributions, enabling measurement of whether a policy has genuinely learned safe behavior or is merely being silently repaired by its safety layer. Experiments on BOPTEST building-control emulators show the quantum policy achieves significantly lower pre-filter violations than a matched classical policy at equal parameter budget, with a notable negative result: a learned energy head is only safe when paired with a distribution-aware runtime guard.
WorldKernel: Formalizing world models as coupling kernels over counterfactual worlds
A new arXiv preprint identifies a structural failure mode in prediction-based world models: strong predictors can recover the diagonal of a counterfactual coupling kernel (ordinary posteriors) but systematically fail on off-diagonal cross-world couplings, collapsing to point estimates that are sometimes provably inadmissible. The authors formalize a world model as a positive semidefinite kernel K(T,T') over admissible possible worlds, showing the off-diagonal encodes counterfactual structure that more data cannot resolve. They demonstrate that PSD constraints provide partial identification bounds computable in polynomial time, that ontological axioms tighten these bounds, and that targeted constraint learning ('scars') closes the gap faster than untargeted approaches. The work has implications for causal reasoning in AI systems and the theoretical limits of learned world models.
Neurosymbolic Learning for Inference-Time Argumentation in Claim Verification
This paper introduces Inference-Time Argumentation (ITA), a trainable neurosymbolic framework for ternary claim verification (true/false/uncertain) that integrates formal argumentation semantics with LLM training. The framework uses argumentation semantics both to guide LLM training for argument generation and scoring, and to compute final predictions deterministically from explicit argumentative structures. Unlike conventional reasoning models that rely on potentially unfaithful post-hoc explanations, ITA produces verdicts that are faithful by construction to the underlying arguments. Experiments on two ternary claim verification datasets show ITA outperforms argumentative baselines and competes with non-argumentative direct-prediction approaches.
BIRDNet: Interpretable Neural Networks via Boolean Implication Knowledge Graphs for Tabular Data
BIRDNet is a neurosymbolic architecture that mines Boolean implication relationships (BIRs) from tabular data using a sparse-exception binomial test, then encodes the resulting directed graph as the connectivity structure of a layered neural network. Each hidden unit corresponds to exactly one mined rule and binds only to its two features, yielding up to 96× parameter reduction versus a matched dense MLP. Evaluated on six transcriptomic and proteomic benchmarks, BIRDNet stays within 0.02 AUROC of dense baselines while recovering known biological signatures such as canonical amplicons and immune-infiltration markers. Unlike most neurosymbolic approaches, BIRDNet derives its structural prior from data rather than an external rule base.
Gated DeltaNet-2: Decoupling Erase and Write Gates in Linear Attention
Gated DeltaNet-2 is a new linear attention architecture from NVIDIA Labs that separates the erase and write operations in the delta-rule update into independent channel-wise gates, generalizing both Gated DeltaNet and Kimi Delta Attention (KDA). The model introduces a chunkwise WY algorithm with channel-wise decay and a gate-aware backward pass for efficient parallel training. At 1.3B parameters trained on 100B FineWeb-Edu tokens, it outperforms Mamba-2, Gated DeltaNet, KDA, and Mamba-3 variants on language modeling, commonsense reasoning, and long-context RULER needle-in-a-haystack retrieval benchmarks. Code is publicly released via NVlabs on GitHub.
