Fetching the paper…
Reading the bibliography…
We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems.
Checking a Large Routine
A. Turing · 1949
Earlier work this paper cites.
Classes of Recursively Enumerable Sets and Their Decision Problems
H. G. Rice · 1953
Earlier work this paper cites.
Proofs of Algorithms by General Snapshots
P. Naur · 1966
Earlier work this paper cites.
Assigning Meanings to Programs
R. W. Floyd · 1967
Earlier work this paper cites.
An Axiomatic Basis for Computer Programming
C. A. R. Hoare · 1969
Earlier work this paper cites.
A Unified Approach to Global Program Optimization
G. Kildall · 1973
Earlier work this paper cites.
Program Proving as Hand Simulation with a Little Induction
R. M. Burstall · 1974
Earlier work this paper cites.
Guarded Commands, Non-Determinacy and Formal Derivation of Programs
E. W. Dijkstra · 1975
Earlier work this paper cites.
Static Determination of Dynamic Properties of Programs
P. Cousot and R. Cousot · 1976
Earlier work this paper cites.
Abstract interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
P. Cousot and R. Cousot · 1977
Earlier work this paper cites.
The Temporal Logic of Programs
A. Pnueli · 1977
Earlier work this paper cites.
Automatic Discovery of Linear Restraints Among Variables of a Program
P. Cousot and N. Halbwachs · 1978
Earlier work this paper cites.
Specification and Verification of Concurrent Systems in CESAR
J. Queille and J. Sifakis · 1982
Earlier work this paper cites.
Classification and Regression Trees
L. Breiman, J. H. Friedman, R. A. Olshen, and C. J. Stone · 1984
Earlier work this paper cites.
Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications
E. Clarke, E. Emerson, and A. Sistla · 1986
Earlier work this paper cites.
Handwritten Digit Recognition: Applications of Neural Network Chips and Automatic Learning
Y. LeCun, L. Jackel, B. E. Boser, J. Denker, H. P. Graf, I. Guyon, D. Henderson, R. E. Howard, and W. Hubbard · 1989
Earlier work this paper cites.
Origins of the Simplex Method
G. B. Dantzig · 1990
Earlier work this paper cites.
Multilayer Feedforward Networks with a Nonpolynomial Activation Function Can Aapproximate Any Function
M. Leshno, V. Y. Lin, A. Pinkus, and S. Schocken · 1993
Earlier work this paper cites.
Symbolic Model Checking
K. McMillan · 1993
Earlier work this paper cites.
The B Book: Assigning Programs to Meanings
J. R. Abrial · 1996
Earlier work this paper cites.
Types as Abstract Interpretations
P. Cousot · 1997
Earlier work this paper cites.
Long Short-Term Memory
S. Hochreiter and J. Schmidhuber · 1997
Earlier work this paper cites.
Refining Initial Points for k-means Clustering
P. S. Bradley and U. M. Fayyad · 1998
Earlier work this paper cites.
Automatic Construction of Decision Trees from Data: A Multi-Disciplinary Survey
S. K. Murthy · 1998
Earlier work this paper cites.
Counterexample-Guided Abstraction Refinement
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith · 2000
Earlier work this paper cites.
An Introduction to Support Vector Machines and Other Kernel-based Learning Methods
N. Cristianini and J. Shawe-Taylor · 2000
Earlier work this paper cites.
Random Forests
L. Breiman · 2001
Earlier work this paper cites.
Greedy Function Approximation: A Gradient Boosting Machine
J. H. Friedman · 2001
Earlier work this paper cites.
The Elements of Statistical Learning
T. Hastie, R. Tibshirani, and J. Friedman · 2001
Earlier work this paper cites.
Interval Arithmetic: From Principles to Implementation
T. Hickey, Q. Ju and M. H. Van Emden · 2001
Earlier work this paper cites.
Gradient-Based Learning Applied to Document Recognition
Y. LeCun, L. Bottou, Y. Bengio, and P. Haffner · 2001
Earlier work this paper cites.
Lagrangian Relaxation
C. Lemaréchal · 2001
Earlier work this paper cites.
Review of Nonlinear Mixed-Integer and Disjunctive Programming Techniques
I. E. Grossmann · 2002
Earlier work this paper cites.
Formal Methods: From Academia to Industrial Practice. A Travel Guide
M. Huisman, D. Gurov, and A. Malkis · 2002
Earlier work this paper cites.
Extentions of Affine Arithmetic: Application to Unconstrained Global Optimization
F. Messine · 2002
Earlier work this paper cites.
Bounded Model Checking
A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu · 2003
Earlier work this paper cites.
Establishing Safety Criteria for Artificial Neural Networks
Z. Kurd and T. Kelly · 2003
Earlier work this paper cites.
Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
X. Yang, H.-D. Tran, W. Xiang, and T. T. Johnson · 2003
Earlier work this paper cites.
Interactive Theorem Proving and Program Development
Y. Bertot and P. Castéran · 2004
Earlier work this paper cites.
A Tool for Checking ANSI-C Programs
E. Clarke, D. Kroening, and F. Lerda · 2004
Earlier work this paper cites.
Adversarial Classification
N. Dalvi, P. Domingos, Mausam, S. Sanghai, and D. Verma · 2004
Earlier work this paper cites.
Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors
A. Miné · 2004
Earlier work this paper cites.
Safe Bounds in Linear and Mixed-Integer Linear Programming
A. Neumaier and O. Shcherbina · 2004
Earlier work this paper cites.
Adversarial Learning
D. Lowd and C. Meek · 2005
Earlier work this paper cites.
Thorough Static Analysis of Device Drivers
T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner · 2006
Earlier work this paper cites.
A Fast Linear-Arithmetic Solver for DPLL (T)
B. Dutertre and L. De Moura · 2006
Earlier work this paper cites.
Efficient Approximations for the Arctangent Function
S. Rajan, S. Wang, R. Inkol, and A. Joyal · 2006
Earlier work this paper cites.
Neural Network Robustness Verification on GPUs
C. Müller, G. Singh, M. Püschel, and M. Vechev · 2007
Earlier work this paper cites.
What Programs Want: Automatic Inference of Input Data Specifications
C. Urban · 2007
Earlier work this paper cites.
Abstract Universal Approximation for Neural Networks
Z. Wang, A. Albarghouthi, and S. Jha · 2007
Earlier work this paper cites.
Z3: An Efficient SMT Solver
L. M. de Moura and N. Bjørner · 2008
Earlier work this paper cites.
Fifteen Years of Formal Property Verification in Intel
L. Fix · 2008
Earlier work this paper cites.
Towards an Industrial Use of Fluctuat on Safety-Critical Avionics Software
D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal, and F. Vedrine · 2009
Earlier work this paper cites.
Visualizing Higher-Layer Features of a Deep Network
D. Erhan, Y. Bengio, A. Courville, and P. Vincent · 2009
Earlier work this paper cites.
The Zonotope Abstract Domain Taylor1+
K. Ghorbal, E. Goubault, and S. Putot · 2009
Earlier work this paper cites.
Learning Multiple Layers of Features from Tiny Images
A. Krizhevsky · 2009
Earlier work this paper cites.
The MNIST Database of Handwritten Digits
Y. LeCun and C. Cortes · 2009
Earlier work this paper cites.
Formal Verification of a Realistic Compiler
X. Leroy · 2009
Cited alongside, same era.
Formal Verification of Avionics Software Products
J. Souyris, V. Wiels, D. Delmas, and H. Delseny · 2009
Cited alongside, same era.
Static Analysis and Verification of Aerospace Software by Abstract Interpretation
J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and X. Rival · 2010
Cited alongside, same era.
ABC: An Academic Industrial-Strength Verification Tool
R. Brayton and A. Mishchenko · 2010
Cited alongside, same era.
A Gentle Introduction to Formal Verification of Computer Systems by Abstract Interpretation
P. Cousot and R. Cousot · 2010
Cited alongside, same era.
Static Contract Checking with Abstract Interpretation
M. Fähndrich and F. Logozzo · 2010
Cited alongside, same era.
Differentiable Abstract Interpretation for Provably Robust Neural Networks
M. Mirman, T. Gehr, and M. Vechev · 2018
Later among the works it cites.
Verifying Properties of Binarized Deep Neural Networks
N. Narodytska, S. Kasiviswanathan, L. Ryzhyk, M. Sagiv, and T. Walsh · 2018
Later among the works it cites.
Certified Defenses against Adversarial Examples
A. Raghunathan, J. Steinhardt, and P. Liang · 2018
Later among the works it cites.
Reachability Analysis of Deep Neural Networks with Provable Guarantees
W. Ruan, X. Huang, and Marta Kwiatkowska · 2018
Later among the works it cites.
Fast and Effective Robustness Certification
G. Singh, T. Gehr, M. Mirman, M. Püschel, and M. Vechev · 2018
Later among the works it cites.
Formal Verification of Random Forests in Safety-Critical Applications
J. Törnblom and S. Nadjm-Tehrani · 2018
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Rectified Linear Units Improve Restricted Boltzmann Machines
V. Nair and G. E. Hinton · 2010
Cited alongside, same era.
An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
L. Pulina and A. Tacchella · 2010
Cited alongside, same era.
LIBSVM: A Library for Support Vector Machines
C.-C. Chang and C.-J. Lin · 2011
Cited alongside, same era.
Fast Computation of Arctangent Functions for Embedded Applications: A Comparative Analysis
A. Ukil, V. H. Shah, and B. Deck · 2011
Cited alongside, same era.
Frama-C: A Software Analysis Perspective
P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski · 2012
Cited alongside, same era.
Challenging SMT Solvers to Verify Neural Networks
L. Pulina and A. Tacchella · 2012
Cited alongside, same era.
Star-Based Reachability Analysis of Deep Neural Networks
H.-D. Tran, D. M. Lopez, P. Musau, X. Yang, L. V. Nguyen, W. Xiang, and T. T. Johnson · 2018
Later among the works it cites.
An Abstract Interpretation Framework for Input Data Usage
C. Urban and P. Müller · 2018
Later among the works it cites.
Formal Security Analysis of Neural Networks Using Symbolic Intervals
S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana · 2018
Later among the works it cites.
Efficient Formal Safety Analysis of Neural Networks
S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana · 2018
Later among the works it cites.
Towards Fast Computation of Certified Robustness for ReLU Networks
T.-W. Weng, H. Zhang, H. Chen, Z. Song, C.-J. Hsieh, L. Daniel, D. Boning, and I. Dhillon · 2018
Later among the works it cites.
Provable Defenses Against Adversarial Examples via the Convex Outer Adversarial Polytope
E. Wong and Z. Kolter · 2018
Later among the works it cites.
Scaling Provable Adversarial Defenses
E. Wong, F. Schmidt, J. H. Metzen, and J. Z. Kolter · 2018
Later among the works it cites.
Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks
W. Xiang, H.-D. Tran, and T. T. Johnson · 2018
Later among the works it cites.
Efficient Neural Network Robustness Certification with General Activation Functions
H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel · 2018
Later among the works it cites.
Provably Robust Boosted Decision Stumps and Trees Against Adversarial Attacks
M. Andriushchenko, and M. Hein · 2019
Later among the works it cites.
CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks
A. Boopathy, T.-W. Weng, P.-Y. Chen, S. Liu, and L. Daniel · 2019
Later among the works it cites.
Adversarial Training of Gradient-Boosted Decision Trees
S. Calzavara, C. Lucchese, and G. Tolomei · 2019
Later among the works it cites.
Robust Decision Trees Against Adversarial Examples
H. Chen, H. Zhang, D. Boning, and C.-J. Hsieh · 2019
Later among the works it cites.
Robustness Verification of Tree-based Models
H. Chen, H. Zhang, S. Si, Y. Li, D. Boning, and C.-J. Hsieh · 2019
Later among the works it cites.
Calculational Design of a Regular Model Checker by Abstract Interpretation
P. Cousot · 2019
Later among the works it cites.
Syntactic and Semantic Soundness of Structural Dataflow Analysis
P. Cousot · 2019
Later among the works it cites.
Abstract Semantic Dependency
P. Cousot · 2019
Later among the works it cites.
Responsibility Analysis by Abstract Interpretation
C. Deng and P. Cousot · 2019
Later among the works it cites.
Scaling Static Analyses at Facebook
D. Distefano, M. Fähndrich, F. Logozzo, and P. W. O’Hearn · 2019
Later among the works it cites.
VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems
T. Dreossi, D. J. Fremont, S. Ghosh, E. Kim, H. Ravanbakhsh, M. Vazquez-Chanlatte, and S. A. Seshia · 2019
Later among the works it cites.
Verifying Robustness of Gradient Boosted Models
G. Einziger, M. Goldstein, Y. Sa’ar, I. Segall · 2019
Later among the works it cites.
Property Inference for Deep Neural Networks
D. Gopinath, H. Converse, C. S. Pasareanu, and A. Taly · 2019
Later among the works it cites.
The Marabou Framework for Verification and Analysis of Deep Neural Networks
G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljić, D. L. Dill, M. J. Kochenderfer, and C. W. Barrett · 2019
Later among the works it cites.
POPQORN: Quantifying Robustness of Recurrent Neural Networks
C.-Y. Ko, Z. Lyu, T.-W. Weng, L. Daniel, N. Wong, and D. Lin · 2019
Later among the works it cites.
Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification
J. Li, J. Liu, P. Yang, L. Chen, X. Huang, and L. Zhang · 2019
Later among the works it cites.
Abstraction based Output Range Analysis for Neural Networks
P. Prabhakar and Z. R. Afza · 2019
Later among the works it cites.
Robustness Verification of Support Vector Machines
F. Ranzato, M. Zanella · 2019
Later among the works it cites.
An Abstract Domain for Certifying Neural Networks
G. Singh, T. Gehr, M. Püschel, and M. Vechev · 2019
Later among the works it cites.
Boosting Robustness Certification of Neural Networks
G. Singh, T. Gehr, M. Püschel, and M. Vechev · 2019
Later among the works it cites.
Beyond the Single Neuron Convex Barrier for Neural Network Certification
G. Singh, R. Ganvir, M. Püschel, and M. Vechev · 2019
Later among the works it cites.
Evaluating Robustness of Neural Networks with Mixed Integer Programming
V. Tjeng, K. Xiao, and R. Tedrake · 2019
Later among the works it cites.
An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles
J. Törnblom and S. Nadjm-Tehrani · 2019
Later among the works it cites.
Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks
H.-D. Tran, P. Musau, D. M. Lopez , X. Yang, L. V. Nguyen, W. Xiang, and T. T. Johnson · 2019
Later among the works it cites.
Robustness May Be at Odds with Accuracy
D. Tsipras, S. Santurkar, L. Engstrom, A. Turner, and A. Madry · 2019
Later among the works it cites.
Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability
K. Y. Xiao, V. Tjeng, N. M. M. Shafiullah, and A. Madry · 2019
Later among the works it cites.
Universal Approximation with Certified Networks
M. Baader, M. Mirman, and M. Vechev · 2020
Later among the works it cites.
Adversarial Training and Provable Defenses: Bridging the Gap
M. Balunović and M. Vechev · 2020
Later among the works it cites.
Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
S. Bak, H.-D. Tran, K. Hobbs, and T. T. Johnson · 2020
Later among the works it cites.
Certifying Decision Trees Against Evasion Attacks by Program Analysis
S. Calzavara, P. Ferrara, C. Lucchese · 2020
Later among the works it cites.
An Abstraction-Based Framework for Neural Network Verification
Y. Y. Elboher, J. Gottschlich, and G. Katz · 2020
Later among the works it cites.
Gurobi Optimizer Reference Manual
Gurobi Optimization, LLC · 2020
Later among the works it cites.
Abstract Interpretation of Decision Tree Ensemble Classifiers
F. Ranzato and M. Zanella · 2020
Later among the works it cites.
Formal Verification of Decision-Tree Ensemble Model and Detection of its Violating-Input-Value Ranges
N. Sato, H. Kuruma, Y. Nakagawa, and H. Ogawa · 2020
Later among the works it cites.
Abstract Neural Networks
M. Sotoudeh and A. V. Thakur · 2020
Later among the works it cites.
Formal Verification of Input-Output Mappings of Tree Ensembles
J. Törnblom and S. Nadjm-Tehrani · 2020
Later among the works it cites.
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
H.-D. Tran, X. Yang, D. M. Lopez, P. Musau, L. V. Nguyen, W. Xiang, S. Bak, and T. T. Johnson · 2020
Later among the works it cites.
Verification of Deep Convolutional Neural Networks Using ImageStars
H.-D. Tran, S. Bak, W. Xiang, and T. T. Johnson · 2020
Later among the works it cites.
Perfectly Parallel Fairness Certification of Neural Networks
C. Urban, M. Christakis, V, Wüstholz, and F. Zhang · 2020
Later among the works it cites.
Towards Stable and Efficient Training of Verifiably Robust Neural Networks
H. Zhang, H. Chen, C. Xiao, S. Gowal, R. Stanforth, B. Li, D. Boning, and C.-J. Hsieh · 2020
Later among the works it cites.
Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis
H. Zhang, M. Shinn, A. Gupta, A. Gurfinkel, N. Le, and N. Narodytska · 2020
Later among the works it cites.