SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
summary
SMT encoding models LIF neurons with Linear Real Arithmetic and runs on Z3 plus SNN Torch to verify properties and adversarial robustness on IRIS and MNIST. For IRIS robustness declines as Delta increases and solver time rises; for MNIST (784 inputs, 10 outputs) verification is feasible for Delta = 1 but runtime explodes and timeouts appear for Delta ≥ 2. Paper shows correctness of the encoding but highlights scalability limits and proposes MILP and more neuron models.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:15Spiking Neural Networks (SNN)
- 0:37SNN versus Traditional Neural Networks
- 1:28SNN Example
- 3:02Leaky Integrate and Fire Neuron.
- 3:46Leaky Integrate and Fire Neuron (cont.)
- 4:40Related Work and Motivations
- 5:21Objectives and Contributions
- 5:41An SMT-Based encoding for SNNs
- 6:20Encoding of SNN
- 8:53Verification of SNNs
- 9:50Adversarial Robustness
- 14:28Conclusions and Future Work
related talks
21mModeling and Verification of Sigma Delta Neural Networks using Satisfiability Modulo(…)
59mVerification and Machine Learning
20mIncremental Verification of Neural Networks
11mExploiting Verified Neural Networks via Floating Point Numerical Error
43mThe Biological Path Towards Strong AI
42mTowards Verification of General Neural Networks: A Dual Approach
49mAn Algorithmic Theory of Brain Networks
55mNetworks of Spiking Neurons Learn to Learn and Remember