SLiR parameterizes linear relaxations by slope and uses shifting to compute sound bounds for general activation functions, enabling up to 7.8x more verified properties than prior methods.
hub
The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results
15 Pith papers cite this work. Polarity classification is still indexing.
15
Pith papers citing it
hub tools
citation-role summary
background 2
citation-polarity summary
years
2026 15roles
background 2polarities
background 2representative citing papers
Formal verification method using Lipschitz optimization on homographies to certify vision network robustness to camera pose changes in predominantly planar scenes.
A reusable framework generates verification instances with provably known robustness labels, revealing numeric tolerance issues and bugs in five verifiers while introducing difficulty profiles to diagnose failure modes.
QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empirical robustness and formal verification than prior approaches.
VNN-LIB 2.0 defines a network theory abstraction, formal query syntax, type system over numeric domains, and Agda-mechanized semantics to provide rigorous foundations for neural network verification independent of evolving model formats.
Differential halo zonotopes enable static verification of global robustness in DNNs by jointly propagating pairs of perturbed inputs while bounding divergence, with a relaxed confidence-based variant.
MLSkip demonstrates that lightweight metadata enables data skipping for ReLU-based ML filters, with 27.4% average pruning using min-max and 38.31% using 2D convex hulls on TPC benchmarks, for a 1.07x end-to-end speedup.
Introduces partial multi-neuron relaxation using existing branching heuristics to balance bound tightness and scalability in neural network verification, with integration into Marabou showing positive experimental comparisons.
A JAX-based differentiable reachability primitive for continuous- and discrete-time NN dynamics and controllers that supports certified training and sampling-based MPC with gradient refinement.
A ReLU-catalyzed abstraction method yields tighter bounds for transformer verification by converting dot-product constraints into ReLU forms that leverage standard convex relaxations.
A polynomial-based circuit model combined with polynomial zonotope reachability analysis verifies analog neural networks under process variations, reducing verification time from days to seconds while enclosing 99% of variation samples across three datasets.
Certified 3D pose estimation from camera images using reachability analysis and formal NN verification delivers formal bounds for safety-critical localization.
Certified robustness varies extremely across training seeds with std larger than recent gains, and generalizes poorly to unseen data.
Case study verifying a neural network drug-dosing controller for infinite-horizon safety using Rocq and the Vehicle theorem prover.
Luna delivers a C++ bound propagator supporting interval, DeepPoly/CROWN, and alpha-CROWN analyses that reports tighter bounds and higher speed than the leading Python alpha-CROWN implementation on VNN-COMP 2025 benchmarks.
citing papers explorer
-
Shifting-based Optimizable Linear Relaxations for General Activation Functions
SLiR parameterizes linear relaxations by slope and uses shifting to compute sound bounds for general activation functions, enabling up to 7.8x more verified properties than prior methods.
-
Lipschitz Optimization for Formal Verification of Homographies
Formal verification method using Lipschitz optimization on homographies to certify vision network robustness to camera pose changes in predominantly planar scenes.
-
Stress-Testing Neural Network Verifiers with Provably Robust Instances
A reusable framework generates verification instances with provably known robustness labels, revealing numeric tolerance issues and bugs in five verifiers while introducing difficulty profiles to diagnose failure modes.
-
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empirical robustness and formal verification than prior approaches.
-
VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification
VNN-LIB 2.0 defines a network theory abstraction, formal query syntax, type system over numeric domains, and Agda-mechanized semantics to provide rigorous foundations for neural network verification independent of evolving model formats.
-
Differential Zonotopes for Verifying Global Robustness of DNNs
Differential halo zonotopes enable static verification of global robustness in DNNs by jointly propagating pairs of perturbed inputs while bounding divergence, with a relaxed confidence-based variant.
-
MLSkip: Data Skipping for ML Filters via Lightweight Metadata
MLSkip demonstrates that lightweight metadata enables data skipping for ReLU-based ML filters, with 27.4% average pruning using min-max and 38.31% using 2D convex hulls on TPC benchmarks, for a 1.07x end-to-end speedup.
-
Neural Network Verification using Partial Multi-Neuron Relaxation
Introduces partial multi-neuron relaxation using existing branching heuristics to balance bound tightness and scalability in neural network verification, with integration into Marabou showing positive experimental comparisons.
-
Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers
A JAX-based differentiable reachability primitive for continuous- and discrete-time NN dynamics and controllers that supports certified training and sampling-based MPC with gradient refinement.
-
Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement
A ReLU-catalyzed abstraction method yields tighter bounds for transformer verification by converting dot-product constraints into ReLU forms that leverage standard convex relaxations.
-
Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes
A polynomial-based circuit model combined with polynomial zonotope reachability analysis verifies analog neural networks under process variations, reducing verification time from days to seconds while enclosing 99% of variation samples across three datasets.
-
Perception with Guarantees: Certified Pose Estimation via Reachability Analysis
Certified 3D pose estimation from camera images using reachability analysis and formal NN verification delivers formal bounds for safety-critical localization.
-
On the Extreme Variance of Certified Local Robustness Across Model Seeds
Certified robustness varies extremely across training seeds with std larger than recent gains, and generalizes poorly to unseen data.
-
Vancomycert: A Certified Neuro-Symbolic Drug Delivery System (Case Study)
Case study verifying a neural network drug-dosing controller for infinite-horizon safety using Rocq and the Vehicle theorem prover.
-
The Luna Bound Propagator for Formal Analysis of Neural Networks
Luna delivers a C++ bound propagator supporting interval, DeepPoly/CROWN, and alpha-CROWN analyses that reports tighter bounds and higher speed than the leading Python alpha-CROWN implementation on VNN-COMP 2025 benchmarks.