PaperlayerView exact revision on arXiv

Source-linked AI summary

Quantitative Verification of Neural Networks And its Security Applications

Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, Prateek Saxena

arXiv:1906.10395v1cs.CRcs.AIcs.LGcs.LO

TL;DR

Existential checks do not answer how often a neural-network property holds, although many analyses require counts. The paper introduces a PAC-guaranteed quantitative verification framework, instantiates it in NPAQ for BNNs, and applies it to robustness, trojan attacks, and fairness.

  • Problem

    Prior verification work largely checks whether a violating input exists, while many neural-network analyses require estimating how often a property holds.

    Source: §1 · p. 1

  • Method

    The framework encodes neural networks and properties as CNF using equi-witnessability, then applies approximate model counting to estimate property counts with PAC-style guarantees.

    Source: §1 · p. 2, §8 · p. 13

  • Results

    NPAQ was evaluated on 1,056 formulae and shown to scale to BNNs with over 50,000 parameters, while the framework demonstrates applications in robustness, trojan attacks, and fairness.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The framework supports quantitative analyses of adversarial inputs, trojan effectiveness, and fairness-related prediction changes in BNNs.

    Source: §3 · p. 3, §8 · p. 13

    The probability interpretation assumes a uniform distribution over inputs; weighted counting for user-defined distributions is left for future work.

    Source: §2 · p. 3

Abstract

from arXiv · show

Neural networks are increasingly employed in safety-critical domains. This has prompted interest in verifying or certifying logically encoded properties of neural networks. Prior work has largely focused on checking existential properties, wherein the goal is to check whether there exists any input that violates a given property of interest. However, neural network training is a stochastic process, and many questions arising in their analysis require probabilistic and quantitative reasoning, i.e., estimating how many inputs satisfy a given property. To this end, our paper proposes a novel and principled framework to quantitative verification of logical properties specified over neural networks. Our framework is the first to provide PAC-style soundness guarantees, in that its quantitative estimates are within a controllable and bounded error from the true count. We instantiate our algorithmic framework by building a prototype tool called NPAQ that enables checking rich properties over binarized neural networks. We show how emerging security analyses can utilize our framework in 3 concrete point applications: quantifying robustness to adversarial inputs, efficacy of trojan attacks, and fairness/bias of given neural networks.

1 INTRODUCTION

The introduction argues that existential verification cannot answer how often a neural-network property holds, a question needed for statistical analyses. It presents a PAC-guaranteed counting framework, instantiated as NPAQ for binarized neural networks, with security applications.

Motivation

  • Existential verification asks whether any input violates a property, while many analyses need to know how often a property holds.Because neural networks are stochastically trained, the existence of satisfying inputs alone may not establish that their counts are statistically significant.Source: §1 · p. 1

Our Approach

  • The framework estimates property counts with PAC-style guarantees: its estimate is within a multiplicative (1 + ε) factor of the true count with confidence at least 1 − δ.The user chooses the tolerance ε and confidence parameter δ.Source: §1 · p. 2
  • The approach encodes networks and properties as CNF formulae using equi-witnessability, then estimates counts of satisfying assignments projected onto part of the formula’s support.Approximate model counting supplies the stated soundness and precision guarantees.Source: §1 · p. 2

Results

  • 97.1% of 1,056 formulae were solved within 24 hours; NPAQ was evaluated on models with up to 51,410 parameters.The evaluation covered BNNs trained on MNIST and UCI Adult Census Income.Source: §1 · p. 2

Contributions

  • NPAQ instantiates the framework for BNNs and supports quantitative analyses of robustness, trojan attacks, and fairness.The paper presents these as security applications of its general framework.Source: §1 · pp. 1–2

2 PROBLEM DEFINITION

The problem is to count or estimate the assignments satisfying a logical specification of network behavior and a property. Exact counting is #P-hard for specifications over BNNs, motivating approximate estimates with probabilistic guarantees.

Specification

  • A specification φ combines network behavior with a property over inputs and outputs; its satisfying assignments form R(φ).The paper illustrates a property comparing the outputs of two networks on the same input.Source: §2 · p. 2

Neural Quantitative Verification

  • Quantitative verification returns the number of satisfying assignments, |R(φ)|, rather than only whether one exists.The paper notes that naïve enumeration can be intractable for large input spaces.Source: §2 · p. 2

Complexity

  • NQV is #P-hard for specifications over binarized neural networks.The proof reduces CNF model counting parsimoniously to quantitative verification of BNNs.Source: §2 · p. 2

Approximate NQV

  • An approximate verifier estimates the count within a multiplicative (1 + ε) factor with probability at least 1 − δ.The user chooses the precision and confidence parameters.Source: §2 · p. 3

Connection to probabilities

  • The probability interpretation assumes uniformly weighted input values; weighted counting for user-defined distributions is left as future work.Under the uniform assumption, |R(φ)| divided by 2^|x| is the event probability.Source: §2 · p. 3

3 SECURITY APPLICATIONS

