SLiR parameterizes linear relaxations by slope and uses shifting to compute sound bounds for general activation functions, enabling up to 7.8x more verified properties than prior methods.
Johnson, and Haoze Wu
11 Pith papers cite this work. Polarity classification is still indexing.
11
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
years
2026 11roles
background 1polarities
background 1representative citing papers
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.
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.
Case study verifying a neural network drug-dosing controller for infinite-horizon safety using Rocq and the Vehicle theorem prover.
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.
citing papers explorer
-
Shifting-based Optimizable Linear Relaxations for General Activation Functions
SLiR parameterizes linear relaxations by slope and uses shifting to compute sound bounds for general activation functions, enabling up to 7.8x more verified properties than prior methods.
-
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.
-
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.
-
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.
- The Luna Bound Propagator for Formal Analysis of Neural Networks