LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions

DOI10.1007/978-3-030-99524-9_19MaRDI QIDQ6535572zbMATH OpenFDO

Authors Brandon Paulsen, Chao Wang

Publication date 23 January 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-99524-9_19

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Artificial neural networks and deep learning (68T07)

Recommendations

• Example Guided Synthesis of Linear Approximations for Neural Network Verification
• Analyzing deep neural networks with symbolic propagation: towards higher precision and faster verification
• Sparse polynomial optimisation for neural network verification
• Formal verification of piece-wise linear feed-forward neural networks
• Probabilistic Lipschitz analysis of neural networks

Cites work

• A Limited Memory Algorithm for Bound Constrained Optimization
• Contractor programming
• Delta-decision procedures for exists-forall problems over the reals
• DiffRNN: differential verification of recurrent neural networks
• dReal: an SMT solver for nonlinear theories over the reals
• Formal verification of piece-wise linear feed-forward neural networks
• Introduction to Interval Analysis
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Safety verification of deep neural networks
• Scalable polyhedral verification of recurrent neural networks
• Star-based reachability analysis of deep neural networks
• Verification of deep convolutional neural networks using ImageStars

This page was built for publication: LinSyn: synthesizing tight linear bounds for arbitrary neural network activation functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535572)