Alert button
Picture for Haoze Wu

Haoze Wu

Alert button

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

May 22, 2023
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark Barrett

Figure 1 for Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Figure 2 for Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Figure 3 for Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Figure 4 for Lightweight Online Learning for Sets of Related Problems in Automated Reasoning

We present Self-Driven Strategy Learning ($\textit{sdsl}$), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. $\textit{sdsl}$ does not require offline training, but instead automatically constructs a dataset while solving earlier problems. It fits a machine learning model to this data which is then used to adjust the solving strategy for later problems. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the sdsl calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the Kissat solver and show that the combination of Kissat+$\textit{sdsl}$ certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.

* Under submission 
Viaarxiv icon

Soy: An Efficient MILP Solver for Piecewise-Affine Systems

Mar 23, 2023
Haoze Wu, Min Wu, Dorsa Sadigh, Clark Barrett

Figure 1 for Soy: An Efficient MILP Solver for Piecewise-Affine Systems
Figure 2 for Soy: An Efficient MILP Solver for Piecewise-Affine Systems
Figure 3 for Soy: An Efficient MILP Solver for Piecewise-Affine Systems
Figure 4 for Soy: An Efficient MILP Solver for Piecewise-Affine Systems

Piecewise-affine (PWA) systems are widely used for modeling and control of robotics problems including modeling contact dynamics. A common approach is to encode the control problem of the PWA system as a Mixed-Integer Convex Program (MICP), which can be solved by general-purpose off-the-shelf MICP solvers. To mitigate the scalability challenge of solving these MICP problems, existing work focuses on devising efficient and strong formulations of the problems, while less effort has been spent on exploiting their specific structure to develop specialized solvers. The latter is the theme of our work. We focus on efficiently handling one-hot constraints, which are particularly relevant when encoding PWA dynamics. We have implemented our techniques in a tool, Soy, which organically integrates logical reasoning, arithmetic reasoning, and stochastic local search. For a set of PWA control benchmarks, Soy solves more problems, faster, than two state-of-the-art MICP solvers.

* Under submission 
Viaarxiv icon

Convex Bounds on the Softmax Function with Applications to Robustness Verification

Mar 03, 2023
Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark Barrett, Eitan Farchi

Figure 1 for Convex Bounds on the Softmax Function with Applications to Robustness Verification
Figure 2 for Convex Bounds on the Softmax Function with Applications to Robustness Verification
Figure 3 for Convex Bounds on the Softmax Function with Applications to Robustness Verification
Figure 4 for Convex Bounds on the Softmax Function with Applications to Robustness Verification

The softmax function is a ubiquitous component at the output of neural networks and increasingly in intermediate layers as well. This paper provides convex lower bounds and concave upper bounds on the softmax function, which are compatible with convex optimization formulations for characterizing neural networks and other ML models. We derive bounds using both a natural exponential-reciprocal decomposition of the softmax as well as an alternative decomposition in terms of the log-sum-exp function. The new bounds are provably and/or numerically tighter than linear bounds obtained in previous work on robustness verification of transformers. As illustrations of the utility of the bounds, we apply them to verification of transformers as well as of the robustness of predictive uncertainty estimates of deep ensembles.

* AISTATS 2023 
Viaarxiv icon

VeriX: Towards Verified Explainability of Deep Neural Networks

Dec 06, 2022
Min Wu, Haoze Wu, Clark Barrett

Figure 1 for VeriX: Towards Verified Explainability of Deep Neural Networks
Figure 2 for VeriX: Towards Verified Explainability of Deep Neural Networks
Figure 3 for VeriX: Towards Verified Explainability of Deep Neural Networks
Figure 4 for VeriX: Towards Verified Explainability of Deep Neural Networks

We present VeriX, a first step towards verified explainability of machine learning models in safety-critical applications. Specifically, our sound and optimal explanations can guarantee prediction invariance against bounded perturbations. We utilise constraint solving techniques together with feature sensitivity ranking to efficiently compute these explanations. We evaluate our approach on image recognition benchmarks and a real-world scenario of autonomous aircraft taxiing.

* To appear in Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI 2023) 
Viaarxiv icon

On Optimizing Back-Substitution Methods for Neural Network Verification

Aug 16, 2022
Tom Zelazny, Haoze Wu, Clark Barrett, Guy Katz

Figure 1 for On Optimizing Back-Substitution Methods for Neural Network Verification
Figure 2 for On Optimizing Back-Substitution Methods for Neural Network Verification
Figure 3 for On Optimizing Back-Substitution Methods for Neural Network Verification
Figure 4 for On Optimizing Back-Substitution Methods for Neural Network Verification

