Back

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

Guy KatzClark BarrettDavid DillKyle JulianMykel Kochenderfer

article2017International Conference on Computer Aided Verification2,193 citations

Introduces Reluplex, a dedicated SMT solver that extends the simplex method to handle non-convex ReLU activations and formally verify safety properties of deep neural networks an order of magnitude larger than prior approaches could support.

safety critical systemsverificationcollision avoidance systemsReluplexNeural NetworksDeep Neural Networks
arXiv: 1702.01135
  • Paper: Intriguing properties of neural networks, Christian Szegedy et al. (2014). Read this foundational paper first to understand the vulnerability of deep neural networks to adversarial examples that Reluplex aims to verify and mitigate.
  • Paper: Deep Sparse Rectifier Neural Networks, Xavier Glorot et al. (2011). Read this study on rectified linear units first to master the non-linear activation function whose verification forms the core technical challenge in Reluplex.
Cover for Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

Abstract

Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.

Topics

safety critical systemsverificationcollision avoidance systemsnetwork architecturerecurrent neural networksconvolutional neural networksfeedforward neural networksdeep learningcommunication networksmesh network

Keywords

ReluplexNeural NetworksDeep Neural NetworksReLUSMTVerifying Deep NeuralSMT SolverDNNsVariablesInput

Table of Contents

  • 1 Introduction
  • 2 Background
  • Neural Networks.
  • Satisfiability Modulo Theories.
  • Linear Real Arithmetic and Simplex.
  • 3 From Simplex to Reluplex
  • The Reluplex Procedure.
  • Example.
  • 4 Efficiently Implementing Reluplex
  • Tighter Bound Derivation.
  • Derived Bounds and Conflict Analysis.
  • Floating Point Arithmetic.
  • 5 Case Study: The ACAS Xu System
  • Network Functionality.
  • Network Properties.
  • 6 Evaluation
  • 7 Related Work
  • 8 Conclusion and Next Steps
  • Acknowledgements.
  • References
  • I Verifying Properties in DNNs with ReLUs is NP-Complete
  • II The Reluplex Calculus is Sound and Complete
  • III A Reluplex Strategy that Guarantees Termination
  • IV Under-Approximations
  • V Encoding ReLUs for SMT and LP Solvers
  • VI Formal Definitions for Properties ϕ1\phi_{1},…,ϕ10\phi_{10}
  • Property ϕ1\phi_{1}.
  • Property ϕ2\phi_{2}.
  • Property ϕ3\phi_{3}.
  • Property ϕ4\phi_{4}.
  • Property ϕ5\phi_{5}.
  • Property ϕ6\phi_{6}.
  • Property ϕ7\phi_{7}.
  • Property ϕ8\phi_{8}.
  • Property ϕ9\phi_{9}.
  • Property ϕ10\phi_{10}.

