Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network's correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors into account. In this paper, we show that verifying the bit-exact implementation of quantized neural networks with bit-vector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.
Towards Efficient Verification of Quantized Neural Networks
Stanford University（斯坦福大学）；Institute of Computing Technology, Chinese Academy of Sciences（中国科学院计算技术研究所）；IT University of Copenhagen（哥本哈根信息技术大学）；National University of Singapore（新加坡国立大学）
QEBVerif: Quantization Error Bound Verification of Neural Networks
ShanghaiTech University（上海科技大学）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Automotive Software Innovation Center（汽车软件创新中心）；Singapore Management University（新加坡管理大学）
Verification of Bit-Flip Attacks against Quantized Neural Networks
National University of Singapore（新加坡国立大学）；ShanghaiTech University（上海科技大学）；ByteDance Inc（字节跳动公司）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；University of Chinese Academy of Sciences（中国科学院大学）；Nanjing Institute of Software Technology（南京软件技术研究院）；Singapore Management University（新加坡管理大学）
ShanghaiTech University（上海科技大学）；Singapore Management University（新加坡管理大学）；East China Normal University（华东师范大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
Deep learning has become a promising programming paradigm in software development, owing to its surprising performance in solving many challenging tasks. Deep neural networks (DNNs) are increasingly being deployed in practice, but are limited on resource-constrained devices owing to their demand for computational power. Quantization has emerged as a promising technique to reduce the size of DNNs with comparable accuracy as their floating-point numbered counterparts. The resulting quantized neural networks (QNNs) can be implemented energy-efficiently. Similar to their floating-point numbered co…
Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
Gran Sasso Science Institute (GSSI)（格拉斯索科学研究所）；Rheinland-Pfälzische Technische Universität (RPTU)（莱茵-普法尔茨技术大学）；ENS de Lyon, CNRS, Université Claude Bernard Lyon 1, Inria, LIP, UMR 5668（里昂大学（ENS de Lyon）、国家科学研究中心（CNRS）、里昂第一大学（Université Claude Bernard Lyon 1）、法国国家信息与自动化研究所（Inria）、里昂研究院（LIP）、UMR 5668）
Stony Brook University（石溪大学）；University of Nebraska-Lincoln（内布拉斯加大学林肯分校）
ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Due the use of a large lookup table in the design, a neural network compression of the policy was proposed. Analysis of this system has spurred a significant body of research in the formal methods community on neural network verification. While many powerful methods have been developed, most work focuses on open-loop properties of the networks, rather than the main point of the system -- collision avoidance -- which requires closed-loop analys…
Generating Synthetic Satellite Imagery With Deep-Learning Text-to-Image Models -- Technical Challenges and Implications for Monitoring and Verification
Berliner Hochschule für Technik（柏林应用技术大学）；Princeton University（普林斯顿大学）；Einstein Center Digital Future（爱因斯坦数字未来中心）
Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）；Microsoft Research（微软研究院）
Learning program semantics from raw source code is challenging due to the complexity of real-world programming language syntax and due to the difficulty of reconstructing long-distance relational information implicitly represented in programs using identifiers. Addressing the first point, we consider Constrained Horn Clauses (CHCs) as a standard representation of program verification problems, providing a simple and programming language-independent syntax. For the second challenge, we explore graph representations of CHCs, and propose a new Relational Hypergraph Neural Network (R-HyGNN) archit…
Assessing High-Risk AI Systems under the EU AI Act: From Legal Requirements to Technical Verification
Luxembourg Institute of Science and Technology (LIST)（卢森堡科学技术研究院（LIST））；LIST, University of Luxembourg（卢森堡大学LIST）；Research Institutes of Sweden (RISE)（瑞典研究院（RISE））
This technical report aims at defining a formal framework for Deep Neural Network (DNN) layer-wise quantization, focusing in particular on the problems related to the final deployment. It also acts as a documentation for the NEMO (NEural Minimization for pytOrch) framework. It describes the four DNN representations used in NEMO (FullPrecision, FakeQuantized, QuantizedDeployable and IntegerDeployable), focusing in particular on a formal definition of the latter two. An important feature of this model, and in particular the IntegerDeployable representation, is that it enables DNN inference using…
RWTH Aachen University（亚琛工业大学）；UMONS – Université de Mons（蒙斯大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining the Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case can be reduced to the stationary one by a…