The paper describes quantitative specifications for robustness, trojan attacks, and fairness. These count relevant inputs or paired inputs, enabling comparisons that existence checks alone do not provide.

Robustness

  • Robustness specifications count inputs misclassified within a chosen perturbation distance of a benign sample.The number of adversarial samples increases monotonically as the permitted perturbation grows; NPAQ can compare models and evaluate defenses.Source: §3 · p. 3
  • NPAQ avoids enumerating a potentially too-large perturbation neighborhood when estimating adversarial-input counts.The paper also reports that its two adversarial-training defenses showed lesser robustness than the plain model.Source: §3 · p. 3

Trojan Attacks

  • Trojan analysis counts trigger-bearing inputs classified as the attack’s target label, and test-set attack accuracy can differ significantly from the count over all specified trojan inputs.The evaluation concerns BNNs trained on MNIST.Source: §3 · p. 3

Fairness

  • The fairness specification compares predictions for paired inputs that keep non-sensitive features equal while changing a sensitive feature.A high count of unchanged predictions indicates that changing only the sensitive feature often leaves the output unchanged.Source: §3 · p. 3
  • Follow-up properties P4 and P5 count paired inputs where changing the sensitive value changes the prediction in opposite directions.The properties separately encode HIGH-to-LOW and LOW-to-HIGH outcomes.Source: §3 · p. 4

4 APPROACH

The approach reduces quantitative neural-network verification to model counting over CNF while preserving the counts of interest through equi-witnessable encodings. Approximate CNF counters then provide sound estimates, including for rare events where random sampling may require intractably many samples.

4 APPROACH

  • Equisatisfiable encodings alone are insufficient for model counting because added variables can create extra satisfying assignments.The paper motivates equi-witnessability as a stronger encoding property for preserving counts.Source: §4 · p. 4
  • Equi-witnessability preserves projected model counts and remains valid under conjunction, allowing encoded network and property constraints to be combined without changing the count.The encoding may introduce variables, so counting assignments projected onto the original variables is essential.Source: §4 · p. 4
  • Approximate CNF counters supply (ε,δ) guarantees after the network and property are encoded as a count-preserving formula.The method composes equi-witnessable encodings and counts over a projected subset of variables.Source: §4 · pp. 4–5
  • Random sampling may require intractably many samples to soundly estimate rare-event counts, which arise in security applications.The framework is intended to work irrespective of the probability of the events being measured.Source: §4 · p. 5

5 NPAQ DESIGN

NPAQ encodes binarized neural networks and properties into count-preserving CNF formulas, then applies projected approximate model counting. Its construction is proved to be an (ε,δ)-NQV procedure.

5 NPAQ DESIGN

  • The tool takes trained BNNs and a property as input and returns how much the property holds with (ε,δ) guarantees.The design encodes the BNN into CNF and uses an approximate counter over projected variables.Source: §5 · p. 5

5.1 BNN to Cardinality Constraints

  • Each BNN block is encoded so the property specification is equi-witnessable to the BNN formula, with intermediate variables uniquely determined by the input.In the trojan example, f1 is equivalent to f despite changed parameters, while f2 changes the prediction for input (0,1,1).Source: §5.1 · p. 6

5.2 Cardinality Constraints to CNF

  • Cardinality networks encode the BNN’s Boolean cardinality constraints as CNF; projected counting avoids overcounting assignments to auxiliary variables.For the example constraint x1 + x3 ≥ 2, counting over {x1,x3} gives the correct count of 1.Source: §5.2 · pp. 6–7
  • The cardinality-network encoding has size linear in the BNN model size under the stated layer and output-block bounds.The passage gives total CNF size O(m × n × l + s × s × n).Source: §5.2 · pp. 7–8

5.3 Projected Model Counting

  • NPAQ counts satisfying assignments over a projected subset of variables using ApproxMC3, which provides PAC-style guarantees.ApproxMC3 makes a logarithmic number of SAT-solver calls in the number of formula variables.Source: §5.3 · p. 8
  • NPAQ is an (ε,δ)-NQV procedure, using equi-witnessable encodings and an approximate model counter with matching guarantees.The guarantee follows from count-preserving encodings of the cardinality constraints and BNN.Source: §5.3 · p. 8

6 IMPLEMENTATION & EVALUATION

The evaluation benchmarks NPAQ on 1,056 formulae and applies it to robustness, trojan-effectiveness, and fairness analyses. NPAQ solves most benchmark formulae within the timeout, while the case studies show how quantitative estimates can expose differences in model behavior.

