PaperlayerView exact revision on arXiv

Source-linked AI summary

Concolic Testing for Deep Neural Networks

Youcheng Sun, Min Wu, Wenjie Ruan, Xiaowei Huang, Marta Kwiatkowska, Daniel Kroening

arXiv:1805.00089v2cs.LGcs.SEstat.ML

TL;DR

DNNs require systematic testing because faulty behavior can threaten safety and security, while existing approaches do not implement concolic testing. The paper introduces a coverage-parameterized method that alternates concrete execution and symbolic analysis, and experiments report high coverage and significant adversarial-example discovery.

  • Problem

    Existing DNN testing approaches provide limited systematic coverage, despite safety and security concerns for systems using DNN components.

  • Method

    The paper develops the first DNN concolic testing method, expressing coverage requirements in QLAR and alternating concrete execution with symbolic analysis.

  • Results

    The method achieves high coverage across broad coverage requirements and discovers a significant number of adversarial examples.

  • Takeaways & Limitations

    Combining concrete execution and symbolic analysis supports coverage-guided DNN testing and automated adversarial-example discovery.

  • Takeaways & Limitations

    Full Lipschitz coverage is typically impossible because some coverage requirements may be inconsistent, and corner-case activation coverage is limited.

Abstract

from arXiv · show

Concolic testing combines program execution and symbolic analysis to explore the execution paths of a software program. This paper presents the first concolic testing approach for Deep Neural Networks (DNNs). More specifically, we formalise coverage criteria for DNNs that have been studied in the literature, and then develop a coherent method for performing concolic testing to increase test coverage. Our experimental results show the effectiveness of the concolic testing approach in both achieving high coverage and finding adversarial examples.

1 Introduction

The paper introduces the first concolic testing method for DNNs, combining concrete execution and symbolic analysis to improve coverage and find adversarial examples. It evaluates the method across diverse coverage requirements and implements it in DeepConcolic.

  • DNN testing matters because faulty behavior in safety- and security-critical systems can endanger lives or cause financial damage.
  • Existing DNN testing approaches use concrete execution or symbolic execution, but none implement concolic testing.
  • Concolic testing alternates concrete execution and symbolic analysis to target difficult-to-cover DNN execution paths.
  • The method expresses coverage requirements in QLAR and iteratively generates new inputs by selecting near-satisfying tests and solving symbolically for satisfying inputs.
  • The method is implemented in DeepConcolic and evaluated over broad coverage requirements, including Lipschitz continuity and structural metrics.
  • DeepConcolic achieves high coverage and discovers a significant number of adversarial examples.

2 Related Work

Related work includes robustness analysis and coverage-driven DNN testing, while concolic testing combines concrete and symbolic execution to guide input generation. DeepConcolic is presented as a generic alternative to ad hoc coverage methods.

  • 2.1 Robustness of DNNs: DNN robustness research spans offensive searches for adversarial examples and defensive techniques intended to increase robustness.
  • 2.1 Robustness of DNNs: Automated verification methods face state-space explosion or scalability limits, including constraint-based approaches restricted to small DNNs.
  • 2.2 Concolic Testing: Coverage-driven DNN testing has used neuron, MC/DC-inspired, and activation-value criteria, followed by oracle-based adversarial-example searches.
  • 2.2 Concolic Testing: Concolic testing alternates concrete execution with symbolic path solving to generate new concrete inputs, with heuristics affecting coverage.
  • 2.3 Comparison with Related Work: DeepConcolic accepts coverage requirements generically, whereas other coverage-driven methods are tailored to specific requirements.
  • 2.3 Comparison with Related Work: DeepConcolic can achieve good coverage from a single input, while other compared methods require a non-trivial input set.
  • 2.3 Comparison with Related Work: DeepConcolic separates test-input generation from the test oracle, unlike methods that incorporate the oracle into generation objectives.

3 Deep Neural Networks

The paper models a DNN as connected layers with activation functions and defines neuron values before and after activation. Inputs instantiate the network and determine its output label.

  • A DNN is represented as a tuple of layers, connections between layers, and activation functions.
  • Hidden-neuron values pass through ReLU, whose activation or deactivation is determined by the input.
  • Each layer contains neurons whose values are propagated through pre-defined weights and biases from preceding layers.
  • The output label is the index of the output-layer neuron with the largest activation value.
  • For an input t, the instantiated network records neuron activations before and after ReLU as u[t] and v[t].
  • Although the formal definition focuses on fully connected and convolutional layers, the method also applies to layers such as maxpooling.

4 Test Coverage for DNNs

The paper models DNN activation patterns and expresses diverse coverage requirements in a quantified linear-arithmetic fragment, enabling one coverage metric and generation framework. Coverage measures the percentage of requirements satisfied and serves as a proxy for confidence in DNN safety.

  • Activation Patterns: DNN activation patterns represent the linear behaviours induced by fixed ReLU activation states for particular inputs.Each hidden neuron is mapped to whether its ReLU is activated, and the resulting pattern can be encoded using linear programming.
  • Requirement Language: The DR fragment expresses existential or universal requirements over one or two inputs using Boolean, arithmetic, and counting operators.Variables range over network inputs and rational-valued neuron variables; DR+ disallows negation.
  • Coverage Framework: A single test-input generation algorithm supports a variety of coverage criteria expressed in DR.The common formula language provides the basis for using one generation procedure across different criteria.
  • Requirement Language: DR formulas can encode activation agreement or disagreement and distance constraints such as ||x1 − x2||∞ ≤ q.The shared representation supports requirements involving neuron activation behaviours and norm-based distances between inputs.
  • Coverage Framework: Coverage satisfaction is defined recursively over test suites, quantified inputs, Boolean combinations, and counts of satisfied expressions.For existential formulas, one or two tests from the suite must make the instantiated expression true; conjunction and counting follow their stated semantics.
  • Coverage Metric: Checking whether a finite test suite satisfies a DR requirement is polynomial in suite size, whereas finding a satisfying test suite is NP-complete.The coverage metric is the percentage of requirements satisfied by the test suite and is used as a safety-confidence proxy.

5 Specific Coverage Requirements

The paper instantiates its coverage language with semantic Lipschitz requirements and structural criteria for neuron activation, independent sign effects, and activation boundaries. Full Lipschitz coverage may be impossible when requirements are inconsistent.

  • Coverage Criteria: The coverage criteria include Lipschitz continuity and structural metrics related to neuron activation and conventional software coverage.Lipschitz continuity is semantic and connected in the paper to DNN theory and robustness, while the other criteria have structural-test analogues.
  • Lipschitz Coverage: Lipschitz coverage seeks input pairs within each subspace that refute a proposed Lipschitz constant c.The paper notes that the best Lipschitz constant is NP-hard to compute and that smaller constants can improve verification performance.
  • Lipschitz Coverage: Full Lipschitz coverage is typically impossible because some requirements may be inconsistent, so generation aims to satisfy as many requirements as possible.The coverage objective is therefore maximization over the feasible requirements induced by the selected subspaces and constant.
  • Neuron Coverage: Neuron Coverage requires every hidden neuron to be activated by at least one test case.Its requirements express the existence of an input x for which the neuron’s activation predicate is true.
  • Sign-Sign Coverage: Sign-Sign Coverage tests whether a condition neuron independently changes the sign of an adjacent decision neuron while other condition signs remain fixed.The criterion extends MC/DC-style reasoning from existence of features to effects of simpler features on more complex features.
  • Neuron Boundary Coverage: Neuron Boundary Coverage targets neuron activation values that exceed specified upper or lower bounds.The requirements use per-neuron upper bounds hk,i and lower bounds lk,i.

6 Overview of our Approach

The approach alternates concrete evaluation and symbolic analysis to incrementally expand a test suite for a specified set of DNN coverage requirements. It stops when requirements are all satisfied or no further requirement can be satisfied, then evaluates robustness.

  • Algorithm Overview: The method alternates concrete activation-pattern evaluation with symbolic generation of new inputs.It selects a promising unsatisfied requirement and existing input, generates a candidate input symbolically, validates it, and adds it when valid.
  • Algorithm Overview: Algorithm 1 takes a DNN, an initial input t0, heuristic δ, and coverage requirements R, returning a test suite T.The suite initially contains t0, and satisfied requirements are removed from R.
  • Termination: Requirement generation repeats until all requirements are satisfied or the remaining requirements cannot be satisfied.The algorithm terminates when R is empty or the failed-requirement set F equals R.
  • Robustness Evaluation: The generated test suite is passed to a robustness oracle that searches for adversarial examples.The oracle identifies close pairs of test cases that receive different classification labels under a chosen distance metric.
  • Algorithm Overview: For requirements involving two inputs, the algorithm can return two inputs rather than one.The paper states that the single-input description generalizes straightforwardly to the two-input case.

