pith. sign in

arxiv: 1906.10395 · v1 · pith:VBTHNQ7Mnew · submitted 2019-06-25 · 💻 cs.CR · cs.AI· cs.LG· cs.LO

Quantitative Verification of Neural Networks And its Security Applications

Teodora Baluta , Shiqi Shen , Shweta Shinde , Kuldeep S. Meel , Prateek Saxena This is my paper

Pith reviewed 2026-05-25 16:45 UTC · model grok-4.3

classification 💻 cs.CR cs.AIcs.LGcs.LO
keywords neural networksquantitative verificationPAC guaranteesbinarized networksadversarial robustnesstrojan attacksfairness
0
0 comments X

The pith

A sampling-based framework delivers bounded-error estimates of how many inputs satisfy logical properties in neural networks.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a method to count the inputs that meet a specified property in a neural network, rather than just checking if any do. This quantitative approach is needed because network training is stochastic and security questions often require knowing the proportion or number of satisfying cases. The framework provides PAC-style guarantees that the estimate is close to the true count within a user-specified error bound. It is realized in a tool for binarized networks and demonstrated on three security tasks.

Core claim

The framework is the first to offer PAC-style soundness guarantees for quantitative verification, meaning its estimates of the number of inputs satisfying a property are within a controllable and bounded error from the true count, achieved through an efficient sampling procedure when the network is binarized.

What carries the argument

NPAQ, a prototype tool that encodes the property as a logical formula and uses sampling to produce PAC-bounded quantitative estimates for binarized neural networks.

If this is right

  • Quantifies the robustness of a network to adversarial inputs by counting violating cases.
  • Measures the efficacy of trojan attacks by estimating how many inputs trigger the backdoor.
  • Assesses fairness and bias by counting inputs that lead to discriminatory outputs.
  • Supports richer probabilistic reasoning about neural network behavior beyond binary checks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar sampling techniques might be adapted for continuous-valued networks with discretization.
  • The approach could inspire quantitative verification in other machine learning models like decision trees.
  • Security certifications might one day require such counts instead of existential checks alone.

Load-bearing premise

The estimates rely on the network being binarized so that the property check can be efficiently sampled with bounded error via PAC learning.

What would settle it

Finding a binarized network and property where repeated sampling produces an estimate outside the claimed error bound at the stated confidence level.

Figures

Figures reproduced from arXiv: 1906.10395 by Kuldeep S. Meel, Prateek Saxena, Shiqi Shen, Shweta Shinde, Teodora Baluta.