6.1 NPAQ Benchmarking

  • In a benchmark breakdown covering 1,056 formulae, NPAQ successfully solved 1,025 (97.1%) within the 24-hour timeout, demonstrating its reported estimation efficiency on this evaluation set.Source: §6.1 · pp. 8–9
  • Encoding takes at most 1 minute per model, and formula size scales linearly with model size.Off-the-shelf CNF counters dominate runtime; NPAQ scales to formulae with about 3.5 × 10^6 variables and 6.2 × 10^6 clauses.Source: §6.1 · p. 9
  • NPAQ solves 93.2% of formulae in the first 12 hours and only 3.9% more in the next 12 hours.Most timeouts are associated with ARCH4 (27/31) and robustness property P1 (26/31).Source: §6.1 · p. 9
  • Across 1,056 formulae, satisfying-solution count did not significantly affect solve time; for fairness formulae, ϵ = 0.1 took 16× longer than ϵ = 0.8, with δ fixed at 0.2.For the fairness formulae, reported counts did not differ significantly across ϵ values when δ = 0.2.Source: §6.1 · p. 9

6.2 Case Study 1: Quantifying Robustness

  • Adversarial-input counts increase with perturbation size, and ARCH1 has fewer adversarial samples than ARCH2–ARCH4 for k ≤ 5.For 11/16 models, plain BNNs are more robust than hardened models; the two defenses show no significant difference in the evaluated models.Source: §6.2 · p. 10

6.3 Case Study 2: Quantifying Effectiveness of Trojan Attacks

  • The model with the highest test-set trojan accuracy matches the model with the highest estimated out-of-distribution trojan effectiveness in only 50% of cases.The comparison covers 20 architecture-and-target-class combinations.Source: §6.3 · p. 11

6.4 Case Study 3: Quantifying Model Fairness

  • Changing a sensitive feature while holding other features fixed changes predictions for 19% of possible inputs in the evaluated fairness analysis.The authors report that most evaluated models have a fairness score below 81%.Source: §6.4 · p. 12
  • The direction of predicted-income changes varies by sensitive feature and model, including different gender-related patterns for ARCH1 and ARCH4.For ARCH1, male rather than female inputs are more likely to receive a higher-income prediction; ARCH4 shows the opposite direction.Source: §6.4 · p. 12

7 RELATED WORK

Prior neural-network verification work mostly addresses existential properties or robustness bounds, while quantitative verification counts satisfying inputs. Related quantitative program analyses also differ from NPAQ in their guarantees.

Non-quantitative Neural Network Verification

  • Earlier neural-network verification methods typically seek a violating input or certify ranges, witnesses, or robustness bounds rather than count satisfying inputs.Examples include SMT and SAT methods, abstract interpretation, and optimization-based approaches.Source: §7 · p. 12
  • NPAQ and prior verification methods both encode networks with deterministic constraints, but equi-witnessability is specific to certain constructions and preserves model counts.The related methods described use SAT solving, SMT, abstract interpretation, or optimization for other verification goals.Source: §7 · p. 12

Quantitative Verification of Programs

  • FairSquare computes weighted volumes for fairness but lacks a finite-time desired-error guarantee, while Webb et al. use statistics without provable error bounds.NPAQ is distinguished by PAC-style guarantees on quantitative counts.Source: §7 · p. 12

CNF Model Counting

  • #CNF is #P-complete, and hashing-based approximate model counting has been developed alongside SAT solvers for CNF and XOR constraints [71].The background connects counting complexity to the polynomial hierarchy and approximate counting techniques.Source: §7 · pp. 12–13

8 CONCLUSION

The paper presents a PAC-sound framework for approximate quantitative verification of neural networks. It defines count-preserving, composable CNF encodings, instantiates them for binarized networks in NPAQ, and demonstrates applications in security analyses.

8 CONCLUSION

  • The framework provides formal PAC-style soundness for approximate quantitative verification of neural networks.It defines equi-witnessability encodings into CNF that preserve counts and compose under logical conjunctions.Source: §8 · p. 13
  • The framework is instantiated for binarized neural networks in the prototype tool NPAQ.The conclusion reports its use for properties arising in three concrete security applications.Source: §8 · p. 13
  • The showcased applications use properties arising in three concrete security analyses.The conclusion identifies the applications collectively without naming them individually.Source: §8 · p. 13

10 APPENDIX

The appendix proves a detailed independent-support claim for the BNN encoding and establishes #P-hardness by reducing formula model counting to quantitative verification. Its reduction represents formula gates with perceptrons and preserves satisfying-assignment counts.

10.1 Lemma 5.1 Detailed Proof

  • For the BNN formula, the input variables independently determine the introduced variables, so counting over the formula matches counting projected onto the inputs.The proof argues that the first, internal, and output blocks’ variables are uniquely determined by the input.Source: §10.1 · p. 15

10.2 Quantitative Verification is #P-hard

  • Quantitative verification is #P-hard even for binarized neural networks, by a reduction that preserves the number of models.The result extends to quantitative verification over multilayer perceptrons in general.Source: §10.2 · p. 15
  • The reduction maps propositional variables to binary inputs and represents formula OR and AND gates with perceptrons.For each clause, the disjunction gadget activates when at least one literal is true; the conjunction gadget activates only when all clauses are satisfied.Source: §10.2 · pp. 15–16
  • Each satisfying assignment corresponds to an accepting BNN output, and the reduction to quantitative verification has polynomial size.The specification requires the network output to equal its computed output and be 1.Source: §10.2 · p. 16
Loading 1906.10395v1…