7 Ranking Coverage Requirements

The ranking stage uses concrete executions to choose an existing test and unsatisfied requirement that most promisingly supports symbolic generation. Heuristics optimize requirement-specific objectives, including Lipschitz violation, neuron activation, sign change, and boundary proximity.

  • Ranking Strategy: Concrete executions transform each unsatisfied requirement r into an optimization objective δ(r), then select the most promising input-requirement pair.The transformation uses arg max or arg min operators evaluated over the current test suite.
  • Optimization Semantics: arg min selects a test satisfying the Boolean condition with the smallest arithmetic objective, while arg max uses the corresponding largest value.The semantics extend to pairs of inputs and to continuous input subspaces.
  • Heuristic Design: The ranking transformations are heuristics, and the paper notes that alternative choices exist even though these definitions worked in its experiments.Thus, δ is a design choice rather than a uniquely determined requirement-ranking procedure.
  • Lipschitz Ranking: For an unsatisfied Lipschitz requirement, ranking maximizes ||v[t1]1−v[t2]1||−c·||t1−t2|| over existing test pairs.The selected pair is intended to make the proposed Lipschitz bound fail as strongly as possible.
  • Neuron Ranking: For neuron-activation requirements, ranking selects the existing test with maximal ck·uk,i[x].The layer coefficient ck normalizes differences in activation magnitudes across layers.
  • Sign-Sign Ranking: For Sign-Sign Coverage, ranking selects a condition neuron whose sign is closest to changing while other condition signs remain unchanged.The objective targets the smallest absolute activation magnitude for the selected condition neuron.
  • Boundary Ranking: For boundary requirements, ranking selects a neuron closest to either its upper or lower activation boundary.The corresponding objectives maximize the distance toward the relevant upper or lower bound after applying the layer factor.

8 Symbolic Generation of New Concrete Inputs

The approach generates new concrete inputs by encoding DNN activation patterns as linear constraints or optimization objectives, then solving for inputs satisfying coverage requirements. Linear programming preserves selected ReLU behavior and minimizes input distance when the metric is linear.

  • Approach: Symbolic analysis finds a new input t′ from a concrete input t and coverage requirement r, adding t′ to the test suite.The approach considers linear programming, global optimization, and a new optimization algorithm.
  • Linear Programming: A DNN input’s activation pattern is encoded with linear constraints that represent neuron activations and ReLU activation or deactivation.Constraint (20) encodes neuron activation, while (21) encodes each ReLU’s state for the given pattern.
  • Linear Programming: The LP model represents inputs sharing an activation pattern, so symbolic analysis searches for a new activation pattern and extracts a feasible test input.An objective minimizes the distance between t and t′ to keep the generated test case meaningful.
  • Distance Metrics: LP-based generation requires a linear distance metric, such as L∞, but does not apply directly to L2.The paper also discusses norm-based and structural similarity metrics as configurable distance choices.
  • Coverage Requirements: For neuron coverage, the method negates the target neuron’s activation sign while preserving preceding neurons’ signs and ignoring irrelevant neurons.If the resulting activation pattern is feasible, the extracted input satisfies the neuron requirement.
  • Coverage Requirements: For SS Coverage, both specified neuron signs are negated; for Neuron Boundary Coverage, the target activation is pushed beyond its higher or lower bound.Global optimization can encode these requirements directly as objectives for generating t′.

8.3 Lipschitz Test Case Generation

