CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness

Abstract

We present CAISAR, an open-source platform under active development for the characterization of AI systems' robustness and safety. CAISAR provides a unified entry point for defining verification problems by using WhyML, the mature and expressive language of the Why3 verification platform. Moreover, CAISAR orchestrates and composes state-of-the-art machine learning verification tools which, individually, are not able to efficiently handle all problems but, collectively, can cover a growing number of properties. Our aim is to assist, on the one hand, the V&V process by reducing the burden of choosing the methodology tailored to a given verification problem, and on the other hand the tools developers by factorizing useful features - visualization, report generation, property description - in one platform. CAISAR will soon be available at https://git.frama-c.com/pub/caisar.

Keywords

• eol>formal verification
• platform
• formal methods
• testing
• metamorphic testing
• reachability analysis
• satisfaction modulo theory
• artificial intelligence

1. Introduction

graded or abandoned. These tools use different techniques, different input formats, handle different ML artefacts and, The integration of machine learning programs as compo- most importantly, have varying performances depending nents of critical systems is said to be bound to happen; on the problems. Our goal of orchestrating multiple tools initiatives from various private and govermental actors aims at maximizing the property coverage in the context (e.g., US’ NSF funding for Trustworthy AI1, France’s of a validation and verification process. Grand Défi IA de confiance 2) are a consequence of that To this end, we present a platform dedicated to Charfact. Trusting such programs is thus becoming a crucial acterizing Artificial Intelligence Safety and Robustness issue, both on technical and ethical sides. (CAISAR) that aims to unify several formal methods and

A possible approach to trust is formal test and verifica- tools, at the input, through the use of a mature and exprestion, a broad set of techniques and tools that have been sive property description and proof orchestration language, applied to software safety for several decades. These for- at the output, through the factorization of features such mal methods build on sound mathematical foundations as visualization and report generation, and at the usage, to assess the behaviour of programs in a principled way, through shared heuristics and interconnections between be it for generating tests or providing proven guarantees. tools.

For the last few years, several independent works have The answer to the question “To what extent can I trust started to investigate the possible applications of formal my machine learning program?” has many components, verification to machine learning program verification and ranging from data analysis to decision explainability. One its limitations. This led to what could be characterized as such important components is dealing with verification a Cambrian explosion of tools aiming to solve a particular and validation, and we wish to make CAISAR an imsubset of the machine learning verification field. In less portant element in the safety toolbelt by covering these than vfie years, more than 20 tools were produced, up- applications.

In the following, we will first present the design principles of CAISAR and state its main goals. We will follow by a description of its most prominent features, as well as its limitations. We will then explain the position of CAISAR regarding other tools for formal verification of machine learning programs, and conclude by presenting some future work and possible research problems.

2. Core principles of CAISAR

confidence on the studied system. In order for users to trust CAISAR as well, it needs to rely on well-known and The aim for CAISAR is to provide a verification envi- approved principles and technologies. It is developed in ronment for Artificial Intelligence (AI) based systems OCaml, a strongly typed programming language, used tailored to different needs. The profusion of tools for AI- to develop tools for program verification and validation. programs certification offers numerous possibilities, from Such tools include Coq [ 1 ], a proof assistant that for inthe choice of technology (formal methods, test generation) stance used to develop CompCert[ 2 ], a C compiler that to the scope of properties to check (coverage, suitability to is guaranteed to output C-ANSI compliant source code, a given distribution, robustness). However, with increased Frama-C [ 3 ], a platform for the static analysis of C code, possibilites comes the burden of choice. Which method and Why3 [ 4 ], a platform for deductive verification of better suits a given use case? Are the results provided programs. by this particular method trustworthy enough? How to bring trust in the process of selecting, tailoring and computing results of a given tool? How to evaluate a given 2.3. Tools composition tool against others? Those are the questions that we aim to answer with CAISAR.

2.1. Compatibility with existing and future methods

