Verification of fixed-precision quantized FNNs is NP-complete under both LP and BV specifications, matching the rational case, while dynamic quantization with BV specs has established upper bounds complementing known PSPACE-hardness.
Johnson, and Haoze Wu
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 1polarities
background 1representative 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.
New verification connection from C-RASP to Lustre model checkers plus local search algorithm for synthesizing C-RASP programs from examples.
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.
Adapts TP and FSDP to bound-propagation verification, with FSDP delivering bitwise-identical bounds and 80-90% baseline memory reduction while TP trades some tightness for ~2x peak-memory savings.
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.
Viverra generates C code from text descriptions together with assertions that are verified by model checkers, and a user study with over 400 participants shows the verified assertions improve code comprehension.
Super-DeepG improves linear relaxation techniques and Lipschitz optimization for neural network robustness certification against geometric perturbations, with a GPU implementation that claims better precision and speed than prior work.
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
-
The Complexity of Verifying Feedforward Neural Networks in Quantised Settings
Verification of fixed-precision quantized FNNs is NP-complete under both LP and BV specifications, matching the rational case, while dynamic quantization with BV specs has established upper bounds complementing known PSPACE-hardness.
-
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.
-
Synthesis and Verification of Transformer Programs (Technical Report)
New verification connection from C-RASP to Lustre model checkers plus local search algorithm for synthesizing C-RASP programs from examples.
-
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.
-
Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism
Adapts TP and FSDP to bound-propagation verification, with FSDP delivering bitwise-identical bounds and 80-90% baseline memory reduction while TP trades some tightness for ~2x peak-memory savings.
-
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.
-
Viverra: Text-to-Code with Guarantees
Viverra generates C code from text descriptions together with assertions that are verified by model checkers, and a user study with over 400 participants shows the verified assertions improve code comprehension.
-
Certified geometric robustness -- Super-DeepG
Super-DeepG improves linear relaxation techniques and Lipschitz optimization for neural network robustness certification against geometric perturbations, with a GPU implementation that claims better precision and speed than prior work.