Knowls

  1. Knowl 1 — Reluplex Deductive Calculus for Linear Real Arithmetic with ReLU Constraints

    algorithm

    The Reluplex calculus determines the satisfiability of conjunctions of linear real arithmetic constraints augmented with piecewise linear Rectified Linear Unit (ReLU) constraints of the form y=ReLU⁡(x)=max⁡(0,x)y = \operatorname{ReLU}(x) = \max(0, x).

    A Reluplex configuration is either SAT\text{SAT}, UNSAT\text{UNSAT}, or a tuple ⟨B,T,l,u,α,R⟩\langle B, T, l, u, \alpha, R \rangle, where:

    • B⊂XB \subset X is the set of basic variables over the variable set X={x1,…,xn}X = \{x_1, \dots, x_n\}.
    • TT is the tableau containing an equation xi=∑xj∉BTi,jxjx_i = \sum_{x_j \notin B} T_{i,j} x_j for each basic variable xi∈Bx_i \in B.
    • l,u:X→R∪{−∞,∞}l, u: X \to \mathbb{R} \cup \{-\infty, \infty\} define lower and upper variable bounds.
    • α:X→R\alpha: X \to \mathbb{R} is the current variable assignment, satisfying all equations in TT.
    • R⊂X×XR \subset X \times X is the set of pairs ⟨xi,xj⟩\langle x_i, x_j \rangle representing the constraints xj=ReLU⁡(xi)x_j = \operatorname{ReLU}(x_i).

    For any basic variable xi∈Bx_i \in B, slack sets are defined as: slack+(xi)={xj∉B∣(Ti,j>0∧α(xj)<u(xj))∨(Ti,j<0∧α(xj)>l(xj))}\text{slack}^+(x_i) = \{x_j \notin B \mid (T_{i,j} > 0 \wedge \alpha(x_j) < u(x_j)) \vee (T_{i,j} < 0 \wedge \alpha(x_j) > l(x_j))\} slack−(xi)={xj∉B∣(Ti,j<0∧α(xj)<u(xj))∨(Ti,j>0∧α(xj)>l(xj))}\text{slack}^-(x_i) = \{x_j \notin B \mid (T_{i,j} < 0 \wedge \alpha(x_j) < u(x_j)) \vee (T_{i,j} > 0 \wedge \alpha(x_j) > l(x_j))\}

    The state transitions are governed by the following guarded derivation rules:

    • Pivot1\textbf{Pivot}_1: If xi∈Bx_i \in B, α(xi)<l(xi)\alpha(x_i) < l(x_i), and xj∈slack+(xi)x_j \in \text{slack}^+(x_i), update T:=pivot(T,i,j)T := \text{pivot}(T, i, j) and B:=B∪{xj}∖{xi}B := B \cup \{x_j\} \setminus \{x_i\}.
    • Pivot2\textbf{Pivot}_2: If xi∈Bx_i \in B, α(xi)>u(xi)\alpha(x_i) > u(x_i), and xj∈slack−(xi)x_j \in \text{slack}^-(x_i), update T:=pivot(T,i,j)T := \text{pivot}(T, i, j) and B:=B∪{xj}∖{xi}B := B \cup \{x_j\} \setminus \{x_i\}.
    • Update\textbf{Update}: If xj∉Bx_j \notin B and (α(xj)<l(xj)∨α(xj)>u(xj))(\alpha(x_j) < l(x_j) \vee \alpha(x_j) > u(x_j)), choose δ\delta such that l(xj)≤α(xj)+δ≤u(xj)l(x_j) \le \alpha(x_j) + \delta \le u(x_j), and set α:=update(α,xj,δ)\alpha := \text{update}(\alpha, x_j, \delta).
    • Updateb\textbf{Update}_b: If xi∉Bx_i \notin B, ⟨xi,xj⟩∈R\langle x_i, x_j \rangle \in R, α(xj)≠max⁡(0,α(xi))\alpha(x_j) \ne \max(0, \alpha(x_i)), and α(xj)≥0\alpha(x_j) \ge 0, set α:=update(α,xi,α(xj)−α(xi))\alpha := \text{update}(\alpha, x_i, \alpha(x_j) - \alpha(x_i)).
    • Updatef\textbf{Update}_f: If xj∉Bx_j \notin B, ⟨xi,xj⟩∈R\langle x_i, x_j \rangle \in R, and α(xj)≠max⁡(0,α(xi))\alpha(x_j) \ne \max(0, \alpha(x_i)), set α:=update(α,xj,max⁡(0,α(xi))−α(xj))\alpha := \text{update}(\alpha, x_j, \max(0, \alpha(x_i)) - \alpha(x_j)).
    • PivotForRelu\textbf{PivotForRelu}: If xi∈Bx_i \in B, (∃xl.⟨xi,xl⟩∈R∨⟨xl,xi⟩∈R)(\exists x_l. \langle x_i, x_l \rangle \in R \vee \langle x_l, x_i \rangle \in R), xj∉Bx_j \notin B, and Ti,j≠0T_{i,j} \ne 0, update T:=pivot(T,i,j)T := \text{pivot}(T, i, j) and B:=B∪{xj}∖{xi}B := B \cup \{x_j\} \setminus \{x_i\}.
    • ReluSplit\textbf{ReluSplit}: If ⟨xi,xj⟩∈R\langle x_i, x_j \rangle \in R, l(xi)<0l(x_i) < 0, and u(xi)>0u(x_i) > 0, split into two branches: in one branch set u(xi):=0u(x_i) := 0 (inactive), and in the other branch set l(xi):=0l(x_i) := 0 (active).
    • ReluSuccess\textbf{ReluSuccess}: If ∀x∈X. l(x)≤α(x)≤u(x)\forall x \in X.\, l(x) \le \alpha(x) \le u(x) and ∀⟨xb,xf⟩∈R. α(xf)=max⁡(0,α(xb))\forall \langle x^b, x^f \rangle \in R.\, \alpha(x^f) = \max(0, \alpha(x^b)), transition to SAT\text{SAT}.
    • Failure\textbf{Failure}: If xi∈Bx_i \in B and (α(xi)<l(xi)∧slack+(xi)=∅)∨(α(xi)>u(xi)∧slack−(xi)=∅)(\alpha(x_i) < l(x_i) \wedge \text{slack}^+(x_i) = \emptyset) \vee (\alpha(x_i) > u(x_i) \wedge \text{slack}^-(x_i) = \emptyset), transition to UNSAT\text{UNSAT}.

  2. Knowl 2 — Encoding Feed-Forward ReLU Neural Networks into SMT Constraints

    model/method

    To formulate a feed-forward deep neural network with nn layers as an input query to the Reluplex solver, each node vv in a hidden layer is split into a pair of variables: a backward-facing variable vbv^b and a forward-facing variable vfv^f, constrained by vf=ReLU⁡(vb)≡max⁡(0,vb)v^f = \operatorname{ReLU}(v^b) \equiv \max(0, v^b).

    For a network where layer ii has size sis_i, weight matrix Wi∈Rsi×si−1W_i \in \mathbb{R}^{s_i \times s_{i-1}}, and bias vector Bi∈RsiB_i \in \mathbb{R}^{s_i}:

    1. The backward-facing variable vector Vib=[vi,1b,…,vi,sib]TV_i^b = [v_{i,1}^b, \dots, v_{i,s_i}^b]^T relates to the forward-facing outputs of the previous layer Vi−1f=[vi−1,1f,…,vi−1,si−1f]TV_{i-1}^f = [v_{i-1,1}^f, \dots, v_{i-1,s_{i-1}}^f]^T via the linear relation Vib=WiVi−1f+BiV_i^b = W_i V_{i-1}^f + B_i. This is placed in the simplex tableau by introducing basic variables ai,ja_{i,j} with lower and upper bounds fixed to 00, enforcing ai,j=−vi,jb+∑kWi,jkvi−1,kf+Bi,j=0a_{i,j} = -v_{i,j}^b + \sum_k W_{i,jk} v_{i-1,k}^f + B_{i,j} = 0.
    2. The activation step is asserted via the ReLU relation ⟨vi,jb,vi,jf⟩∈R\langle v_{i,j}^b, v_{i,j}^f \rangle \in R, with the forward variable bounded below by l(vi,jf)=0l(v_{i,j}^f) = 0.
    3. Input layer variables V1V_1 and output layer variables VnV_n are bounded by intervals defining the input domain and property-violation target conditions, respectively.

  3. Knowl 3 — Bound Tightening and Direct ReLU Elimination in Reluplex

    algorithm

    Reluplex dynamically tightens variable bounds using the tableau equations during search, which allows eliminating non-linear ReLU constraints without branching.

    For any basic variable xi∈Bx_i \in B defined by tableau equation xi=∑xj∉BTi,jxjx_i = \sum_{x_j \notin B} T_{i,j} x_j, let pos(xi)={xj∉B∣Ti,j>0}\text{pos}(x_i) = \{x_j \notin B \mid T_{i,j} > 0\} and neg(xi)={xj∉B∣Ti,j<0}\text{neg}(x_i) = \{x_j \notin B \mid T_{i,j} < 0\}. Bounds are tightened independently of the current assignment α\alpha using: deriveLowerBound:l(xi):=max⁡(l(xi),  ∑xj∈pos(xi)Ti,j⋅l(xj)+∑xj∈neg(xi)Ti,j⋅u(xj))\text{deriveLowerBound}: \quad l(x_i) := \max\left(l(x_i),\; \sum_{x_j \in \text{pos}(x_i)} T_{i,j} \cdot l(x_j) + \sum_{x_j \in \text{neg}(x_i)} T_{i,j} \cdot u(x_j)\right) deriveUpperBound:u(xi):=min⁡(u(xi),  ∑xj∈pos(xi)Ti,j⋅u(xj)+∑xj∈neg(xi)Ti,j⋅l(xj))\text{deriveUpperBound}: \quad u(x_i) := \min\left(u(x_i),\; \sum_{x_j \in \text{pos}(x_i)} T_{i,j} \cdot u(x_j) + \sum_{x_j \in \text{neg}(x_i)} T_{i,j} \cdot l(x_j)\right)

    When tighter bounds are derived for a ReLU pair ⟨xb,xf⟩∈R\langle x^b, x^f \rangle \in R representing xf=ReLU⁡(xb)x^f = \operatorname{ReLU}(x^b):

    • If l(xb)>0l(x^b) > 0 or l(xf)>0l(x^f) > 0, the ReLU is permanently fixed to its active state (xf=xbx^f = x^b).
    • If u(xb)<0u(x^b) < 0, the ReLU is permanently fixed to its inactive state (xf=0x^f = 0).

    If bound derivation leads to l(x)>u(x)l(x) > u(x) for any variable xx, a bound conflict is detected.

  4. Knowl 4 — Operational Search Strategy and Conflict Analysis in Reluplex

    algorithm

    The Reluplex execution engine interleaves linear simplex steps, bound tightening, and lazy case-splitting according to the following search strategy:

    Input: Reluplex configuration <B, T, l, u, alpha, R>
    Output: SAT with feasible assignment alpha, or UNSAT
    while true do
        while exists x in X violating bound l(x) <= alpha(x) <= u(x) do
            Apply Pivot1, Pivot2, or Update to correct the bound violation
            if Failure rule applies then
                if splitting stack is empty then
                    return UNSAT
                else
                    Perform conflict analysis, back-jump, and flip split choice
            Perform bound tightening on the entering variable
        
        if periodically scheduled then
            Perform bound tightening on all equations in tableau T
            Check for bound conflict l(x) > u(x)
            if conflict detected then
                Analyze conflicting bound derivations and back-jump multiple split levels
                
        if all bounds and all ReLU constraints in R are satisfied then
            return SAT
            
        Select a violated ReLU pair <x_b, x_f> in R
        if number of updates on <x_b, x_f> < 5 then
            if x_b is basic and x_f is basic then
                Apply PivotForRelu to make one of them non-basic
            Apply Update_b or Update_f to fix the ReLU violation
        else
            Apply ReluSplit on <x_b, x_f>, push decision to stack, and branch

  5. Knowl 5 — Floating-Point Cumulative Roundoff Error Monitoring and Tableau Restoration

    equation

    To enable the use of double-precision floating-point arithmetic while preventing numerical instability from accumulating over millions of pivots, Reluplex monitors cumulative roundoff error EE relative to the initial tableau T0T_0 and initial basic variable set B0B_0:

    E=∑xi∈B0∣α(xi)−∑xj∉B0T0 i,j⋅α(xj)∣E = \sum_{x_i \in B_0} \left| \alpha(x_i) - \sum_{x_j \notin B_0} T_{0\,i,j} \cdot \alpha(x_j) \right|

    where α\alpha is the current assignment to variables and T0 i,jT_{0\,i,j} is the initial coefficient of non-basic variable xjx_j in the definition of basic variable xix_i.

    Reluplex computes EE every 5,000 pivot steps. If E>10−6E > 10^{-6}, the coefficients of the current tableau TT are restored by taking T0T_0 and executing the shortest sequence of pivot operations necessary to reconstruct the current basis BB, resetting accumulated rounding errors.

  6. Knowl 6 — Definitions of Local and Global Adversarial Robustness for Neural Networks

    definition

    Adversarial robustness formalizes whether perturbations to the input space of a deep neural network can cause unexpected changes in output classifications:

    1. δ\delta-Local Adversarial Robustness: A network is δ\delta-locally-robust at an input point xx if every perturbed input point x′x' within an L∞L_\infty-ball of radius δ\delta receives the identical output advisory/label as xx: ∀x′.  ∥x−x′∥∞≤δ  ⟹  label⁡(x′)=label⁡(x)\forall x'.\; \|x - x'\|_\infty \le \delta \implies \operatorname{label}(x') = \operatorname{label}(x) For networks outputting scores where the minimum score indicates the chosen action, label⁡(x)=arg⁡min⁡kyk(x)\operatorname{label}(x) = \arg\min_k y_k(x).

    2. ϵ\epsilon-Global Adversarial Robustness: A network NN is ϵ\epsilon-globally-robust for input perturbation radius δ\delta if for all pairs of inputs x1,x2x_1, x_2, an input distance bounded by δ\delta implies that all output dimensions differ by at most ϵ\epsilon: ∀x1,x2.  ∥x1−x2∥∞≤δ  ⟹  max⁡k∣yk(x1)−yk(x2)∣≤ϵ\forall x_1, x_2.\; \|x_1 - x_2\|_\infty \le \delta \implies \max_k |y_k(x_1) - y_k(x_2)| \le \epsilon This property is encoded in Reluplex by instantiating two parallel copies of the network, N1N_1 and N2N_2, operating on separate input variable vectors x1x_1 and x2x_2 constrained by ∥x1−x2∥∞≤δ\|x_1 - x_2\|_\infty \le \delta.

  7. Knowl 7 — Comparative Performance of Reluplex Against SMT and LP Solvers

    data/table

    Performance of Reluplex evaluated against SMT solvers (CVC4, Z3, Yices, MathSat) and an LP solver (Gurobi) on 8 output-bound satisfiable properties (ϕ1,…,ϕ8\phi_1, \dots, \phi_8, each of the form x≥cx \ge c for an output variable xx) on 2 ACAS Xu deep neural networks (with a 4-hour timeout):

    Solver ϕ1\phi_1 ϕ2\phi_2 ϕ3\phi_3 ϕ4\phi_4 ϕ5\phi_5 ϕ6\phi_6 ϕ7\phi_7 ϕ8\phi_8
    CVC4 - - - - - - - -
    Z3 - - - - - - - -
    Yices 1 37 - - - - - -
    MathSat 2040 9780 - - - - - -
    Gurobi 1 1 1 - - - - -
    Reluplex 8 2 7 7 93 4 7 9

    Runtimes are reported in seconds; a dash (-) denotes timeout (> 14,400 seconds). SMT solvers failed on nearly all instances due to exact arithmetic overhead and the absence of specialized ReLU theory solvers. Gurobi solved only instances that did not require case-splitting, timing out on all others. Reluplex successfully solved all 8 instances in under 100 seconds each.

  8. Knowl 8 — Verification of Safety and Operational Properties on ACAS Xu Neural Networks

    data/table

    Reluplex was evaluated on 10 quantitative properties (ϕ1\phi_1 through ϕ10\phi_{10}) across a family of 45 fully connected ACAS Xu prototype DNNs (each having 6 hidden layers, 5 inputs, 5 outputs, and 300 ReLU nodes):

    Property Tested Networks Result Time (s) Avg. Stack Depth Total Splits
    ϕ1\phi_1 41 UNSAT 394517 47 1522384
    4 TIMEOUT - - -
    ϕ2\phi_2 1 UNSAT 463 55 88388
    35 SAT 82419 44 284515
    ϕ3\phi_3 42 UNSAT 28156 22 52080
    ϕ4\phi_4 42 UNSAT 12475 21 23940
    ϕ5\phi_5 1 UNSAT 19355 46 58914
    ϕ6\phi_6 1 UNSAT 180288 50 548496
    ϕ7\phi_7 1 TIMEOUT - - -
    ϕ8\phi_8 1 SAT 40102 69 116697
    ϕ9\phi_9 1 UNSAT 99634 48 227002
    ϕ10\phi_{10} 1 UNSAT 19944 49 88520

    An UNSAT result indicates that no counterexample input exists (the property is verified to hold), while SAT indicates a counterexample violating the property was found. On property ϕ8\phi_8, Reluplex found a counterexample input exposing an unintended discrepancy between the DNN and the lookup table. Across all properties, the maximum nested split depth reached (21 to 69) remained far below the total of 300 ReLU nodes in each network, showing that bound tightening and simplex updates pruned the vast majority of the 23002^{300} potential search space.

  9. Knowl 9 — Local Adversarial Robustness Verification Results on ACAS Xu DNN

    data/table

    Local adversarial robustness verification on an ACAS Xu network across 5 arbitrary input points and 5 perturbation radii δ∈{0.1,0.075,0.05,0.025,0.01}\delta \in \{0.1, 0.075, 0.05, 0.025, 0.01\}:

    Point δ=0.1\delta=0.1 Time δ=0.075\delta=0.075 Time δ=0.05\delta=0.05 Time δ=0.025\delta=0.025 Time δ=0.01\delta=0.01 Time Total (s)
    Point 1 SAT 135 SAT 239 SAT 24 UNSAT 609 UNSAT 57 1064
    Point 2 UNSAT 5880 UNSAT 1167 UNSAT 285 UNSAT 57 UNSAT 5 7394
    Point 3 UNSAT 863 UNSAT 436 UNSAT 99 UNSAT 53 UNSAT 1 1452
    Point 4 SAT 2 SAT 977 SAT 1168 UNSAT 656 UNSAT 7 2810
    Point 5 UNSAT 14560 UNSAT 4344 UNSAT 1331 UNSAT 221 UNSAT 6 20462

    Runtimes are reported in seconds. SAT indicates that an adversarial input exists within the L∞L_\infty-distance δ\delta which changes the minimal-score output advisory, whereas UNSAT proves that no such adversarial perturbation exists. Performing a binary search on δ\delta using Reluplex bounds the optimal local robustness threshold (for instance, between 0.025 and 0.05 for Point 1 and Point 4).

