Formal verification method using Lipschitz optimization on homographies to certify vision network robustness to camera pose changes in predominantly planar scenes.
hub
The 6th international verification of neural networks competition (VNN-COMP 2025): Summary and results
13 Pith papers cite this work. Polarity classification is still indexing.
13
Pith papers citing it
hub tools
citation-role summary
background 2
citation-polarity summary
years
2026 13roles
background 2polarities
background 2representative citing papers
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.
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
-
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.
-
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.