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