Coverage note — The under-approximation optimization and formal correctness proof derivations were omitted as they are detailed exclusively in the supplementary material.

References

  1. 1.Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512–526. Springer, Heidelberg (2006). doi:10.1007/11916277_35
  2. 2.Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories (Chap. 26). In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
  3. 3.Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. In: Proceedings of the 30th Conference on Neural Information Processing Systems (NIPS) (2016)
  4. 4.Bojarski, M., Del Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel, L., Monfort, M., Muller, U., Zhang, J., Zhang, X., Zhao, J., Zieba, K.: End to end learning for self-driving cars, Technical report (2016). http://arxiv.org/abs/1604.07316
  5. 5.Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)
  6. 6.Glorot, X., Bordes, A., Bengio, Y.: Deep sparse rectifier neural networks. In: Proceedings of the 14th International Conference on Artificial Intelligence and Statistics (AISTATS), pp. 315–323 (2011)
  7. 7.Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016)
  8. 8.Goodfellow, I., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples, Technical report (2014). http://arxiv.org/abs/1412.6572
  9. 9.Hinton, G., Deng, L., Yu, D., Dahl, G., Mohamed, A., Jaitly, N., Senior, A., Vanhoucke, V., Nguyen, P., Sainath, T., Kingsbury, B.: Deep neural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Sig. Process. Mag. 29(6), 82–97 (2012)
  10. 10.Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks, Technical report (2016). http://arxiv.org/abs/1610.06940
  11. 11.Jarrett, K., Kavukcuoglu, K., LeCun, Y.: What is the best multi-stage architecture for object recognition? In: Proceedings of the 12th IEEE International Conferernce on Computer Vision (ICCV), pp. 2146–2153 (2009)
  12. 12.Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21–36. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_2
  13. 13.Julian, K., Lopez, J., Brush, J., Owen, M., Kochenderfer, M.: Policy compression for aircraft collision avoidance systems. In: Proceedings of the 35th Digital Avionics Systems Conference (DASC), pp. 1–10 (2016)
  14. 14.Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex (2017). https://github.com/guykatzz/ReluplexCav2017
  15. 15.Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: an efficient smt solver for verifying deep neural networks. Supplementary Material (2017). https://arxiv.org/abs/1702.01135
  16. 16.Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 93–100 (2016)
  17. 17.King, T.: Effective algorithms for the satisfiability of quantifier-free formulas over linear real and integer arithmetic. Ph.D. thesis, New York University (2014)
  18. 18.King, T., Barret, C., Tinelli, C.: Leveraging linear and mixed integer programming for SMT. In: Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 139–146 (2014)
  19. 19.Kochenderfer, M.: Optimized airborne collision avoidance. In: Decision Making Under Uncertainty: Theory and Application. MIT Press, Cambridge (2015)
  20. 20.Kochenderfer, M., Chryssanthacopoulos, J.: Robust airborne collision avoidance through dynamic programming. Project report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (2011)
  21. 21.Kochenderfer, M., Edwards, M., Espindle, L., Kuchar, J., Griffith, J.: Airspace encounter models for estimating collision risk. AIAA J. Guidance Control Dyn. 33(2), 487–499 (2010)
  22. 22.Kochenderfer, M., Holland, J., Chryssanthacopoulos, J.: Next generation airborne collision avoidance system. Linc. Lab. J. 19(1), 17–33 (2012)
  23. 23.Krizhevsky, A., Sutskever, I., Hinton, G.: Imagenet classification with deep convolutional neural networks. In: Advances in Neural Information Processing Systems, pp. 1097–1105 (2012)
  24. 24.Kuchar, J., Drumm, A.: The traffic alert and collision avoidance system. Linc. Lab. J. 16(2), 277–296 (2007)
  25. 25.Maas, A., Hannun, A., Ng, A.: Rectifier nonlinearities improve neural network acoustic models. In: Proceedings of the 30th International Conference on Machine Learning (ICML) (2013)
  26. 26.Marques-Silva, J., Sakallah, K.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)
  27. 27.Nair, V., Hinton, G.: Rectified linear units improve restricted Boltzmann machines. In: Proceedings of the 27th International Conference on Machine Learning (ICML), pp. 807–814 (2010)
  28. 28.Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM (JACM) 53(6), 937–977 (2006)
  29. 29.Padberg, M., Rinaldi, G.: A branch-and-cut algorithm for the resolution of large-scale symmetric traveling salesman problems. SIAM Rev. 33(1), 60–100 (1991)
  30. 30.Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 243–257. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_24
  31. 31.Pulina, L., Tacchella, A.: Challenging SMT solvers to verify neural networks. AI Commun. 25(2), 117–135 (2012)
  32. 32.Riesenhuber, M., Tomaso, P.: Hierarchical models of object recognition in cortex. Nat. Neurosci. 2(11), 1019–1025 (1999). doi:10.1038/14819
  33. 33.Silver, D., Huang, A., Maddison, C., Guez, A., Sifre, L., Van Den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S.: Mastering the game of Go with deep neural networks and tree search. Nature 529(7587), 484–489 (2016)
  34. 34.Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks, Technical report (2013). http://arxiv.org/abs/1312.6199
  35. 35.Vanderbei, R.: Linear Programming: Foundations and Extensions. Springer, Heidelberg (1996)

Citation

MLA
Katz, G., et al. “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”. arXiv, 2017, http://arxiv.org/abs/1702.01135v2.
APA
Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv. http://arxiv.org/abs/1702.01135v2
Chicago
Katz, G., C. Barrett, D. Dill, K. Julian, and M. Kochenderfer. 2017. “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”. arXiv. http://arxiv.org/abs/1702.01135v2.
Harvard
Katz, G. et al. (2017) “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”, arXiv [Preprint]. Available at: http://arxiv.org/abs/1702.01135v2.
Vancouver
1. Katz G, Barrett C, Dill D, Julian K, Kochenderfer M (2017) Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. arXiv

BibTeX

@article{katz2017reluplex,
  title = {Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks},
  author = {Katz, Guy and Barrett, Clark and Dill, David and Julian, Kyle and Kochenderfer, Mykel},
  year = {2017},
  journal = {arXiv},
  url = {http://arxiv.org/abs/1702.01135v2},
  eprint = {1702.01135}
}
Metadata:arXiv

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF