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.
Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
years
2026 6representative citing papers
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.
A tensor-based batch fuzzing framework with adaptive perturbation scaling from specification ranges achieves up to 40X higher throughput and 4X more detected violations than sequential baselines on DNN benchmarks.
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.
HiTaB introduces a hierarchical Taylor bound framework for neural network reachability that systematically exploits second-order smoothness and curvature Lipschitz constants via layerwise propagation.
GeoCert uses hyperbolic geometry to unify forecasting with physical reasoning and built-in formal certification, claiming major gains in accuracy and efficiency.
citing papers explorer
-
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.
-
Tensor-Based Batch Fuzzing with Adaptive Perturbation Scaling for Deep Neural Networks
A tensor-based batch fuzzing framework with adaptive perturbation scaling from specification ranges achieves up to 40X higher throughput and 4X more detected violations than sequential baselines on DNN benchmarks.
-
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.
-
Hierarchical End-to-End Taylor Bounds for Complete Neural Network Verification
HiTaB introduces a hierarchical Taylor bound framework for neural network reachability that systematically exploits second-order smoothness and curvature Lipschitz constants via layerwise propagation.
-
GeoCert: Certified Geometric AI for Reliable Forecasting
GeoCert uses hyperbolic geometry to unify forecasting with physical reasoning and built-in formal certification, claiming major gains in accuracy and efficiency.