DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.26

DNN Verification, Reachability, and the Exponential Function Problem

Authors: Omri Isac, Yoni Zohar, Clark Barrett, and Guy Katz

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract

Deep neural networks (DNNs) are increasingly being deployed to perform safety-critical tasks. The opacity of DNNs, which prevents humans from reasoning about them, presents new safety and security challenges. To address these challenges, the verification community has begun developing techniques for rigorously analyzing DNNs, with numerous verification algorithms proposed in recent years. While a significant amount of work has gone into developing these verification algorithms, little work has been devoted to rigorously studying the computability and complexity of the underlying theoretical problems. Here, we seek to contribute to the bridging of this gap. We focus on two kinds of DNNs: those that employ piecewise-linear activation functions (e.g., ReLU), and those that employ piecewise-smooth activation functions (e.g., Sigmoids). We prove the two following theorems: (i) the decidability of verifying DNNs with a particular set of piecewise-smooth activation functions, including Sigmoid and tanh, is equivalent to a well-known, open problem formulated by Tarski; and (ii) the DNN verification problem for any quantifier-free linear arithmetic specification can be reduced to the DNN reachability problem, whose approximation is NP-complete. These results answer two fundamental questions about the computability and complexity of DNN verification, and the ways it is affected by the network’s activation functions and error tolerance; and could help guide future efforts in developing DNN verification tools.

Cite as

Omri Isac, Yoni Zohar, Clark Barrett, and Guy Katz. DNN Verification, Reachability, and the Exponential Function Problem. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{isac_et_al:LIPIcs.CONCUR.2023.26,
  author =	{Isac, Omri and Zohar, Yoni and Barrett, Clark and Katz, Guy},
  title =	{{DNN Verification, Reachability, and the Exponential Function Problem}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.26},
  URN =		{urn:nbn:de:0030-drops-190205},
  doi =		{10.4230/LIPIcs.CONCUR.2023.26},
  annote =	{Keywords: Formal Verification, Computability Theory, Deep Neural Networks}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.85

On the Succinctness of Idioms for Concurrent Programming

Authors: David Harel, Guy Katz, Robby Lampert, Assaf Marron, and Gera Weiss

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

The ability to create succinct programs is a central criterion for comparing programming and specification methods. Specifically, approaches to concurrent programming can often be thought of as idioms for the composition of automata, and as such they can then be compared using the standard and natural measure for the complexity of automata, descriptive succinctness. This measure captures the size of the automata that the evaluated approach needs for expressing the languages under discussion. The significance of this metric lies, among other things, in its impact on software reliability, maintainability, reusability and simplicity, and on software analysis and verification. Here, we focus on the succinctness afforded by three basic concurrent programming idioms: requesting events, blocking events and waiting for events. We show that a programming model containing all three idioms is exponentially more succinct than non-parallel automata, and that its succinctness is additive to that of classical nondeterministic and "and" automata. We also show that our model is strictly contained in the model of cooperating automata à la statecharts, but that it may provide similar exponential succinctness over non-parallel automata as the more general model - while affording increased encapsulation. We then investigate the contribution of each of the three idioms to the descriptive succinctness of the model as a whole, and show that they each have their unique succinctness advantages that are not subsumed by their counterparts. Our results contribute to a rigorous basis for assessing the complexity of specifying, developing and maintaining complex concurrent software.

Cite as

David Harel, Guy Katz, Robby Lampert, Assaf Marron, and Gera Weiss. On the Succinctness of Idioms for Concurrent Programming. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 85-99, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{harel_et_al:LIPIcs.CONCUR.2015.85,
  author =	{Harel, David and Katz, Guy and Lampert, Robby and Marron, Assaf and Weiss, Gera},
  title =	{{On the Succinctness of Idioms for Concurrent Programming}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{85--99},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.85},
  URN =		{urn:nbn:de:0030-drops-53849},
  doi =		{10.4230/LIPIcs.CONCUR.2015.85},
  annote =	{Keywords: Descriptive Succinctness, Module Size, Automata, Bounded Concurrency}
}

Search Results

Documents authored by Katz, Guy

DNN Verification, Reachability, and the Exponential Function Problem

Abstract

Cite as

On the Succinctness of Idioms for Concurrent Programming

Abstract

Cite as

Thanks for your feedback!

Could not send message