With the increasing application of deep learning in mission-critical systems, there is a growing need to obtain formal guarantees about the behaviors of neural networks. Indeed, many approaches for verifying neural networks have been recently proposed, but these generally struggle with limited scalability or insufficient accuracy. A key component in many state-of-the-art verification schemes is computing lower and upper bounds on the values that neurons in the network can obtain for a specific input domain -- and the tighter these bounds, the more likely the verification is to succeed. Many common algorithms for computing these bounds are variations of the symbolic-bound propagation method; and among these, approaches that utilize a process called back-substitution are particularly successful. In this paper, we present an approach for making back-substitution produce tighter bounds. To achieve this, we formulate and then minimize the imprecision errors incurred during back-substitution. Our technique is general, in the sense that it can be integrated into numerous existing symbolic-bound propagation techniques, with only minor modifications. We implement our approach as a proof-of-concept tool, and present favorable results compared to state-of-the-art verifiers that perform back-substitution.

* This is the extended version of a paper with the same title that appeared at FMCAD 2022 
Viaarxiv icon

Toward Certified Robustness Against Real-World Distribution Shifts

Jun 09, 2022
Haoze Wu, Teruhiro Tagomori, Alexander Robey, Fengjun Yang, Nikolai Matni, George Pappas, Hamed Hassani, Corina Pasareanu, Clark Barrett

Figure 1 for Toward Certified Robustness Against Real-World Distribution Shifts
Figure 2 for Toward Certified Robustness Against Real-World Distribution Shifts
Figure 3 for Toward Certified Robustness Against Real-World Distribution Shifts
Figure 4 for Toward Certified Robustness Against Real-World Distribution Shifts

We consider the problem of certifying the robustness of deep neural networks against real-world distribution shifts. To do so, we bridge the gap between hand-crafted specifications and realistic deployment settings by proposing a novel neural-symbolic verification framework, in which we train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations, which are fundamental to many state-of-the-art generative models. To address this challenge, we propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement. The key idea is to "lazily" refine the abstraction of sigmoid functions to exclude spurious counter-examples found in the previous abstraction, thus guaranteeing progress in the verification process while keeping the state-space small. Experiments on the MNIST and CIFAR-10 datasets show that our framework significantly outperforms existing methods on a range of challenging distribution shifts.

* Under submission 
Viaarxiv icon

Efficient Neural Network Analysis with Sum-of-Infeasibilities

Mar 19, 2022
Haoze Wu, Aleksandar Zeljić, Guy Katz, Clark Barrett

Figure 1 for Efficient Neural Network Analysis with Sum-of-Infeasibilities
Figure 2 for Efficient Neural Network Analysis with Sum-of-Infeasibilities
Figure 3 for Efficient Neural Network Analysis with Sum-of-Infeasibilities
Figure 4 for Efficient Neural Network Analysis with Sum-of-Infeasibilities

Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, DeepSoI, to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI. Extending the complete search with DeepSoI achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.

* TACAS'22 
Viaarxiv icon

Scalable Verification of GNN-based Job Schedulers

Mar 07, 2022
Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh

Figure 1 for Scalable Verification of GNN-based Job Schedulers
Figure 2 for Scalable Verification of GNN-based Job Schedulers
Figure 3 for Scalable Verification of GNN-based Job Schedulers
Figure 4 for Scalable Verification of GNN-based Job Schedulers

Recently, Graph Neural Networks (GNNs) have been applied for scheduling jobs over clusters achieving better performance than hand-crafted heuristics. Despite their impressive performance, concerns remain over their trustworthiness when deployed in a real-world environment due to their black-box nature. To address these limitations, we consider formal verification of their expected properties such as strategy proofness and locality in this work. We address several domain-specific challenges such as deeper networks and richer specifications not encountered by existing verifiers for image and NLP classifiers. We develop GNN-Verify, the first general framework for verifying both single-step and multi-step properties of these schedulers based on carefully designed algorithms that combine abstractions, refinements, solvers, and proof transfer. Our experimental results on challenging benchmarks show that our approach can provide precise and scalable formal guarantees on the trustworthiness of state-of-the-art GNN-based scheduler.

* Under submission 
Viaarxiv icon

DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers

Mar 02, 2021
Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark Barrett

Figure 1 for DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers
Figure 2 for DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers
Figure 3 for DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers
Figure 4 for DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers

We introduce DeepCert, a tool-supported method for verifying the robustness of deep neural network (DNN) image classifiers to contextually relevant perturbations such as blur, haze, and changes in image contrast. While the robustness of DNN classifiers has been the subject of intense research in recent years, the solutions delivered by this research focus on verifying DNN robustness to small perturbations in the images being classified, with perturbation magnitude measured using established Lp norms. This is useful for identifying potential adversarial attacks on DNN image classifiers, but cannot verify DNN robustness to contextually relevant image perturbations, which are typically not small when expressed with Lp norms. DeepCert addresses this underexplored verification problem by supporting:(1) the encoding of real-world image perturbations; (2) the systematic evaluation of contextually relevant DNN robustness, using both testing and formal verification; (3) the generation of contextually relevant counterexamples; and, through these, (4) the selection of DNN image classifiers suitable for the operational context (i)envisaged when a potentially safety-critical system is designed, or (ii)observed by a deployed system. We demonstrate the effectiveness of DeepCert by showing how it can be used to verify the robustness of DNN image classifiers build for two benchmark datasets (`German Traffic Sign' and `CIFAR-10') to multiple contextually relevant perturbations.

Viaarxiv icon