skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Parallel Verification for delta-Equivalence of Neural Network Quantization
Quantization replaces floating point arithmetic with integer arithmetic in deep neural networks, enabling more efficient on-device inference with less power and memory. However, it also brings in loss of generalization and even potential errors to the models. In this work, we propose a parallelization technique for formally verifying the equivalence between quantized models and their original real-valued counterparts. In order to guarantee both soundness and completeness, mixed integer linear programming (MILP) is deployed as the baseline technique. Nevertheless, the incorporation of two networks as well as the mixture of integer and real number arithmetic make the problem much more challenging than verifying a single network, and thus using MILP alone is inadequate for the non-trivial cases. To tackle this, we design a distributed verification technique that can leverage hundreds of CPUs on high-performance computing clusters. We develop a two-tier parallel framework and propose property- and output-based partition strategies. Evaluated on perception networks quantized with PyTorch, our approach outperforms existing methods in successfully verifying many cases that are otherwise considered infeasible.  more » « less
Award ID(s):
2211505
PAR ID:
10584656
Author(s) / Creator(s):
; ; ; ; ; ;
Editor(s):
Avni, Guy; Giacobbe, Mirco; Johnson, Taylor T; Katz, Guy; Lukina, Anna; Narodytska, Nina; Schilling, Christian
Publisher / Repository:
Springer Nature Switzerland
Date Published:
Page Range / eLocation ID:
78 to 99
Subject(s) / Keyword(s):
Quantized neural networks Equivalence verification Parallel computing
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; (, Proceedings of the ACM on Programming Languages)
    While mixed integer linear programming (MILP) solvers are routinely used to solve a wide range of important science and engineering problems, it remains a challenging task for end users to write correct and efficient MILP constraints, especially for problems specified using the inherently non-linear Boolean logic operations. To overcome this challenge, we propose a syntax guided synthesis (SyGuS) method capable of generating high-quality MILP constraints from the specifications expressed using arbitrary combinations of Boolean logic operations. At the center of our method is an extensible domain specification language (DSL) whose expressiveness may be improved by adding new integer variables as decision variables, together with an iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations using these integer variables. To make the synthesis method efficient, we also propose an over-approximation technique for soundly proving the correctness of the synthesized linear constraints, and an under-approximation technique for safely pruning away the incorrect constraints. We have implemented and evaluated the method on a wide range of benchmark specifications from statistics, machine learning, and data science applications. The experimental results show that the method is efficient in handling these benchmarks, and the quality of the synthesized MILP constraints is close to, or higher than, that of manually-written constraints in terms of both compactness and solving time. 
    more » « less
  2. ; ; ; (, Journal of Modern Power Systems and Clean Energy)
    Recently, we demonstrated the success of a time-synchronized state estimator using deep neural networks (DNNs) for real-time unobservable distribution systems. In this paper, we provide analytical bounds on the performance of the state estimator as a function of perturbations in the input measurements. It has already been shown that evaluating performance based only on the test dataset might not effectively indicate the ability of a trained DNN to handle input perturbations. As such, we analytically verify the robustness and trustworthiness of DNNs to input perturbations by treating them as mixed-integer linear programming (MILP) problems. The ability of batch normalization in addressing the scalability limitations of the MILP formulation is also highlighted. The framework is validated by performing time-synchronized distribution system state estimation for a modified IEEE 34-node system and a real-world large distribution system, both of which are incompletely observed by micro-phasor measurement units. 
    more » « less
  3. ; ; (, IEEE Power Tech Conference)
    Although knowing the feeder topology and line impedances is a prerequisite for solving any grid optimization task, utilities oftentimes have limited or outdated information on their electric network assets. Given the rampant integration of smart inverters, we have previously advocated perturbing their power injections to unveil the underlying grid topology using the induced voltage responses. Under an approximate grid model, the perturbed power injections and the collected voltage deviations obey a linear regression setup, where the unknown is the vector of line resistances. Building on this model, topology processing can be performed in two steps. Given a candidate radial topology, the line resistances can be estimated via a least-squares (LS) fit on the probing data. The topology attaining the best fit can be then selected. To avoid evaluating the exponentially many candidate topologies, this two-step approach is uniquely formulated as a mixed-integer linear program (MILP) using the McCormick relaxation. If the recovered topology is not radial, a second, computationally more demanding MILP confines the search only within radial topologies. Numerical tests explain how topology recovery depends on the noise level and probing duration, and demonstrate that the first simpler MILP yields a tree topology in 90% of the cases tested. 
    more » « less
  4. ; (, IEEE International Conference on Robotics and Automation)
    The line coverage problem is the coverage of linear environment features (e.g., road networks, power lines), modeled as 1D segments, by one or more robots while respecting resource constraints (e.g., battery capacity, flight time) for each of the robots. The robots incur direction dependent costs and resource demands as they traverse the edges. We treat the line coverage problem as an optimization problem, with the total cost of the tours as the objective, by formulating it as a mixed integer linear program (MILP). The line coverage problem is NP-hard and hence we develop a heuristic algorithm, Merge- Embed-Merge (MEM). We compare it against the optimal MILP approach and a baseline heuristic algorithm, Extended Path Scanning. We show the MEM algorithm is fast and suitable for real-time applications. To tackle large-scale problems, our approach performs graph simplification and graph partitioning, followed by robot tour generation for each of the partitioned subgraphs. We demonstrate our approach on a large graph with 4,658 edges and 4,504 vertices that represents an urban region of about 16 sq. km. We compare the performance of the algorithms on several small road networks and experimentally demonstrate the approach using UAVs on the UNC Charlotte campus road network. 
    more » « less
  5. ; ; (, ISPRS International Journal of Geo-Information)
    Geospatial data conflation involves matching and combining two maps to create a new map. It has received increased research attention in recent years due to its wide range of applications in GIS (Geographic Information System) data production and analysis. The map assignment problem (conceptualized in the 1980s) is one of the earliest conflation methods, in which GIS features from two maps are matched by minimizing their total discrepancy or distance. Recently, more flexible optimization models have been proposed. This includes conflation models based on the network flow problem and new models based on Mixed Integer Linear Programming (MILP). A natural question is: how are these models related or different, and how do they compare? In this study, an analytic review of major optimized conflation models in the literature is conducted and the structural linkages between them are identified. Moreover, a MILP model (the base-matching problem) and its bi-matching version are presented as a common basis. Our analysis shows that the assignment problem and all other optimized conflation models in the literature can be viewed or reformulated as variants of the base models. For network-flow based models, proof is presented that the base-matching problem is equivalent to the network-flow based fixed-charge-matching model. The equivalence of the MILP reformulation is also verified experimentally. For the existing MILP-based models, common notation is established and used to demonstrate that they are extensions of the base models in straight-forward ways. The contributions of this study are threefold. Firstly, it helps the analyst to understand the structural commonalities and differences of current conflation models and to choose different models. Secondly, by reformulating the network-flow models (and therefore, all current models) using MILP, the presented work eases the practical application of conflation by leveraging the many off-the-shelf MILP solvers. Thirdly, the base models can serve as a common ground for studying and writing new conflation models by allowing a modular and incremental way of model development. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email