The first principle of CAISAR is to ease this burden of choice by automating parts of it. CAISAR aims to provide a unique interface for vastly different tools, with a single entry point to specify verification goals. Choosing which tool to use is an informed decision that may not be relevant for the user; the goal is to provide an actionable answer on the safety of the system, by using whatever tool is suitable for the problem. Ideally, the user should not be bothered with deciding which tool is suitable for their use case: CAISAR will automatically figure out how to express the given property to suit verifiers. As AI systems pipelines are becoming more and more complex, it is crucial for CAISAR to handle this complexity. Currently, CAISAR supports neural networks and support vector machines, and an industrial benchmark of an ensemble model (NNSVM), which we are unable to further discuss, is being used as a concrete real-word use-case.

2.2. Common modelling and answers

Existing verifiers rely on different decision procedures, e.g., Mixed Integer Linear Programming (MILP), abstract interpretation, or Satisfaction Modulo Theory (SMT) calculus. Modelling a verification problem using these frameworks require different skills and is time-consuming; for instance, some modelling choices made for MILP may not be applied under SMT. Moreover, even if one succeeds in phrasing a verification problem under multiple decision procedures, the different results may not be immediately comparable.

CAISAR aims to provide a common ground for inputs and outputs, which will lead to an easier comparison, lower time consumption and an informed decision. Furthermore, collecting and presenting the user with multiple answers from different techniques can provide additional Some works are starting to combine multiple techniques [ 5 ] for their analysis, using an exact MILP solver to refine bounds obtained by abstract interpretation. Our goal with CAISAR is to bring tool composition to another level. For instance, metamorphic transformations could generate different input space partitions for formal verifiers. A reachability analysis tool could be called numerous times with tighter bounds until reaching a precise enough answer. Coverage testing objectives could be extracted from reachability analysis tools and fed to test generators. CAISAR will be more than the sum of its part, allowing communication between vastly different tools to provide faster and more accurate answers.

2.4. Automatic proposal of verification strategies

A long-term goal for CAISAR is to provide a reasoning engine where past verification problems processed by CAISAR can inform next ones, gradually building a knowledge base that is suitable for the specific needs of the user. CAISAR will also implement its own built-in heuristics to supplement specialized programs that do not implement them.

3. Architecture and features

CAISAR’s architecture can be divided into the following functional blocks:

1. A Common specification Language (CL)

2. A Proof Obligation Generator (POG), associated with a Dispatcher (DISP) 3. An Intermediate Representation (IR) 4. A visualization module (VIZ)

See fig. 1 for a visual depiction of dependencies between blocks.

3.1. Specification language and verification predicates

Ada programs [ 6 ]. This global expressiveness and safety allows to write once and for all, independently of the verifier. For instance, Figure 2 shows the definition of robustness against a perturbation of amplitude using the ∞ distance within CAISAR’s standard library, and fig. 3 the WhyML file the user need to write in order to verify the robustness of a given TestSVM against a perturbation of amplitude 0.5. Note that all the necessary element to define , namely , , and , are defined in those ifles: is the function TestSVM, and is the predicate itself. Note that WhyML is not limited to the robustness against a given perturbation property, often met in the literature. For instance, asserting that a neural network respect the properties of being differentialy private [ 7 ] or respecting causal fairness [ 8 ] is something that could be phrased as WhyML programs, since those properties have a mathematical characterization. Finally, WhyML does not constrain the form of nor . In particular, it is possible to define multiple verification goals in the same , opening the way to subdivide it into subproblems, and providing answers at each step.

CAISAR then automatically translates into a format supported by the selected verifiers, through a succession of encoding transformations and simplifications. For instance, some verifiers are best used when trying to falsify the property: instead of checking they instead try to satisfy the negation ∀ ∈ , () ⇒ ( (), ) ∃ ∈ , () ∧ ¬( (), ) A typical task for program verification involves to solve This transformation is embedded in CAISAR, when calla verification problem . A verification problem consists ing Marabou: a verification problem can be transon checking that a program with a given set of inputs is formed into an equivalent one ′ that can be dispatched meeting certain expectations on its outputs. More for- to Marabou. mally, let be an input space, (· ) be a property on the input space, be a program, and (· , · ) be a property 3.2. Proof Obligations Generations for on the output space. By property, we mean a statement various tools that describes a desirable behaviour for the program. Let = ( , , , ) be a verification problem . The goal is to verify the following property:

∀ ∈ , () ⇒ ( (), ) To write , one needs to be able to express concisely and without ambiguity each component: the program to verify , the properties and , and the dataset . To this end, CAISAR provides full support for the WhyML specification and programming language [ 4 ]. WhyML is a language with static strong typing, pattern matching, types invariants and inductive predicates. This gives WhyML programs a sound semantic as logical propositions. WhyML is at the core of the Why3 verification platform, and has been used as an intermediate language for verification of CAISAR currently supports a variety of tools and techniques: metamorphic testing, reachability analysis based on abstract interpretation and constraint-based propagations. CAISAR can analyze neural networks and support vector machines. This versatility allows for CAISAR to verify system components using different machine learning architectures.

Marabou Marabou [ 9 ] is a deep neural network verification complete verifier. Its core routine relies on a modified simplex algorithm that lazily relaxes constraints on piecewise linear activation functions. Marabou also makes use of several heuristics that help speeding up the verification procedure, like relying on tight convex overapproximations [ 10 ] or sound overapproximations [ 11 ]. It can answer reachability and conjunction of linear constraint queries. Marabou ranked fifth at the VNN-COMP 2021.

It is currently in active development.

SAVer use TestSVM . SVMasArray use i e e e _ f l o a t . F l o a t 6 4 use c a i s a r .SVM g o a l G: f o r a l l a : i n p u t _ t y p e . r o b u s t _ t o svm_apply a ( 0 . 5 : t ) The Support Vector Machine reachability analysis tool Figure 3: Example verification problem specified to SAVer [ 12 ] is specialized in the verification of support CAISAR. The program to verify is TestSVM, the input vector machines (SVM), a popular machine learning algo- space is defined by the elements in a, the output space is rithm used alongside neural networks for classification or the result of the application of the function svm_apply. regression tasks. SAVer can answer reachability queries, and supports a variety of SVM configurations. This tool was selected for support as, to the best of our knowledge, the VNNLIB standard, used in the VNN-COMP, uses a it is the first one to deal with verification of SVM. subset of SMTLIB2, which paves the way for the support of future tools in CAISAR.

Alt-Ergo and SMTLIB compliant solvers Existing general purpose SMT solvers for program verification like Alt-Ergo [ 13 ] or Z3 [ 14 ] all support a standard input language, SMTLIB [ 15 ]. CAISAR leverages Why3 existing support for SMT solvers and can translate neural network control flows directly into SMTLIB compliant strings using its intermediate representation, which allows the support of a variety of off-the-shelf solvers. Note that type i n p u t _ t y p e = i n t − > t type o u t p u t _ t y p e = i n t type model = { app : i n p u t _ t y p e − > o u t p u t _ t y p e ; num_input : i n t ; num_classes : i n t } p r e d i c a t e d i s t _ l i n f ( a : i n p u t _ t y p e ) ( b : i n p u t _ t y p e ) ( eps : t ) ( n : i n t ) = f o r a l l i . 0 <= i < n − > .− eps . < a i .− b i . < eps

Python Reachability Assessment Tool The Python Reachability Assessment Tool (PyRAT) is a static analyzer targeting specifically neural networks. It builds upon the framework of abstract interpretation [ 16 ] using abstract domains adapted for the approximation of the reachable space in a neural network. Three main domains are used: intervals with symbolic relations as described in [ 17, 18 ], zonotopes [ 19 ] and Deep poly domain [ 5 ].

For low dimensional inputs, PyRAT use input partitioning as described in [ 18 ], with heuristics tailored to relational domains: the zonotope domain and the deeppoly domain with backsubstitution. Those heuristics allow the computation of a non-trivial (e.g., not just widest interval first) score ranking the inputs by their estimated influence on the outputs. PyRAT has comparable results to state-of-the-art analyzers on the widely used ACASXu [20] benchmark, and outperforms the similar domains of ERAN on S-shape activations functions such as the sigmoid or hyperbolic tangent functions with specific approximations.

AIMOS: a Metamorphic testing utility AI Metamorphism Observing Software (AIMOS) is a p r e d i c a t e r o b u s t _ t o software developped at the same time as CAISAR, aiming ( model : model ) to provide metamorphic properties testing or perturbations ( a : i n p u t _ t y p e ) on a dataset for a given AI model. Metamorphic testing (f eoprsa:l l t b) . = d i s t _ l i n f a b eps is a testing technique relying on properties symmetries model . num_input − > and invariance on the operating domain. See [21] for a model . app a = model . app b comprehensive survey on this approach. AIMOS offers tools to derive properties from a set of transformations on the inputs: given , , and a transformation function Figure 2: An example of a predicate in CAISAR’s stan- : ∈ ↦→ , it generates a set of new properies ′ dard library: being “robust to” against a perturbation of that are coherent with the transformation. As an example, amplitude . Here, the predicate defines (). a symmetry on the inputs of a classification model could result on a symmetry on the outputs; AIMOS would then 3.4. Answer composition automatically modify the property to check against the symmetrical labels. CAISAR currently offer two ways to compose verifiers.

AIMOS can generate test cases scenarios from the First, CAISAR can launch several solvers on the same task most common input transformations (geometrical rota- and compose their answer: it can then provide a summary tions, noise addition); others can be added if necessary. stating which solver succeeded and which one failed. SecAIMOS was evaluated on a metamorphic property on the ond, CAISAR has the ability to verify pipelines that are ACAS-Xu benchmark. The aim of the property was to composed of several machine learning programs: for inevaluate the ability of neural networks trained on ACAS stance, a pipeline composed of several neural networks, or to generalize with symmetric inputs. Given a symmetry a neural network which outputs are processed by a SVM. on inputs, AIMOS generates the expected symmetrical CAISAR can be used to state an overall verification goal, output, and tests models against the base and symmetrical and to model that the outputs of a block of the pipeline outputs. See table 1 for results. AIMOS was able to show are the inputs of another block. More advanced methods that neural networks trained on ACAS have a low, but of composition, such as automatic subgoals generation noticeable sensitivity to symmetry on one input. or refinement by multiple analysis constitute a promising research venue.

The most similar work to CAISAR is the DNNV plat- instance out-of-distribution detection, is another future form [ 34 ]. As CAISAR, DNNV provides support to var- work. ious state-of-the-art verifiers. It similarly aims to be a Finally, to further help the user to select the optimal set hub for neural network verification by supporting a wide of tools for its verification problem, a long-term goal of range of input and output formats, and by providing a mod- CAISAR is to provide a verification helper to design optielling language for properties specification and discharge mal queries for verification problems based on previous to capable provers. Their Domain Specific Language, runs.

DNNP, is built on Python; while CAISAR’s specification language, WhyML, is already used in several formal verification platforms and provide additional theoretical References guarantees, which is a key component to provide trust. As stated before, WhyML allows specifying multiple verification goals in the same verification problem, which helps modelling more complex use cases.

The main difference between CAISAR and DNNV is that the latter does not combine verifiers answers, that is to say there is (at the time of writing) no feature that aims to interoperate verifiers: from the DNNV documentation5: "DNNV standardizes the network and property input formats to enable multiple verification tools to run on a single network and property. This facilitates both verifier comparison, and artifact re-use." As verifiers are becoming more and more sophisticated and specialized, combination of methods will become even more fruitful, and we expect this to be a key difference with DNNV.

5. Conclusion & future works

As the field of machine learning verification is blooming, choosing the right tool for the right verification problem becomes more and more tedious. We presented CAISAR, a platform aimed to alleviate this difficulty by presenting a single, extensible entry point to machine learning veriifcation problem modelling and solving. Plenty of work still needs to be done, however.

Altough CAISAR already integrates some state-of-theart tools, other verifiers that ranked high in the VNNCOMP are on the way of integration. Such verifiers include , -CROWN [ 23, 35 ], who scored first on said competition.

Another research venue would be the integration of neural network reparation techniques such as [ 36 ]. Corrective techniques would contribute to provide a feedback loop composed of problem specification, verification, fault identification and correction proposal.

Various problem splitting heuristics based, for instance, on [ 37, 38 ] could be integrated into CAISAR to leverage parallelism for verifiers that do not support them