Lipschitz test cases are generated by alternating compass-search optimizations within norm balls or hypercubes. The method seeks pairs whose estimated Lipschitz constant exceeds a threshold, returning the best pair found if refutation fails.

  • Problem Formulation: The method generates two inputs within a norm ball or hypercube around representative point t0, using a radius or size parameter ∆.The two inputs are optimized under norm metrics such as L0, L2, or L∞.
  • Optimization: An alternating compass-search scheme solves relaxed optimization problems to maximize a lower bound of the Lipschitz constant.The original nonlinear proportional optimization is reformulated linearly when both metrics are L∞.
  • Stage One: Minimizing F(t1,t0) increases the Lipschitz constant because −F(t1,t0)/∆ lower-bounds Lip(t1,t0).The objective searches for t1 maximizing the output-distance term within the allowed input region.
  • Search Procedure: Compass search checks each candidate pair against threshold c and returns it when Lip exceeds c; otherwise, optimization continues.The search is derivative-free and designed for first-order global convergence.
  • Search Procedure: If the search converges without refuting c, the method returns the best pair found and its largest observed Lipschitz constant, which is smaller than c.The returned pair is therefore the strongest result obtained without satisfying the refutation requirement.
  • Overall Scheme: The overall procedure repeatedly shifts the search origin to the best concrete input found to gradually cover the norm-ball space.This alternates symbolic execution with concrete optimization trajectories.

9 Test Oracle

The test oracle first checks validity against inputs assumed to have correct classifications, then evaluates robustness by comparing nearby classified cases. A failing test provides evidence that the DNN lacks robustness.

  • Validity Checking: The paper validates generated inputs against a reference set O of inputs assumed to have correct classifications.A valid test input is close to at least one classified reference input under the selected distance criterion.
  • Robustness Oracle: The robustness oracle evaluates a test suite using a set O of classified inputs and identifies whether generated cases satisfy the robustness criterion.The oracle operates after validity checking and test generation.
  • Robustness Oracle: A test input that fails the robustness oracle serves as evidence that the DNN lacks robustness.Such failures correspond to adversarial examples under the paper’s robustness framing.

10 Experimental Results

Experiments compare DeepConcolic with existing testing approaches across structural, adversarial-example, and Lipschitz-coverage requirements. DeepConcolic generally achieves broad or high coverage and finds adversarial examples, while some costs and limitations remain.

  • Comparison with DeepXplore: DeepConcolic yields much higher neuron coverage than DeepXplore across its light, occlusion, and blackout modes, although DeepXplore is faster.The comparison uses DNNs trained on MNIST and CIFAR-10.
  • Comparison with DeepXplore: DeepConcolic generates adversarial images under L∞- and L0-based testing that resemble human perception without DeepXplore’s domain-specific image constraints.For MNIST, examples gradually reverse black and white colours; for CIFAR-10, L0 examples resemble DeepXplore’s blackout examples.
  • Results for NC, SSC, and NBC: DeepConcolic achieves high coverage and detects a significant number of adversarial examples across NC, SSC, and NBC experiments.The experiments use a single seed for NC, 1,000 initially sampled images for SSC and NBC, and distance bounds of 0.3 under L∞ and 100 pixels under L0.
  • Results for NC, SSC, and NBC: Coverage of corner-case activation values, represented by NBC, is limited, and SSC with L0-norm is excluded because global-optimisation symbolic analysis has too much overhead.The exclusion is reported for the SSC result with L0-norm.
  • Results for NC, SSC, and NBC: Adversarial examples reach the minimum possible distance: 1/255 ≈0.0039 for L∞ and 1 pixel for L0.The reported average-distance analysis also shows that NC’s adversarial-example counts can vary substantially when the distance metric changes.
  • Lipschitz Constant Testing: For image-1 on MNIST, random testing reaches a maximum Lipschitz coverage of 3.23, whereas concolic testing covers [0.01, 10.38].Most concolic cases lie in [3.5, 10], a range poorly covered by random testing; the comparison also reports significant outperformance on MNIST and CIFAR-10.

11 Conclusions

The paper proposes the first concolic testing method for DNNs and evaluates it for coverage-guided test generation, robustness assessment, and adversarial-example discovery.

  • The method is implemented in a software tool and applied to evaluate the robustness of well-known DNNs.
  • Test-input generation can be guided by diverse coverage metrics, including Lipschitz continuity.
  • Combining concrete execution with symbolic analysis delivers coverage and automates adversarial-example discovery.
Loading 1805.00089v2…