Figure 1
Figure 1. Figure 1: Example of encoding different BNNs (f , f1, f2) as a conjunction over a set of cardinality constraints. An attacker manipulates f with the goal to increase the inputs with trigger x3 = 1 that classify as y = 0. Specifically, to obtain f1 the weights of x1, x2, x3 in constraints of f for v2,v3,v4 are set to 0 (highlighted with dashed lines, on the left). To obtain f2, we set w21 = 0. The trojan property P … view at source ↗
Figure 2
Figure 2. Figure 2: Cardinality networks encoding for x1 + x3 ≥ 2. For this case, cardinality networks amount to a 2-comparator gate. Observe there are two satisfying assignments for 2-Comp ∧y2 due to the “don’t care" assignment to y1. Running Example. Revisiting our example in Section 5.1, con￾sider f2’s cardinality constraint corresponding to v1, denoted as S ′ 1 = x1 + x3 ≥ 2. This constraint translates to the most basic g… view at source ↗
Figure 3
Figure 3. Figure 3: Number of formulae NPAQ solves with respect to the time. The solid line represents the aggregate number of formulaeNPAQ solves before the given time. The dashed line represents the total number of formulae. 0-6 6-12 12-18 18-24 0 20 40 60 80 100 Time (hour) % of formulae PS ≤ 10% 10% <PS ≤ 50% PS > 50% [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: PS with respect to the time taken by NPAQ. The size of each region represents the fraction of formulae NPAQ solves within the specific time for each range of PS. of the formulae within 24 hours for these two applications. In ro￾bustness application, the total input sizes are a maximum of about 7.5 × 107 . Result 1: NPAQ solves 97.1% formulae in 24-hour timeout. Encoding Efficiency. NPAQ takes a maximum of … view at source ↗
Figure 5
Figure 5. Figure 5: Disjunction gadget: Perceptron equivalent to an [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Conjunction gadget: Perceptron equivalent to an [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper proposes a framework for quantitative verification of logical properties over neural networks. It claims to be the first to provide PAC-style soundness guarantees, meaning quantitative estimates are within a controllable bounded error from the true count. The framework is instantiated as the NPAQ prototype tool for binarized neural networks and demonstrated on three security applications: quantifying robustness to adversarial inputs, efficacy of trojan attacks, and fairness/bias of neural networks.

Significance. If the claimed reduction to an efficient sampling procedure over binarized networks with PAC-bounded error holds, the work would enable probabilistic and quantitative reasoning in NN verification, which is valuable for security analyses where counting satisfying inputs matters. The grounding in standard statistical learning theory for the bounds is a potential strength.

major comments (1)
  1. [Abstract / Framework description] The central claim rests on the existence of an efficient sampling procedure whose output count is within a PAC-bounded error of the true measure after reducing the NN property to a logical formula over a binarized network. The abstract asserts this is achieved in NPAQ, but no derivation of the PAC bounds, error analysis, or explicit sampling procedure is visible; the manuscript must show the concrete reduction and bound application in the relevant technical section.
minor comments (1)
  1. Clarify the precise form of the PAC guarantee (additive vs. multiplicative error, dependence on network size or formula complexity) to make the soundness claim easier to evaluate.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review and constructive feedback on our manuscript. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract / Framework description] The central claim rests on the existence of an efficient sampling procedure whose output count is within a PAC-bounded error of the true measure after reducing the NN property to a logical formula over a binarized network. The abstract asserts this is achieved in NPAQ, but no derivation of the PAC bounds, error analysis, or explicit sampling procedure is visible; the manuscript must show the concrete reduction and bound application in the relevant technical section.

    Authors: We agree that the central technical elements require more explicit presentation. Sections 3 and 4 describe the property reduction to a logical formula over the binarized network and invoke the PAC sampling procedure, but we will revise the manuscript to add a dedicated subsection that derives the PAC bounds from statistical learning theory, provides the error analysis, and includes pseudocode for the sampling procedure. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's central claim of PAC-style soundness guarantees rests on applying standard statistical learning theory to bound sampling error for properties encoded over binarized networks. This is an external result from PAC learning, not derived from or equivalent to the paper's own fitted parameters, definitions, or self-citations. No load-bearing step reduces by construction to its inputs; the framework is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review; no free parameters, invented entities, or non-standard axioms are described. The central claim rests on the applicability of PAC bounds to the sampling procedure for neural-network property counting.

axioms (1)
  • domain assumption PAC learning bounds apply to the sampling procedure used for counting satisfying inputs to logical properties over binarized neural networks
    The soundness guarantees are stated to be PAC-style, which presupposes that the standard PAC framework can be instantiated here.

pith-pipeline@v0.9.0 · 5728 in / 1081 out tokens · 28920 ms · 2026-05-25T16:45:49.199901+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

108 extracted references · 108 canonical work pages

  1. [1]

    Correctional Offender Management Profiling for Alternative Sanctions

    2012. Correctional Offender Management Profiling for Alternative Sanctions. http://www.northpointeinc.com/files/downloads/FAQ_Document.pdf. (2012)

    work page 2012

  2. [2]

    UCI Machine Learning Repository

    2017. UCI Machine Learning Repository. http://archive.ics.uci.edu/ml. (2017)

    work page 2017

  3. [3]

    BDDs for pseudo-Boolean constraints–revisited

    Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez- Carbonell. BDDs for pseudo-Boolean constraints–revisited. In SAT’11

    work page

  4. [4]

    A parametric approach for smaller and better encodings of cardinality constraints

    Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez- Carbonell. A parametric approach for smaller and better encodings of cardinality constraints. In CP’13

    work page

  5. [5]

    On the solution-space geome- try of random constraint satisfaction problems

    Dimitris Achlioptas and Federico Ricci-Tersenghi. On the solution-space geome- try of random constraint satisfaction problems. In STOC’06

    work page

  6. [6]

    Theodoropoulos

    Dimitris Achlioptas and P. Theodoropoulos. Probabilistic Model Counting with Short XORs. In SAT’17

    work page

  7. [7]

    FairSquare: probabilistic verification of program fairness

    Aws Albarghouthi, Loris D’Antoni, Samuel Drews, and Aditya V Nori. FairSquare: probabilistic verification of program fairness. In OOPSLA’17

    work page

  8. [8]

    Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez- Carbonell. 2011. Cardinality networks: a theoretical and empirical study. Con- straints (2011)

    work page 2011

  9. [9]

    Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples

    Anish Athalye, Nicholas Carlini, and David Wagner. Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples. In ICML’18

    work page

  10. [10]

    #∃ SAT: Projected Model Counting

    Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. #∃ SAT: Projected Model Counting. In SAT’15

    work page

  11. [11]

    Neural machine translation by jointly learning to align and translate

    Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural machine translation by jointly learning to align and translate. In ICLR’15. 5https://www.nscc.sg/

    work page

  12. [12]

    Sorting networks and their applications

    Kenneth E Batcher. Sorting networks and their applications. In AFIPS’1968

    work page 1968

  13. [13]

    Certification considerations for adaptive systems

    Siddhartha Bhattacharyya, Darren Cofer, D Musliner, Joseph Mueller, and Eric Engstrom. Certification considerations for adaptive systems. In ICUAS’15

    work page

  14. [14]

    Poisoning attacks against support vector machines

    Battista Biggio, Blaine Nelson, and Pavel Laskov. Poisoning attacks against support vector machines. In ICML’12

    work page

  15. [15]

    An effective decision procedure for linear arithmetic over the integers and reals

    Bernard Boigelot, Sébastien Jodogne, and Pierre Wolper. An effective decision procedure for linear arithmetic over the integers and reals. In TOCL’05

    work page

  16. [16]

    Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, and Others. 2016. End to end learning for self-driving cars. arXiv (2016)

    work page 2016

  17. [17]

    Nicholas Carlini, Chang Liu, Jernej Kos, Úlfar Erlingsson, and Dawn Song. 2018. The Secret Sharer: Measuring Unintended Neural Network Memorization & Extracting Secrets. arXiv (2018)

    work page 2018

  18. [18]

    Hidden Voice Commands

    Nicholas Carlini, Pratyush Mishra, Tavish Vaidya, Yuankai Zhang, Micah Sherr, Clay Shields, David Wagner, and Wenchao Zhou. Hidden Voice Commands.. In USENIX’16

    work page

  19. [19]

    Towards Evaluating the Robustness of Neural Networks

    Nicholas Carlini and David Wagner. Towards Evaluating the Robustness of Neural Networks. In SP’17

    work page

  20. [20]

    From Weighted to Unweighted Model Counting

    Supratik Chakraborty, Dror Fried, Kuldeep S Meel, and Moshe Y Vardi. From Weighted to Unweighted Model Counting.. In IJCAI’15

    work page

  21. [21]

    A scalable approxi- mate model counter

    Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. A scalable approxi- mate model counter. In CP’13

    work page

  22. [22]

    Algorithmic im- provements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls

    Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. Algorithmic im- provements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. In IJCAI’16

    work page

  23. [23]

    Balancing scalability and uniformity in SAT witness generator

    Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. Balancing scalability and uniformity in SAT witness generator. In DAC’14

    work page

  24. [24]

    Use privacy in data-driven systems: Theory and experiments with machine learnt programs

    Anupam Datta, Matthew Fredrikson, Gihyuk Ko, Piotr Mardziel, and Shayak Sen. Use privacy in data-driven systems: Theory and experiments with machine learnt programs. In CCS’17

    work page

  25. [25]

    Algorithmic transparency via quanti- tative input influence: Theory and experiments with learning systems

    Anupam Datta, Shayak Sen, and Yair Zick. Algorithmic transparency via quanti- tative input influence: Theory and experiments with learning systems. In SP’16

    work page

  26. [26]

    Elvis Dohmatob. 2018. Limitations of adversarial robustness: strong No Free Lunch Theorem. arXiv (2018)

    work page 2018

  27. [27]

    Dudek, Kuldeep S

    Jeffrey M. Dudek, Kuldeep S. Meel, and Moshe Y. Vardi. Combining the k-CNF and XOR phase-transitions. In IJCAI’16

    work page

  28. [28]

    Dudek, Kuldeep S

    Jeffrey M. Dudek, Kuldeep S. Meel, and Moshe Y. Vardi. The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas. In IJCAI’17

    work page

  29. [29]

    Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. 2018. A Dual Approach to Scalable Verification of Deep Net- works. arXiv (2018)

    work page 2018

  30. [30]

    Fairness through awareness

    Cynthia Dwork, Moritz Hardt, Toniann Pitassi, Omer Reingold, and Richard Zemel. Fairness through awareness. In ITCS’12

    work page

  31. [31]

    Niklas Eén and Niklas Sörensson. 2006. Translating Pseudo-Boolean Constraints into SAT. JSAT 2, 1-4 (2006), 1–26

    work page 2006

  32. [32]

    Formal verification of piece-wise linear feed-forward neural networks

    Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In ATV A’17

    work page

  33. [33]

    Embed and project: Discrete sampling with universal hashing

    Stefano Ermon, Carla P Gomes, Ashish Sabharwal, and Bart Selman. Embed and project: Discrete sampling with universal hashing. In NIPS’13

    work page

  34. [34]

    Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization

    Stefano Ermon, Carla P Gomes, Ashish Sabharwal, and Bart Selman. Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization. In ICML’13

    work page

  35. [35]

    Stefano Ermon, Carla P Gomes, Ashish Sabharwal, and Bart Selman. 2013. Op- timization with parity constraints: From binary codes to discrete integration. arXiv (2013)

    work page 2013

  36. [36]

    Robust physical-world attacks on deep learning models

    Ivan Evtimov, Kevin Eykholt, Earlence Fernandes, Tadayoshi Kohno, Bo Li, Atul Prakash, Amir Rahmati, and Dawn Song. Robust physical-world attacks on deep learning models. In CVPR’18

    work page

  37. [37]

    Certifying and removing disparate impact

    Michael Feldman, Sorelle A Friedler, John Moeller, Carlos Scheidegger, and Suresh Venkatasubramanian. Certifying and removing disparate impact. In SIGKDD’15

    work page

  38. [38]

    Nic Ford, Justin Gilmer, Nicolas Carlini, and Dogus Cubuk. 2019. Adversarial Examples Are a Natural Consequence of Test Error in Noise. arXiv (2019)

    work page 2019

  39. [39]

    Model inversion attacks that exploit confidence information and basic countermeasures

    Matt Fredrikson, Somesh Jha, and Thomas Ristenpart. Model inversion attacks that exploit confidence information and basic countermeasures. In CCS’15

    work page

  40. [40]

    Privacy in Pharmacogenetics: An End-to-End Case Study of Personalized Warfarin Dosing

    Matt Fredrikson, Eric Lantz, Somesh Jha, Simon Lin, David Page, and Thomas Ris- tenpart. Privacy in Pharmacogenetics: An End-to-End Case Study of Personalized Warfarin Dosing.. In USENIX’14’

    work page

  41. [41]

    Attacking Binarized Neural Networks

    Angus Galloway, Graham W Taylor, and Medhat Moussa. Attacking Binarized Neural Networks. In ICLR’18

    work page

  42. [42]

    A decision procedure for bit-vectors and arrays

    Vijay Ganesh and David L Dill. A decision procedure for bit-vectors and arrays. In CA V’07

    work page

  43. [43]

    Yansong Gao, Chang Xu, Derui Wang, Shiping Chen, Damith C Ranasinghe, and Surya Nepal. 2019. STRIP: A Defence Against Trojan Attacks on Deep Neural Networks. arXiv (2019)

    work page 2019

  44. [44]

    AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation

    Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In SP’18

    work page

  45. [45]

    Arturo Geigel. 2013. Neural network trojan. Journal of Computer Security (2013)

    work page 2013

  46. [46]

    Justin Gilmer, Ryan P Adams, Ian Goodfellow, David Andersen, and George E Dahl. 2018. Motivating the rules of the game for adversarial example research. arXiv (2018)

    work page 2018

  47. [47]

    Justin Gilmer, Luke Metz, Fartash Faghri, Samuel S Schoenholz, Maithra Raghu, Martin Wattenberg, and Ian Goodfellow. 2018. Adversarial spheres.arXiv (2018)

    work page 2018

  48. [48]

    Ciresan, Fang-Lin He, Juan P

    Alessandro Giusti, Jerome Guzzi, Dan C. Ciresan, Fang-Lin He, Juan P. Rodriguez, Flavio Fontana, Matthias Faessler, Christian Forster, Jurgen Schmidhuber, Gi- anni Di Caro, Davide Scaramuzza, and Luca M. Gambardella. 2016. A Machine Learning Approach to Visual Perception of Forest Trails for Mobile Robots. IEEE Robotics and Automation Letters (2016)

    work page 2016

  49. [49]

    Gomes, Ashish Sabharwal, and Bart Selman

    Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting: A new strategy for obtaining good bounds. In AAAI’06

    work page

  50. [50]

    Explaining and Har- nessing Adversarial Examples

    Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and Har- nessing Adversarial Examples. In ICLR’15

    work page

  51. [51]

    Monte carlo model checking

    Radu Grosu and Scott A Smolka. Monte carlo model checking. In TACAS’05

    work page

  52. [52]

    Equality of opportunity in supervised learning

    Moritz Hardt, Eric Price, Nati Srebro, et al. Equality of opportunity in supervised learning. In NIPS’16

    work page

  53. [53]

    W Keith Hastings. 1970. Monte Carlo sampling methods using Markov chains and their applications. (1970)

    work page 1970

  54. [54]

    Deep residual learning for image recognition

    Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Deep residual learning for image recognition. In CVPR’16

    work page

  55. [55]

    Sound Abstraction and Decom- position of Probabilistic Programs

    Steven Holtzen, Guy Broeck, and Todd Millstein. Sound Abstraction and Decom- position of Probabilistic Programs. In ICML’18

    work page

  56. [56]

    Safety Verification of Deep Neural Networks

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety Verification of Deep Neural Networks. In CA V’17

    work page

  57. [57]

    Binarized neural networks

    Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El-Yaniv, and Yoshua Bengio. Binarized neural networks. In NIPS’16

    work page

  58. [58]

    Jerrum and Alistair Sinclair

    Mark R. Jerrum and Alistair Sinclair. 1996. The Markov chain Monte Carlo method: an approach to approximate counting and integration. Approximation algorithms for NP-hard problems (1996), 482–520

    work page 1996

  59. [59]

    Policy compression for aircraft collision avoidance systems

    Kyle D Julian, Jessica Lopez, Jeffrey S Brush, Michael P Owen, and Mykel J Kochenderfer. Policy compression for aircraft collision avoidance systems. In DASC’16

    work page

  60. [60]

    Reluplex: An efficient SMT solver for verifying deep neural networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. InCA V’17

    work page

  61. [61]

    Understanding black-box predictions via influ- ence functions

    Pang Wei Koh and Percy Liang. Understanding black-box predictions via influ- ence functions. In ICML’17

    work page

  62. [62]

    A decision procedure for the propositional µ-calculus

    Dexter Kozen and Rohit Parikh. A decision procedure for the propositional µ-calculus. In WLP’1983

    work page 1983

  63. [63]

    Imagenet classification with deep convolutional neural networks

    Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton. Imagenet classification with deep convolutional neural networks. In NIPS’12

    work page

  64. [64]

    Jaeha Kung, David Zhang, Gooitzen van der Wal, Sek Chai, and Saibal Mukhopad- hyay. 2018. Efficient object detection using embedded binarized neural networks. Journal of Signal Processing Systems (2018)

    work page 2018

  65. [65]

    Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. 2015. Deep learning. nature (2015)

    work page 2015

  66. [66]

    Yann LeCun and Corinna Cortes. 2010. MNIST handwritten digit database. (2010)

    work page 2010

  67. [67]

    Defense against adversarial attacks using high-level representation guided denoiser

    Fangzhou Liao, Ming Liang, Yinpeng Dong, Tianyu Pang, Xiaolin Hu, and Jun Zhu. Defense against adversarial attacks using high-level representation guided denoiser. In CVPR’18

    work page

  68. [68]

    Trojaning Attack on Neural Networks

    Yingqi Liu, Shiqing Ma, Yousra Aafer, Wen-Chuan Lee, Juan Zhai, Weihang Wang, and Xiangyu Zhang. Trojaning Attack on Neural Networks. In NDSS’18

    work page

  69. [69]

    Saeed Mahloujifar, Dimitrios I Diochnos, and Mohammad Mahmoody. 2018. The curse of concentration in robust learning: Evasion and poisoning attacks from concentration of measure. arXiv (2018)

    work page 2018

  70. [70]

    Embedded Binarized Neural Networks

    Bradley McDanel, Surat Teerapittayanon, and H T Kung. Embedded Binarized Neural Networks. In EWSN’17

    work page

  71. [71]

    Kuldeep S. Meel. 2017. Constrained Counting and Sampling: Bridging the Gap between Theory and Practice . Ph.D. Dissertation. Rice University

    work page 2017

  72. [72]

    Meel, Moshe Y

    Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J Fremont, Sanjit A Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik. Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. In AAAI’16 (Beyond NP Workshop)

    work page

  73. [73]

    Verifying properties of binarized deep neural networks

    Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. In AAAI’18

    work page

  74. [74]

    Radford M Neal. 1993. Probabilistic inference using Markov chain Monte Carlo methods. (1993)

    work page 1993

  75. [75]

    Robert Nieuwenhuis and Albert Oliveras. 2005. Decision procedures for SAT, SAT modulo theories and beyond. the BarcelogicTools. In International Conference on Logic for Programming Artificial Intelligence and Reasoning . Springer, 23–46

    work page 2005

  76. [76]

    Nicolas Papernot, Patrick McDaniel, and Ian Goodfellow. 2016. Transferability in Machine Learning: from Phenomena to Black-Box Attacks using Adversarial Samples. arXiv (2016)

    work page 2016

  77. [77]

    The limitations of deep learning in adversarial settings

    Nicolas Papernot, Patrick McDaniel, Somesh Jha, Matt Fredrikson, Z Berkay Celik, and Ananthram Swami. The limitations of deep learning in adversarial settings. In EuroS&P’16

    work page

  78. [78]

    Distillation as a defense to adversarial perturbations against deep neural net- works

    Nicolas Papernot, Patrick McDaniel, Xi Wu, Somesh Jha, and Ananthram Swami. Distillation as a defense to adversarial perturbations against deep neural net- works. In SP’16

    work page

  79. [79]

    Automatic differentiation in PyTorch

    Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in PyTorch. InNIPS-W’17

    work page

  80. [80]

    Deepxplore: Automated whitebox testing of deep learning systems

    Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. Deepxplore: Automated whitebox testing of deep learning systems. In SOSP’17

    work page

Showing first 80 references.