Data is the cornerstone of modern machine learning systems, and it is necessary to give tools to handle its complexity. Support for more various data kinds, such as time series, is a first step towards this direction. Integration of tools for analyzing data in relation with a program, for

5https://docs.dnnv.org/en/stable/

References

[1] G. Huet , G. Kahn, C. Paulin-Mohring , The Coq Proof Assistant : A Tutorial : Version 7.2, Research Report RT-0256 , INRIA, 2002 . URL: https://hal. inria.fr/inria-00069918, projet COQ.

[2] X. Leroy , S. Blazy , D. Kästner , B. Schommer , M. Pister , C. Ferdinand , Compcert-a formally veriifed optimizing compiler , in: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress , 2016 .

[3] P. Baudin , F. Bobot , D. Bühler , L. Correnson , F. Kirchner , N. Kosmatov , A. Maroneze , V. Perrelle , V. Prevosto , J. Signoles , N. Williams , The dogged pursuit of bug-free C programs: The Frama-C software analysis platform , Communications of the ACM 64 ( 2021 ) 56 - 68 . doi: 10 .1145/3470569.

[4] J.-C. Filliâtre , A. Paskevich , Why3 - Where Programs Meet Provers, in: M. Felleisen , P. Gardner (Eds.), Programming Languages and Systems, Lecture Notes in Computer Science , Springer, Berlin, Heidelberg, 2013 , pp. 125 - 128 . doi: 10 .1007/ 978-3- 642 -37036- 6 _ 8 .

[5] G. Singh , T. Gehr , M. Püschel , M. Vechev , An abstract domain for certifying neural networks , Proceedings of the ACM on Programming Languages 3 ( 2019 ) 1 - 30 .

[6] J. Guitton , J. Kanig , Y. Moy, why hi-lite ada , Rustan , et al.[ 32 ] ( 2011 ) 27 - 39 .

[7] M. Abadi , A. Chu , I. Goodfellow , B. McMahan , I. Mironov , K. Talwar , L. Zhang, Deep Learning with Differential Privacy , in: 23rd ACM Conference on Computer and Communications Security (ACM CCS) , 2016 , pp. 308 - 318 .

[8] C. Urban , M. Christakis , V. Wüstholz , F. Zhang , Perfectly Parallel Fairness Certification of Neural Networks , arXiv: 1912 .02499 [cs] ( 2019 ). arXiv: 1912 .02499.

[9] G. Katz , D. A. Huang , D. Ibeling , K. Julian , C. Lazarus , R. Lim , P. Shah , S. Thakoor , H. Wu , A . Zeljic´, D. L. Dill , M. J. Kochenderfer , C. Barrett , The Marabou Framework for Verification and Analysis of Deep Neural Networks , in: I. Dillig , S. Tasiran (Eds.), Computer Aided Verification , volume 11561 , Springer International Publishing, Cham, 2019 , pp. 443 - 452 .

[10] H. Wu , A . Zeljic´, G. Katz, C. Barrett , Efficient Neu- K. Grauman , N. Cesa-Bianchi , R. Garnett (Eds.), ral Network Analysis with Sum-of- Infeasibilities , Advances in Neural Information Processing in: D. Fisman , G. Rosu (Eds.), Tools and Algo- Systems 31 , Curran Associates , Inc., 2018 , pp. rithms for the Construction and Analysis of Sys- 10802-10813 . URL: http://papers.nips.cc/paper/ tems, Lecture Notes in Computer Science, Springer 8278- fast- and -effective-robustness-certification . International Publishing, Cham , 2022 , pp. 143 - 163 . pdf. doi: 10 .1007/978-3- 030 -99524- 9 _ 8 . [20] G. Manfredi , Y. Jestin , An introduction to ACAS

[11] M. Ostrovsky , C. W. Barrett , G. Katz, An Xu and the challenges ahead, in: IEEE/AIAA Digabstraction-refinement approach to verifying convo- ital Avionics Systems Conference (DASC), Sacralutional neural networks , CoRR abs/2201 .01978 mento, CA, USA, 2016 . doi: 10 .1109/DASC. ( 2022 ). URL: https://arxiv.org/abs/2201. 01978 . 2016 . 7778055 . arXiv: 2201 . 01978 . [21] T. Y. Chen , F.-C. Kuo , H. Liu, P.-L. Poon , D. Towey ,

