Approximations play a pivotal role in verifying deep neural networks (DNNs). Existing approaches typically rely on either single-neuron approximations (simpler to design but less precise) or multi-neuron approximations (higher precision but significantly more complex to construct). Between them, a notable gap exists. This work bridges the gap. The idea is to lift single-neuron approximations into multi-neuron approximations with precision gain. To this end, we formulate the approximation transition as a novel problem, named Convex Approximation Lifting (CAL), and propose a constructive approach, Support Triangle Machine (STM), to solving it. STM is grounded in two core insights: (i) there exists a simple geometric structure, called the support triangle, along with an efficient triangle lifting technique that connects single-neuron approximations and multi-neuron approximations; and (ii) typical single-neuron approximations can be easily decomposed into multiple atomically liftable components . Specifically, given a CAL instance, STM constructs a multi-neuron approximation by iteratively processing each output coordinate. For each coordinate, it decomposes the single-neuron approximation into several linear parts, lifts each of them using the triangle lifting technique, and then synthesize an intermediate approximation, which later servers as input for the next iteration. We theoretically prove the correctness of STM and empirically evaluate its performance on a variety of CAL problems and DNN verification tasks. Experimental results demonstrate STM’s broad applicability, improved precision, and sustained efficiency. Beyond DNN verification, STM has the potential to facilitate approximation construction process in more general tasks, and we expect it to catalyze further research in related fields.

Convex hulls are commonly used to tackle the non-linearity of activation functions in the verification of neural networks. Computing the exact convex hull is a costly task though. In this work, we propose a fast and precise approach to over-approximating the convex hull of the ReLU function (referred to as the ReLU hull ), one of the most used activation functions. Our key insight is to formulate a convex polytope that “wraps” the ReLU hull, by reusing the linear pieces of the ReLU function as the lower faces and constructing upper faces that are adjacent to the lower faces. The upper faces can be efficiently constructed based on the edges and vertices of the lower faces, given that an n -dimensional (or simply n d hereafter) hyperplane can be determined by an ( n - 1 ) d hyperplane and a point outside of it. We implement our approach as WraLU , and evaluate its performance in terms of precision, efficiency, constraint complexity, and scalability. WraLU outperforms existing advanced methods by generating fewer constraints to achieve tighter approximation in less time. It exhibits versatility by effectively addressing arbitrary input polytopes and higher-dimensional cases, which are beyond the capabilities of existing methods. We integrate WraLU into PRIMA, a state-of-the-art neural network verifier, and apply it to verify large-scale ReLU-based neural networks. Our experimental results demonstrate that WraLU achieves a high efficiency without compromising precision. It reduces the number of constraints that need to be solved by the linear programming solver by up to half, while delivering comparable or even superior results compared to the state-of-the-art verifiers.

Due to the great advance in machine learning (ML) techniques, numerous ML models are expanding their application domains in recent years. To adapt for resource-constrained platforms such as mobile and Internet of Things (IoT) devices, pre-trained models are often processed to enhance their efficiency and compactness, using optimization techniques such as pruning and quantization. Similar to the optimization process in other complex systems, e.g., program compilers and databases, optimizations for ML models can contain bugs, leading to severe consequences such as system crashes and financial loss. While bugs in training, compiling and deployment stages have been extensively studied, there is still a lack of systematic understanding and characterization of model optimization bugs (MOBs). In this work, we conduct the first empirical study to identify and characterize MOBs. We collect a comprehensive dataset containing 371 MOBs from TensorFlow and PyTorch, the most extensively used open-source ML frameworks, covering the entire development time span of their optimizers (May 2019 to August 2022). We then investigate the collected bugs from various perspectives, including their symptoms, root causes, life cycles, detection and fixes. Our work unveils the status quo of MOBs in the wild, and reveals their features on which future detection techniques can be based. Our findings also serve as a warning to the developers and the users of ML frameworks, and an appeal to our research community to enact dedicated countermeasures.

