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
12 Pith papers cite this work. Polarity classification is still indexing.
12
Pith papers citing it
hub tools
citation-role summary
background 2
citation-polarity summary
years
2026 12roles
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 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
-
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.
-
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.
-
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.