[12] F. Ranzato , M. Zanella , Robustness verification of T. Tse, Z. Q. Zhou , Metamorphic testing: A review support vector machines, in: International Static of challenges and opportunities , ACM Computing Analysis Symposium , Springer, 2019 , pp. 271 - 295 . Surveys (CSUR) 51 ( 2018 ) 1 - 27 .

[13] S. Conchon , A. Coquereau , M. Iguernlala , A . Meb- [22] G. Katz , C. Barrett , D. Dill , K. Julian , M. Kochensout , Alt-Ergo 2.2 , in: SMT Workshop: Inter- derfer, Reluplex: An efficient smt solver for national Workshop on Satisfiability Modulo Theo- verifying deep neural networks , arXiv preprint ries , Oxford, United Kingdom, 2018 . URL: https: arXiv: 1702 .01135 ( 2017 ). //hal.inria.fr/hal-01960203. [23] S. Wang , H. Zhang , K. Xu , X. Lin , S. Jana , C.-J.

[14] L. de Moura , N. Bjørner, Z3: An Efficient SMT Hsieh , J. Z. Kolter , Beta-CROWN: Efficient Bound Solver , in: C. R. Ramakrishnan, J. Rehof (Eds.), Propagation with Per-neuron Split Constraints for Tools and Algorithms for the Construction and Anal- Complete and Incomplete Neural Network Robustysis of Systems , Lecture Notes in Computer Science, ness Verification, ???? URL: http://arxiv.org/abs/ Springer, Berlin, Heidelberg, 2008 , pp. 337 - 340 . 2103 .06624. arXiv: 2103 .06624. doi: 10 .1007/978-3- 540 -78800-3_ 24 . [24] Z. Shi , H. Zhang , K.- W. Chang , M. Huang , C.-J.

[15] C. Barrett , P. Fontaine , C. Tinelli , The Sat- Hsieh, Robustness Verification for Transformers, in: isfiability Modulo Theories Library (SMT-LIB) , International Conference on Learning Representawww.SMT-LIB.org , 2016 . tions, 2020 . URL: https://openreview.net/forum?id=

[16] P. Cousot , R. Cousot , Abstract interpretation: A BJxwPJHFwS. unified lattice model for static analysis of programs [25] S. Bak , Nnenum: Verification of ReLU Neural by construction or approximation of fixpoints, in: Networks with Optimized Abstraction Refinement , POPL , 1977 , pp. 238 - 252 . in: A. Dutle , M. M. Moscato , L. Titolo , C. A.

[17] J. Li , J. Liu , P. Yang , L. Chen , X. Huang , L. Zhang , Muñoz, I. Perez (Eds.), NASA Formal Methods, Analyzing deep neural networks with symbolic prop- Lecture Notes in Computer Science , Springer Inagation: Towards higher precision and faster ver- ternational Publishing , Cham, 2021 , pp. 19 - 36 . ification, in: B. E. Chang (Ed.), Static Analy- doi:10.1007/978-3- 030 -76384- 8 _2. sis - 26th International Symposium, SAS 2019 , [26] P. Henriksen , A. Lomuscio , Efcfiient Neural NetPorto , Portugal, October 8- 11 , 2019 , Proceedings, work Verification via Adaptive Refinement and Advolume 11822 of Lecture Notes in Computer Sci- versarial Search , in: 24th European Conference ence, Springer, 2019 , pp. 296 - 319 . URL: https: on Artificial Intelligence - ECAI 2020 , Santiago de //doi.org/10.1007/978-3- 030 -32304-2_ 15 . doi:10. Compostela , Spain, 2020 , p. 8 . 1007 /978-3- 030 -32304-2\_ 15 . [27] S. Dutta , S. Jha , S. Sanakaranarayanan , A . Ti-

