{'fraction_non_alphanumeric': 0.04098021168890934, 'fraction_numerical': 0.009364933271974228, 'mean_word_length': 4.470232850849591, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 3, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 40, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Neuro-Symbolic Verification of Deep Neural Networks

Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handful of properties that can be expressed as first-order constraints over the inputs and output of a network. While adversarial robustness and fairness fall under this category, many real-world properties (e.g.,"an autonomous vehicle has to stop in front of a stop sign") remain outside the scope of existing verification technology. To mitigate this severe practical restriction, we introduce a novel framework for verifying neural networks, named neuro-symbolic verification. The key idea is to use neural networks as part of the otherwise logical specification, enabling the verification of a wide variety of complex, real-world properties, including the one above. Moreover, we demonstrate how neuro-symbolic verification can be implemented on top of existing verification infrastructure for neural networks, making our framework easily accessible to researchers and practitioners alike.


Introduction
The exceptional performance of deep neural networks in areas such as perception and natural language processing has made them an integral part of many real-world AI systems, including safety-critical ones such as medical diagnosis and autonomous driving. However, neural networks are inherently opaque, and various defects have been found in state-of-the-art networks. The perhaps best-known one among those is the lack of adversarial robustness [Szegedy et al., 2014]. This term describes the phenomenon that even slight perturbations of an input to a neural network can cause entirely different outputs. In fact, the prevalence of defects in learning-based systems has prompted the introduction of a dedicated database to monitor AI incidents and avoid repeated undesired outcomes [McGregor, 2021]. 1 Motivated by decade-long advances in software reliability, formal verification has emerged as a powerful approach to ensure the correctness and safety of neural networks (we refer the reader to Section 2 for further details). In contrast to (empirical) statistical evaluation methods from machine learning, such as cross-validation, formal verification techniques have the great advantage that they are not limited to checking a given property on just a finite number of inputs. Instead, they allow verifying that a property holds for all (or at least infinitely many) inputs to a deep neural network, including unseen data and corner cases. However, formal verification has a fundamental limitation that often constitutes a significant obstacle in practice: it requires that the property to verify can be expressed as "simple" (typically quantifier-free, first-order) constraints over the inputs and output of the neural network.
While adversarial robustness and fairness fall under the above category, many real-world properties remain outside the scope of existing verification technology. Consider, for instance, a deep neural network controlling an autonomous vehicle and the property that the vehicle needs to decelerate as soon as a stop sign appears in the front view. It is not hard to see that formalizing this property in terms of constraints on inputs and outputs of a deep neural network is extremely difficult, if not impossible: it would require capturing all essential features of all possible stop signs, such as their position, shape, and orientation, on the level of image pixels. If this was possible, machine learning would not be necessary in the first place because one could implement a detection algorithm based on such a formal specification.
To overcome this severe limitation and make formal verification applicable to real-world scenarios, we propose a neurosymbolic framework for verifying deep neural networks. Following the general idea of neuro-symbolic reasoning [d'Avila Garcez et al., 2019;Raedt et al., 2020], our key contribution is a novel specification language, named Neuro-Symbolic Assertion Language (NESAL), that allows one to combine logical specifications and deep neural networks. The neural networks, which we call specification networks, serve as proxies for complex, semantic properties and enable the integration of advances in fields such as perception and natural language recognition into formal verification. In the context of our example above, one could train a highly-specialized specification network to detect stop signs. Then, the desired property can be expressed straightforwardly as "if the specification network detects a stop sign, the network controlling the autonomous vehicle has to issue a braking command". We present our neuro-symbolic framework in Section 3, where we also discuss ways of obtaining specification networks in practice.
An essential feature of our framework is that it can be built on top of the existing verification infrastructure for neural networks, which we demonstrate in Section 4 by presenting a prototype verifier for NESAL properties based on the popular Marabou framework [Katz et al., 2019]. In Section 5, we then show that our prototype effectively verifies a variety of neuro-symbolic properties and can produce informative counterexamples to failed verification attempts. As targets for our verification, we have trained deep neural networks on the German Traffic Sign Recognition Benchmark (GTSRB) [Stallkamp et al., 2011] and MNIST [LeCun et al., 2010].
Finally, we want to highlight that our neuro-symbolic framework is general and not limited to deep neural networks. Instead, it can-in principle-be applied to any system that allows for suitable verification techniques, including differential models, hardware, and software. However, we leave an in-depth study of this promising direction to future work.

Related Work
Driven by the demand for trustworthy and reliable artificial intelligence, the formal verification of deep neural networks has become a very active and vibrant research area over the past five years (we refer the reader to a textbook [Albarghouthi, 2021] for a detailed overview). To the best of our knowledge, Seshia et al. [2018] conducted the first comprehensive survey of correctness properties arising in neural network verification. Similar to the verification of software, the authors classify these properties into several (not necessarily disjoint) categories: system-level specifications, input-output robustness, other input-output relations, semantic invariance, monotonicity, fairness, input/distributional assumptions, coverage criteria, and temporal specifications. However, we are not aware of any work proposing a neuro-symbolic verification approach, neither for deep neural networks or other differential models nor for hardware or software.
The key motivation of neuro-symbolic AI is to combine the advantages of symbolic and deep neural representations into a joint system [d'Avila Garcez et al., 2009;d'Avila Garcez et al., 2019;Jiang and Ahn, 2020;d'Avila Garcez and Lamb, 2020]. This is often done in a hybrid fashion where a neural network acts as a perception module that interfaces with a symbolic reasoning system [Yi et al., 2018;Mao et al., 2019]. The goal of such an approach is to mitigate the issues of one type of representation by the other (e.g., using the power of symbolic reasoning to handle the generalizability issues of neural networks and to handle the difficulty of noisy data for symbolic systems via neural networks). Recent work has also demonstrated the advantage of neuro-symbolic XAI [Ciravegna et al., 2020;Stammer et al., 2021] and commonsense reasoning [Arabshahi et al., 2021]. The link to verification, however, has not been explored much.  explore symbolic propagation, but a higher-order specification framework does not exist.
To automatically verify correctness properties of deep neural networks, a host of distinct techniques have been proposed. The arguably most promising and, hence, most popular ones are abstract interpretation Singh et al., 2018;Bonaert et al., 2021;Henriksen and Lomuscio, 2021] and deductive verification [Ehlers, 2017;Katz et al., 2019]. The former performs the computation of a network abstractly on an infinite number of inputs, while the latter reduces the verification problem to a satisfiability check of logic formulas (we survey both in Section 2). In addition, various other approaches have been suggested, which are often derived from existing techniques for software verification. Examples include optimization-based methods [Gowal et al., 2019], concolic testing [Sun et al., 2018], model checking [Liu et al., 2020], refinement types [Kokke et al., 2020], and decomposition-based methods Batten et al., 2021]. While our neuro-symbolic framework is independent of the actual verification technique, we focus on deductive verification in this paper. As mentioned above, we leave an in-depth study of which other techniques can benefit from our approach for future work.

Background on Neural Network Verification
Neural Network Verification is the task of formally proving that a deep neural network satisfies a semantic property (i.e., a property that refers to the semantic function computed by the network). To not clutter this section with too many technical details, let us illustrate this task through two popular examples: adversarial robustness and fairness. We will later formalize neural network verification in Section 3 when we introduce our neuro-symbolic verification framework.
In the case of adversarial robustness, one wants to prove that a neural network is robust to small perturbations of its inputs (i.e., that small changes to an input do not change the output). To make this mathematically precise, let us assume that we are given a multi-class neural network f : R m → {c 1 , . . . , c n } with m features and n classes, a specific input x ∈ R m , a distance function d : R m × R m → R + , and a distance ε ≥ 0. Then, the task is to prove that (1) for all inputs x ∈ R m . In other words, the classes of x and every input at most ε away from x must coincide. An input x ∈ R m violating Property (1) is called an adversarial example and witnesses that f is not adversarially robust.
In the case of fairness, one wants to prove that the output of a neural network is not influenced by a sensitive feature such as sex or race. Again, let us assume that we are given a neural network f : R m → R n with m features, including a sensitive feature i ∈ {1, . . . , m}. Then, the task is to prove that for all pairs x, x ∈ R m of inputs with x = (x 1 , . . . , x m ) and x = (x 1 , . . . x m ). In other words, if two inputs x and x only differ on a sensitive feature, then the output of f must not change. Note that in the case of fairness, a counterexample consists of pairs x, x of inputs.
Properties (1) and (2) demonstrate a fundamental challenge of neural network verification: the task is to prove a property for all (usually infinitely many) inputs. Thus, cross-validation or other statistical approaches from machine learning are no longer sufficient because they test the network only on a finite number of inputs. Instead, one needs to employ methods that can reason symbolically about a given network.
Motivated by the success of modern software verification, a host of symbolic methods for the verification of neural networks have been proposed recently [Albarghouthi, 2021]. Among the two most popular are deductive verification [Ehlers, 2017;Katz et al., 2019] and abstract interpretation [Gehr et al., 2018;Singh et al., 2018]. Let us briefly sketch both.
The key idea of deductive verification is to compile a deep neural network f : R m → R n together with a semantic property P into a logic formula ψ f ,P , called verification condition. This formula typically falls into the quantifier-free fragment of real arithmetic and is designed to be valid (i.e., satisfied by all inputs) if and only if f satisfies P. To show the validity of ψ f ,P , one checks whether its negation ¬ψ f ,P is satisfiable. This can be done either with the help of an off-the-shelf Satisfiability Modulo Theory solver (such as Z3 [de Moura and Bjørner, 2008]) or using one of the recently proposed, specialized constraint solvers such as Planet [Ehlers, 2017] or Marabou [Katz et al., 2019]. If ¬ψ f ,P is unsatisfiable, then ψ f ,P is valid, and-by construction-f satisfies P. If ¬ψ f ,P is satisfiable, on the other hand, then ψ f ,P is not valid, implying that f violates the property P. In the latter case, most constraint solvers (including the ones mentioned above) can produce an assignment satisfying ¬ψ f ,P , which can then be used to extract inputs to f that witness a violation of P.
Abstract interpretation is a mathematical framework for computing sound and precise approximations of the semantics of software and other complex systems [Cousot and Cousot, 1977]. When applied to neural network verification, the basic idea is to over-approximate the computation of a deep neural network on an infinite set of inputs. Each such infinite set is symbolically represented by an element of a so-called abstract domain, which consists of logical formulas capturing shapes such as n-dimensional boxes, polytopes, or zonotopes. To approximate a network's computation, an element of the abstract domain is propagated through the layers of the network. Since layers operate on concrete values and not abstract elements, this propagation requires replacing each layer with an abstract one (called abstract transformer) that computes the effects of the layer on abstract elements. Thus, when given an abstract element A in the input space of a network f (e.g., representing the neighborhood of a fixed input x ), the result of abstract interpretation is an abstract element A in the output space over-approximating all outputs f (x) of concrete inputs x ∈ A. To verify that a property P holds, it is then enough to check whether A is included in an abstract element representing all outputs satisfying P. Since abstract interpretation computes over-approximations of the actual input-output behavior of a network, the property P typically describes a safety condition.
While neural network verification is a vibrant and highly active field, virtually all existing research suffers from three substantial shortcomings: 1. Existing research focuses on verifying "simple" proper-ties that can be formalized using quantifier-free first-order constraints on the inputs and outputs of a network. Examples of such properties include adversarial robustness and fairness, illustrated by Properties (1) and (2) above. However, the overwhelming majority of relevant correctness properties cannot be expressed in this simple way.
As an example, consider a neural network controlling an autonomous car and the property that the car needs to decelerate as soon as a stop sign appears in the front view. It is clear that formalizing this property is extremely hard (if not impossible, as Seshia and Sadigh [2016] argue): it would require us to mathematically capture all essential features of all possible stop signs, including their position, shape, angle, color, etc.
2. Virtually all properties considered in neural network verification today are either local (referring to inputs in the neighborhood of an a priori fixed input x ) or global (referring to all inputs). Adversarial robustness is an example of the former type, while fairness illustrates the latter. However, a more natural and helpful approach would be to restrict the verification to inputs from the underlying data distribution since we do typically not expect our networks to process out-of-distribution data. Again, such a restriction is very hard to capture mathematically and, therefore, not featured by current methods.

A fundamental problem, especially when verifying global
properties, is that counterexamples (i.e., inputs witnessing the violation of the property) are often out of distribution and, hence, of little value. Again, restricting the verification to inputs originating from the underlying data distribution would mitigate this issue but is not supported by current approaches.
In the next section, we address these drawbacks by introducing a neuro-symbolic framework for neural network verification.

A Neuro-Symbolic Verification Framework
As illustrated by Properties (1) and (2), the primary obstacle in today's neural network verification is that correctness properties have to be formalized in a suitable-often relatively simple-logical formalism that relates inputs and outputs of a deep neural network (e.g., the quantifier-free fragment of real arithmetic). This requirement fundamentally limits current verification approaches to only a few different types of correctness properties, arguably making them ill-equipped to tackle real-world AI verification tasks. As a first step towards overcoming this severe practical limitation, we propose a neuro-symbolic approach to neural network verification. Our main idea is seemingly simple yet powerful: we propose the use of highly specialized deep neural networks, named specification networks, as proxy objects for capturing semantic correctness properties. We introduce the concept of specification networks and possible ways of how to obtain them in Section 3.1. In Section 3.2, we then propose a fragment of quantifier-free first-order logic to formalize correctness properties involving specification networks. We call this type of properties neuro-symbolic and the resulting assertion language NESAL.
Once we have defined our new assertion language, Section 4 demonstrates how checking NESAL properties can be reduced to deductive verification of neural networks. This reduction allows utilizing any existing deductive verifier (e.g., Planet [Ehlers, 2017], Reluplex [Katz et al., 2017], or Marabou [Katz et al., 2019]), making our neuro-symbolic verification framework easily accessible to researchers and practitioners alike. It is worth pointing out that other neural network verification techniques can also be lifted to neurosymbolic verification, but we leave this research direction for future work.

Specification Networks
Generally speaking, a specification network is a highly specialized deep neural network trained for a specific task (e.g., perception, anomaly detection, recognizing the underlying data distribution, etc.). We use one (or multiple) of such networks as proxy objects to capture correctness properties. Their precise architecture does not matter at this point, but might influence the choice of which verification engine to use.
Let us illustrate the concept of specification networks using the autonomous vehicle example from Section 2. For the sake of simplicity, let us assume that we are given • a deep neural network f that takes pictures x from the front camera as input and outputs the steering commands "left", "right", "accelerate", and "decelerate"; and • a property P stating " f has to issue a deceleration command as soon as a stop sign appears in the front camera". Instead of trying to formalize all characteristics of stop signs in logic (i.e., their possible positions, shapes, colors, etc.), we now train a second deep neural network g for the specific perception task of recognizing stop signs. Assuming that g is a binary-class network (outputting "yes" if it detects a stop sign in the image x and "no" otherwise), one can then express the property P above straightforwardly as if g( x) = "yes", then f ( x) = "decelerate". (3) Note that our original property P now amounts to a simple constraint over the inputs and outputs of the networks f and g. An essential requirement of our framework is the availability of adequate specification networks. We here sketch three conceivable ways of how to obtain them: 1. The perhaps simplest way of obtaining specification networks is to train them explicitly. To avoid systematic errors, it is crucial to train a specification network on a dataset that is different from the one used to train the network under verification. Preferably, one should additionally use a different architecture and hyperparameters. 2. Similar to standard datasets such as MNIST [LeCun et al., 2010], researchers and interested companies might create public repositories for specification networks.
To boot-strap such efforts, we have made the specification networks used in our experimental evaluation (see Section 5) available at https://github.com/LebronX/ Neuro-Symbolic-Verification. 3. Finally, regulatory bodies might provide specification networks as references for future AI-enabled systems.
Such an approach can be used, for instance, to guarantee minimum standards for the correctness and reliability of neural networks in safety-critical applications. Similarly, notified bodies, such as Germany's TÜV 2 , might provide specification networks as part of their testing, certification, and advisory services.

A Neuro-Symbolic Assertion Language
Inspired by neuro-symbolic reasoning [d'Avila Garcez et al., 2019;Raedt et al., 2020], we now describe how to use specification networks to formalize correctness properties of neural networks. Specifically, we introduce an assertion language, named Neuro-Symbolic Assertion Language, which is inspired by the Hoare logic used in software verification [Hoare, 1969] and follows the notation introduced by Albarghouthi [Albarghouthi, 2021]. This language is a fragment of the quantifier-free first-order logic over the reals and allows formalizing complex correctness properties-involving multiple specification networks-in an interpretable and straightforward manner. Throughout the remainder of this paper, we assume that we are given k ∈ N specification networks g 1 , . . . , g k with g i : R m i → R n i for i ∈ {1, . . . , k}. Moreover, let us assume that we want to formalize a correctness property for a single deep neural network f : R m 0 → R n 0 , which we call the network under verification (NUV). Note that the latter assumption is not a restriction of our framework, but it simplifies the following presentation. Our framework can easily be extended to multiple networks under verification.
Let us now turn to the definition of our Neuro-Symbolic Assertion Language (NESAL). Formally, NESAL is the quantifier-free fragment of first-order logic over the reals that contains all logic formulas of the form . . , g k } for i ∈ {1, . . . , } are function symbols representing the given neural networks, one of which is the NUV f ; • x 1 , . . . , x are vectors of real variables representing the input values of the networks h i ∈ { f , g 1 , . . . , g k }; • y 1 , . . . , y are vectors of real variables representing the output values of the networks h i ∈ { f , g 1 , . . . , g k }; • the expressions y i ← h i ( x i ) store the result of the computation h i ( x i ) in the variable y i , where we assume that x i and y i match the dimensions of the input and output space of h i , respectively; • ϕ pre is a quantifier-free first-order formula over the free variables x 1 , . . . , x , called pre-condition, expressing constraints on the inputs to the networks f , g 1 , . . . , g k ; and • ϕ post is a quantifier-free first-order formula over the free variables x 1 , . . . , x and y 1 , . . . , y , called post-condition, expressing desired properties of f while considering the computations of g 1 , . . . , g k .
We call each such formula a neuro-symbolic property to emphasize that correctness properties are no longer restricted to simple first-order constraints on the inputs and outputs of the network under verification but can depend on other networks. The intuitive meaning of a neuro-symbolic property is that if the inputs x 1 , . . . , x satisfy ϕ pre and the output of the networks on these inputs is y 1 , . . . , y , then ϕ post has to be satisfied as well. Let us illustrate this definition with our example of Section 3.1. In this example, we are given a NUV f : R m×m → left, right, accelerate, decelerate mapping m × m pixel images to steering commands and a single specification network g : R m×m → yes, no detecting stop signs. Then, Property (3) can be formalized in NESAL as This neuro-symbolic property is a prototypical example of how our approach mitigates the first shortcoming of classical neural network verification discussed in Section 2. To address the second and third shortcomings, we can train an autoencoder g : R m → R m to capture the distribution underlying the training data. To restrict the verification of a network f : R m → R n to the underlying data distribution, we can use the neuro-symbolic property Here, P is the original property we want to verify, and the condition d( x, y 2 ) ≤ ε for some ε ≥ 0 follows the usual idea that a large reconstruction error (i.e., d( x, y 2 ) > ε) indicates out-ofdistribution data [Sakurada and Yairi, 2014]. As a byproduct, we obtain that any counterexample to this new property violates the original property P and originates from the underlying data distribution (as captured by the autoencoder g).
It is not hard to verify that "simple" properties, such as adversarial robustness and fairness, can easily be expressed as neuro-symbolic properties as well. For instance, adversarial robustness can be formalized in NESAL as where x ∈ R m is a fixed input, ε ≥ 0, and assuming that the distance function d can be expressed in the quantifierfree fragment of first-order logic over the reals. Note that we allow individual networks to appear multiple times in a neuro-symbolic property.
Given a neuro-symbolic property {ϕ pre } ϕ assign {ϕ post } with ϕ assign := i=1 y i ← h i ( x i ), the overall goal is to check whether the logic formula ψ := ϕ pre ∧ ϕ assign → ϕ post is valid (i.e., whether ∀ x, y : ψ is a tautology). In analogy to software verification, we call this task the neuro-symbolic verification problem and the formula ψ a neuro-symbolic verification condition. The next section demonstrates how this verification problem can be reduced to deductive verification.

Reduction to Deductive Verification
In this section, we show how to translate a neuro-symbolic property, including the network under verification and the specification networks, into a (neuro-symbolic) verification condition, whose validity we can then check using an existing constraint solver. This process is inspired by modern software verification, where it is called deductive verification. However, before we can describe our deductive verification approach in detail, we need to set up additional notation.

Background and Notation
For the purpose of deductive verification, we view a deep neural network f : R m → R n as an extended graph G f = (V,V I ,V O , E, α) where V is a finite set of vertices (i.e., neurons), V I are the input neurons, V O are the output neurons is a weighted, directed edge relation, and α is a mapping that assigns an activation function (e.g., ReLU, sigmoid, etc.) to each neuron in V \ V I . Without loss of generality, we omit the network's biases since they can easily be included in the definition of the activation functions. Moreover, we assume that the input neurons V I = {ν in,1 , . . . , ν in,m } and the output neurons V O = {ν out,1 , . . . , ν out,n } are implicitly ordered, reflecting the order of the inputs and outputs of the network.
We also need to introduce elementary background on constraint solving. To this end, let X be a set of real variables and ϕ a quantifier-free first-order formula over X . Moreover, let I : X → R be a mapping that assigns a real value to each variable in X , called an interpretation. We define satisfaction as usual (see any textbook on first-order logic for details, for instance, the one by Huth and Ryan [2000]) and write I |= ϕ if the interpretation I satisfies the formula ϕ (i.e., the interpretation of the variables in ϕ make the formula true). Although checking the satisfiability of a first-order formula is undecidable in general, a host of effective constraint solvers for specific fragments of first-order logic exist. The verification conditions we generate in the following fall in such a fragment.

Deductive Verification of Neuro-Symbolic Properties
To simplify the following presentation, let us assume for now that a given neuro-symbolic property P involves a single network under verification f : R m → R n and no specification network (we explain shortly how this restriction can be lifted). More precisely, let the property be given by where x = (x 1 , . . . , x m ), y = (y 1 , . . . , y n ), and ϕ assign ( x, y) : The key idea of our translation of P into a neuro-symbolic verification condition is to substitute the appearance of the symbol f in P with a logic formula capturing the semantics of the deep neural network. To this end, we assign to each neuron ν ∈ V a real variable X ν that tracks the output of ν for a given input to the network. For input neurons ν ∈ V I , the variables X ν are simply used to store the input values of the neural network. For all other neurons ν ∈ V \V I , the variables X ν are used to compute the output of ν given the variables of the neurons in the preceding layer. This computation can be "executed" by constraining the variable X ν using the formula which first computes the weighted sum of the inputs to ν and then applies ν's activation function α(ν). In the case of a ReLU activation function, for instance, the formula ϕ ν can be implemented straightforwardly as where Y ν is an unused, auxiliary variable. Note that ϕ ν falls into the fragment of Linear Real Arithmetic (LRA) in this specific case.
To capture the semantics of the entire network f , we can simply take the conjunction of all neuron constraints defined above. A straightforward induction over the layers of f then shows that this formula indeed simulates the computation of f on any input, as formalized in the lemma below. Note that ϕ f ranges over the variables X ν for all neurons ν ∈ V , even the input neurons.
Lemma 1 Let f : R m → R n be a deep neural network with graph representation G f = (V,V I ,V O , E, α), x = (x 1 , . . . , x m ) ∈ R m an input to f , and out ν ∈ R the output of neuron ν ∈ V when f processes the input x. Moreover, let ϕ f be as defined above and I an interpretation with I (X ν in,i ) = x i for i ∈ {1, . . . , m}. Then, I |= ϕ f if and only if I (X ν ) = out ν for each neuron ν ∈ V . In particular, f ( x) = I(X ν out,1 ), . . . , I(X ν out,n ) holds (i.e., the output of f on x can be obtained from the variables X ν out,1 , . . . , X ν out,n ).
Given the variables X ν for ν ∈ V , the construction of the neuro-symbolic verification condition is now straightforward. First, we replace the formula ϕ assign with ϕ f . Second, we substitute each occurrence of the variables x = (x 1 , . . . , x m ) and y = (y 1 , . . . , y n ) in the formulas ϕ pre and ϕ post by X V I = (X ν in,1 , . . . , X ν in,m ) and X V O = (X ν out,1 , . . . , X ν out,n ), respectively. This process then results in the verification condition where we use ϕ[ z 1 / z 2 ] to denote the formula resulting from the substitution of the vector of variables z 1 by z 2 in ϕ.
In order to determine whether the network f satisfies the neuro-symbolic property P, we now have to check whether ψ is valid (i.e., satisfied by all possible values of the free variables). Typically, this is done by checking whether the negation ¬ψ is satisfiable. If ψ is satisfiable (i.e., the property does not hold), a satisfying assignment I of ψ can be used to derive inputs to f (from X ν in,1 , . . . , X ν in,m ) that violate the property P. The correctness of this approach follows from Lemma 1 and is summarized in the theorem below.
Theorem 1 Let f be a deep neural network, P a neurosymbolic property, and ψ the neuro-symbolic verification condition as constructed above. Then, f satisfies P if and only if ¬ψ is satisfiable (i.e., ψ is valid). Additionally, if I |= ¬ψ, then I (X ν in,1 ), . . . , I (X ν in,m ) are inputs to f that violate P.
The approach described in this section can easily be generalized to neuro-symbolic properties that contain multiple specification networks g 1 , . . . , g (and even multiple networks under verification). In this case, the formula ϕ assign needs to be replaced by the conjunction ϕ f ∧ ϕ g 1 ∧ · · · ∧ ϕ g where ϕ f and ϕ g 1 , . . . , ϕ g are constructed as described above. Moreover, the variables x 1 , . . . , x and y 1 , . . . , y in the formulas ϕ pre and ϕ post now have to be replaced by their corresponding counterparts X V 1 I , . . . , X V I and X V 1 O , . . . , X V O , respectively. It is not hard to verify that a generalized version of Theorem 1 holds as well.

Building Neuro-Symbolic Verifiers on Top of Existing Verification Infrastructure
Let us now describe how to build a neuro-symbolic verifier on top of the existing verification infrastructure for deep neural network verification. After translating the given neurosymbolic property and all deep neural networks into a neurosymbolic verification condition ψ, the remaining task is to check the satisfiability of ¬ψ and extract a counterexample if the verification fails (i.e., ¬ψ is satisfiable). Since our neurosymbolic verification conditions fall into a decidable fragment of real arithmetic, one can simply apply off-the-shelf Satisfiability Modulo Theories solvers (e.g., dReal [Gao et al., 2012], CVC4 [Barrett et al., 2011], or Z3 [de Moura andBjørner, 2008]). On the level of logic, it is irrelevant whether a verification condition involves one or multiple neural networks and which of them are specification networks. The only important property is that the resulting verification condition falls into a fragment of first-order logic that the constraint solver can handle.
In addition to the "general-purpose" Satisfiability Modulo Theories solvers mentioned above, a range of specialized constraint solvers exists for the classical verification of deep neural networks with fully-connected layers or ReLU activation functions (e.g., Planet [Ehlers, 2017], Reluplex [Katz et al., 2017], and Marabou [Katz et al., 2019]). As long as the NUV and the specification networks are of this form, all three solvers can also be used for neuro-symbolic verification because Constraint (4) appears only non-negated in ¬ψ := ϕ pre ∧ ϕ assign ∧ ¬ϕ post . Consequently, the resulting verification conditions fall into a logical fragment that all three solvers can handle.
To demonstrate the ease of using existing infrastructure for neuro-symbolic verification, we have built a deductive verifier on top of the popular Marabou framework [Katz et al., 2019], called Neuro-Symbolic Verifier (NSV). Since the standard version of Marabou does not support NESAL properties-or even classical verification queries with multiple networks-, we have modified it as follows: • We have extended Marabou's input language to support multiple deep neural networks and correctness properties expressed in NESAL.
• We have added a lightweight bookkeeping mechanism to track which of the variables/constraints corresponds to which neural network.
• We have extended Marabou's reporting facilities to extract counterexamples that consist of inputs to multiple networks or relate multiple networks (using the bookkeeping mechanism described above).
These modifications did not require any substantial changes to the core of Marabou, showing that our neuro-symbolic verification framework can effortlessly be adopted in practice.

Empirical Evaluation
In this section, we demonstrate that NSV is effective in verifying a variety of neuro-symbolic properties. However, it is paramount to stress that we are not interested in the absolute performance of NSV, how well it scales to huge networks, or how it compares to other verification techniques on nonneuro-symbolic properties. Instead, our goals are twofold: (1) we demonstrate that our neuro-symbolic approach can be implemented on top of existing verification infrastructure for deep neural networks and is effective in verifying neuro-symbolic properties; and (2) we showcase that our neuro-symbolic framework can find more informative counterexamples than a purely deductive verification approach in case the verification fails. Note that the former makes it possible to leverage future progress in neural network verification to our neuro-symbolic setting, while the latter greatly improves the debugging of learning systems. In our experimental evaluation, we have considered two widely used datasets: For both datasets, the task is to predict the correct class of an input image (i.e., which sign or which digit). The remainder is structured along the two goals laid out at the beginning of this section. We first demonstrate the effectiveness of NSV in verifying neuro-symbolic properties and then show that NSV can generate more informative counterexamples to failed verification attempts. The code of NSV and all experimental data can be found online at https://github.com/LebronX/Neuro-Symbolic-Verification.

Effectiveness of Verifying Neuro-Symbolic Properties
For both the GTSRB and the MNIST datasets, we considered the following three prototypical neuro-symbolic properties. By convention, we use f to denote the network under verification (NUV) and g to denote a specification network. Moreover, we use the L ∞ -norm as distance function d.
P 1 : "If the input image x is of class c, then the NUV outputs c", expressed in NESAL as Here, the NUV f is a multi-class deep neural network mapping images to their class (i.e., one of the 43 traffic signs or one of the ten digits), while the specification network g is a deep neural network specifically trained to detect the specific class c (outputting 0 or 1). 3 P 2 : "If the input x follows the distribution of the underlying data, then the NUV classifies the input correctly with high confidence", expressed in NESAL as where ε, δ ≥ 0 and conf := (| y 1 |·y i −∑ j =i y j ) /| y 1 | is the confidence of the NUV that the input x is of class c. Here, the NUV f is a multi-class deep neural network mapping images to their class (i.e., one of the 43 traffic signs or one of the ten digits), while the specification network g is an autoencoder used to detect out-distribution data [Sakurada and Yairi, 2014] (i.e., if d( y 2 − x) > ε).
P 3 : "Two deep neural networks (of different architecture) compute the same function up to a maximum error of ε", expressed in NESAL as where ε ≥ 0. Here, the NUV f and the specification network g have the same dimensions of the input and output space but potentially distinct architectures.
For each benchmark suite, each class (remember that we have only considered ten classes of GTSRB), and each of the three properties, we have trained one NUV and one specification network with the architectures shown in Table 1 (all using ReLU activation functions). We have resized the MNIST images for property P 2 to 14 × 14 and the GTSRB images to 16 × 16 for all properties to keep the verification tractable. For property P 2 , we have chosen 0.05 ≤ ε ≤ 0.14 with step size 0.01 and 1 ≤ δ ≤ 20 with step size 1. For property P 3 , we have chosen 0.05 ≤ ε ≤ 0.14 with step size 0.01.
i5-5350U CPU (1.80 GHz) with 8 GB RAM running MacOS Catalina 10.15.7 with a timeout of 1, 800 s per benchmark. Figure 1 depicts the results of our experiments in terms of the accumulated average runtimes. On the MNIST benchmark suite, NSV timed out on one benchmark (for property P 1 ) and terminated on all others. It found a counterexample in all cases (i.e., none of the NUVs satisfied the properties). On the GTSRB suite, NSV always terminated. It proved that all NUVs satisfied property P 1 , while finding counterexamples for all benchmarks of properties P 2 and P 3 . Note that the single timeout on the MINST benchmark suite causes the steep increase in the graph of property P 1 on the left of Figure 1. Moreover, note that we have not taken any measures during the training process to ensure that our NUVs satisfy any of the properties, which explains the large number of counterexamples. We believe that the relatively low resolution of the GTSRB images causes the NUVs to satisfy property P 1 . In total, our experiments show that NSV is a versatile tool, effective at verifying a diverse set of neuro-symbolic properties. The fact that it was built on top of existing verification infrastructure further shows that our neuro-symbolic framework is easy to adopt in practice, making it accessible to researchers and practitioners alike.

Quality of Counterexamples
To assess the quality of the counterexamples generated by NSV, we have modified Property P 2 to exclude the requirement that the data must come from the underlying distribution. The resulting property P 2 , expressed in NESAL, is true y 1 ← f ( x) arg max ( y 1 ) = c → conf > δ . Figure 2: Counterexamples to the neuro-symbolic property P 2 (left) and the corresponding non-neuro-symbolic property P 2 (right) Note that P 2 involves only one network and represents a typical global property arising in classical neural network verification.
We have verified Property P 2 on the deep neural networks from the MNIST dataset using the original Marabou framework. Selected results are shown on the right-hand-side of Figure 2. Since Property P 2 is global, the verification has to consider all possible inputs. As Figure 2 demonstrates, counterexamples to such properties are often random noise and arguably of little value. In fact, we could not identify a single counterexample that looked close to the original dataset.
By contrast, the left-hand-side of Figure 2 shows two counterexamples to the neuro-symbolic property P 2 . These counterexamples are substantially more meaningful and intuitive because they originate from the underlying distribution of the data (as captured by an autoencoder trained to reconstruct the data). This demonstrates that neuro-symbolic verification produces meaningful counterexamples that can greatly simplify the development and debugging of learning systems.

Conclusion and Future Work
Today's approaches to neural network verification are limited to "simple" properties that can be formalized by quantifier-free first-order constraints. To mitigate this severe practical restriction, we have introduced the first neuro-symbolic framework for neural network verification, which allows expressing complex correctness properties through deep neural networks. We have demonstrated that our framework can straightforwardly be implemented on top of existing verification infrastructure and provides more informative counterexamples than existing methods. To the best of our knowledge, we are the first to propose a neuro-symbolic approach to formal verification.
The concept of neuro-symbolic verification can, in principle, also be applied to hardware and software verification (e.g., to express properties involving perception), and we believe that this is a promising direction of future work. Another essential future task will be to develop novel verification algorithms (e.g., based on abstract interpretation) that exploit the neuro-symbolic nature of correctness properties and can reason about multiple, inter-depending deep neural networks. To further improve scalability, we also intend to investigate neuro-symbolic approaches to (concolic) testing and symbolic execution.