Recently, several abstraction refinement techniques have been proposed to improve the verification precision for deep neural networks (DNNs). However, these techniques usually take many refinement steps to verify a property and the refinement decision in each step is hard to interpret, thus hindering their analysis, reasoning and optimization.In this work, we propose SURGEON, a novel DNN verification refinement approach that is both effective and interpretable, allowing analyst to understand why and how each refinement decision is made. The main insight is to leverage the ‘interpretable’ nature of debugging processes and formulate the verification refinement problem as a debugging problem. Given a failed verification procedure, SURGEON refines it in an iterative manner and, in each iteration, it effectively identifies the root cause of the failure and heuristically generates fixes according to abstract transformers.We have implemented SURGEON in a prototype and evaluated it using a set of local robustness verification problems. Besides the interpretability, the experimental results show our approach can improve the precision of base verification methods and is more effective than existing refinement techniques.

Smart contracts are computerized transaction protocols built on top of blockchain networks. Users are charged with fees, a.k.a. gas in Ethereum, when they create, deploy or execute smart contracts. Since smart contracts may contain vulnerabilities which may result in huge financial loss, developers and smart contract compilers often insert codes for security checks. The trouble is that those codes consume gas every time they are executed. Many of the inserted codes are however redundant. In this work, we present sOptimize, a tool that optimizes smart contract gas consumption automatically without compromising functionality or security. sOptimize works on smart contract bytecode, statically identifies 3 kinds of code patterns, and further removes them through verification-assisted techniques. The resulting code is guaranteed to be equivalent to the original one and can be directly deployed on blockchain. We evaluate sOptimize on a collection of 1,152 real-world smart contracts and show that it optimizes 43% of them, and the reduction on gas consumption is about 2.0% while in deployment and 1.2% in transactions, the amount can be as high as 954,201 gas units per contract.

We propose DGG: Deep clustering via a Gaussian-mixture variational autoencoder (VAE) with Graph embedding. To facilitate clustering, we apply Gaussian mixture model (GMM) as the prior in VAE. To handle data with complex spread, we apply graph embedding. Our idea is that graph information which captures local data structures is an excellent complement to deep GMM. Combining them facilitates the network to learn powerful representations that follow global model and local structural constraints. Therefore, our method unifies model-based and similarity-based approaches for clustering. To combine graph embedding with probabilistic deep GMM, we propose a novel stochastic extension of graph embedding: we treat samples as nodes on a graph and minimize the weighted distance between their posterior distributions. We apply Jenson-Shannon divergence as the distance. We combine the divergence minimization with the log-likelihood maximization of the deep GMM. We derive formulations to obtain an unified objective that enables simultaneous deep representation learning and clustering. Our experimental results show that our proposed DGG outperforms recent deep Gaussian mixture methods (model-based) and deep spectral clustering (similarity-based). Our results highlight advantages of combining model-based and similarity-based clustering as proposed in this work. Our code is published here: https:// github.com/dodoyang0929/DGG.git.

Automatic loop-invariant generation is important in program analysis and verification. In this paper, we propose to generate loop-invariants automatically through learning and verification. Given a Hoare triple of a program containing a loop, we start with randomly testing the program, collect program states at run-time and categorize them based on whether they satisfy the invariant to be discovered. Next, classification techniques are employed to generate a candidate loop-invariant automatically. Afterwards, we refine the candidate through selective sampling so as to overcome the lack of sufficient test cases. Only after a candidate invariant cannot be improved further through selective sampling, we verify whether it can be used to prove the Hoare triple. If it cannot, the generated counterexamples are added as new tests and we repeat the above process. Furthermore, we show that by introducing a path-sensitive learning, i.e., partitioning the program states according to program locations they visit and classifying each partition separately, we are able to learn disjunctive loop-invariants. In order to evaluate our idea, a prototype tool has been developed and the experiment results show that our approach complements existing approaches.

We introduce a fast invariant inference framework based on active learning and SVMs (Support Vector Machines) which aims to systematically generate a variety of loop invariants efficiently. Given a program containing one loop along with a precondition and a post-condition, our approach can learn an invariant which is sufficiently strong for program verification or otherwise provide counter-examples to assist software developers to locate program bugs. By invoking learning and checking phases iteratively, our preliminary experiments show, this approach may be potentially more effective and efficient when compared with other existing approaches.