[18] S. Wang , K. Pei , J. Whitehouse , J. Yang , S. Jana, wari, Output Range Analysis for Deep Neural Efficient Formal Safety Analysis of Neural Net- Networks , arXiv: 1709 .09130 [cs, stat] ( 2017 ). works, in: S. Bengio, H. Wallach , H. Larochelle, arXiv: 1709 .09130. K. Grauman , N. Cesa-Bianchi , R. Garnett (Eds.), [28] A. D. Palma , R. Bunel , A. Desmaison , K. DviAdvances in Neural Information Processing jotham , P. Kohli, P. H. S. Torr , M. P. Kumar , Systems 31, Curran Associates , Inc., 2018 , Improved branch and bound for neural network pp. 6367 - 6377 . URL: http://papers.nips.cc/paper/ verification via lagrangian decomposition (????). 7873 -efficient-formal-safety-analysis-of-neural-networks . arXiv:2104 .06718v1. pdf. [29] R. Ehlers , Formal Verification of Piece-Wise Linear

[19] G. Singh , T. Gehr , M. Mirman , M. Püschel , Feed-Forward Neural Networks , arXiv: 1705 .01320 M. Vechev , Fast and Effective Robustness Certifi- [cs] ( 2017 ). arXiv: 1705 .01320. cation, in: S. Bengio, H. Wallach , H. Larochelle, [30] C. Urban , A. Miné , A Review of Formal Methods applied to Machine Learning , arXiv:2104 .02466 [cs] ( 2021 ). arXiv: 2104 . 02466 .

[31] C. Liu , T. Arnon , C. Lazarus , C. Barrett , M. J. Kochenderfer , Algorithms for Verifying Deep Neural Networks , arXiv: 1903 .06758 [cs, stat] ( 2019 ). arXiv: 1903 .06758.

[32] R. Li , J. Li , C.-C. Huang , P. Yang , X. Huang , L. Zhang , B. Xue , H. Hermanns, PRODeep: a platform for robustness verification of deep neural networks , in: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering , ESEC/FSE 2020, Association for Computing Machinery , New York, NY, USA, 2020 , pp. 1630 - 1634 . URL: https://doi.org/10.1145/3368089. 3417918. doi: 10 .1145/3368089.3417918.

[33] M. Balunovic , M. Baader , G. Singh , T. Gehr , M. Vechev , Certifying Geometric Robustness of Neural Networks, in: Advances in Neural Information Processing Systems , volume 32 , Curran Associates , Inc., 2019 . URL: https://papers.nips.cc/paper/2019/hash/ f7fa6aca028e7ff4ef62d75ed025fe76-Abstract. html.

[34] D. Shriver , S. Elbaum , M. B. Dwyer , DNNV: A Framework for Deep Neural Network Verification , in: A. Silva , K. R. M. Leino (Eds.), Computer Aided Verification, Lecture Notes in Computer Science , Springer International Publishing, Cham, 2021 , pp. 137 - 150 . doi: 10 .1007/ 978-3- 030 -81685- 8 _ 6 .

[35] K. Xu , H. Zhang , S. Wang , Y. Wang , S. Jana , X. Lin , C.-J. Hsieh , Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers , arXiv: 2011 .13824 [cs] ( 2021 ). URL: http://arxiv. org/abs/ 2011 .13824, arXiv: 2011 .13824.

[36] B. Goldberger , G. Katz, Y. Adi , J. Keshet , Minimal modifications of deep neural networks using veriifcation , in: E. Albert , L. Kovacs (Eds.), LPAR23. LPAR-23: 23rd International Conference on Logic for Programming , Artificial Intelligence and Reasoning , volume 73 of EPiC Series in Computing, EasyChair, 2020 , pp. 260 - 278 . doi: 10 .29007/699q.

[37] J. Girard-Satabin , A. Varasse , M. Schoenauer , G. Charpiat , Z. Chihani , DISCO: Division of input space into convex polytopes for neural network verification , JFLA ( 2021 ).

[38] R. Bunel , J. Lu , I. Turkaslan , P. H. Torr , P. Kohli , M. P. Kumar , Branch and bound for piecewise linear neural network verification , Journal of Machine Learning Research 21 ( 2020 ) 1 - 39 .