Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due
ECE 598HZ: Advanced Topics in Machine Learning and Formal Methods Fall 2024
Typeset your solutions using LATEX zip your solutions in a single file called netid-598-F24.zip and upload this file through Canvas.
Start working on your homework EARLY!
Problem 1: CROWN Bound propagation on Irregular Neural Network (30pts)
In this problem, we consider an irregular neural network with a “skip” connection and two inputs x1, x2 added to two different layers of the neural network. The output of the network y is defined as:
Here the inputs x1, x2 ∈ R 2 and y ∈ R. The input set S = {x1, x2 | − 1 ≤ x1,1 ≤ 1, −1 ≤ x1,2 ≤ 1, −2 ≤ x2,1 ≤ −1, 1 ≤ x2,2 ≤ 2}, where xi,j represents the j-th element in xi . The network weights are defined as:
- Use interval bound propagation (IBP) to calculate the lower bound of y (5pts)
- Use CROWN to calculate the intermediate layer lower and upper bounds of z (2). You will need these bounds to obtain linear relaxations for zˆ (2) = ReLU(z (2)) in your next step. (10pts)
- Using the intermediate layer bounds you obtained in step 2, calculate CROWN lower bound on the output y. (10pts)
- Now we consider optimizing α to tighten the lower bound of y for this neural network. As suming all ReLU neurons are unstable, how many αs can we use to get the tightest possible lower bound of y? (hint 1: tighter intermediate layer bounds can lead to a tighter bound on y, and intermediate layer bounds can be optimized independently; hint 2: to obtain the tightest lower bounds and upper bounds, two sets of αs can be used, one for the lower bounds and one for the upper bounds). (5pts)
- Can you show one setting of α that leads to a tighter lower bound compared to the lower bound calculated in step 3? (bonus 15 pts)
Problem 2: Implementing the Mixed Integer Programming and Linear Programming Formulations for Neural Network Verification (35 pts)
In our lecture, we discussed the linear programming formulation and mixed integer linear pro gramming formulation for neural network verification. In this problem, you will implement these formulations on a simple neural network.
The example code loads a simple pretrained feedforward model with three linear layers, and one test image (a handwritten digit, 0 - 9) from the MNIST dataset. The test image t ∈ R 784 contains 28 × 28 pixel values. Element-wise perturbation with a given perturbation size is added to each pixel: e.g., when the perturbation size is s, the input set S := {x | ti − s ≤ xi ≤ ti + s, ∀i ∈ [1, 784]}. The neural network predicts scores y ∈ R 10, and yi represents the score for the image being recognized as a digit i. If the label of test image t is c, we want to verify that yc is always the top-1 score for all x ∈ S by solving 9 optimization objectives.
You can run code template mip assigment.py with an input data data1.pth by running python3 mip assigment.py data1.pth. The README document in the repository provides additional instructions for running the code.
You will use the Gurobi optimizer to solve MILP and LP problems. Your code needs to formulate the verification problem using the Python interface of Gurobi. You can refer to the Gurobi Python documentation available at this link.
Note that MILP and LP formulations require the pre-activation intermediate layer bounds (upper bound u ( j i) and lower bound l j (i) ). In the given implementation, these bounds need to be computed using the MILP/LP formulation as well, by treating zj (i) as the optimization objective.
Now, complete the following tasks:
4. Use LP or MIP to solve the lower bound for the irregular neural network in Problem 1 (you will need to extend the LP/MIP formulation to an irregular neural network), and compare the exact object from MIP, the lower bound from LP, to the CROWN lower bound you ob tained in task 3 of Problem 1. (bonus 15pts)
Problem 3: Deriving and implementing CROWN for a new activation function (35pts)
Graphically, the function clips the input z into the range [a, b]. Here a ≤ b are two constants that will not be perturbed.
1. Derive the linear lower and upper bounds for clip(z) given the preactivation bounds l ≤ z ≤ u. Use the tightest linear bounds when possible, and when there are multiple possible solutions (like the linear lower bound for ReLU), you can make the lower and upper bounds use the same slope. (Hint: you will need to consider different segments of the function, see Table 2, Table 3, Figure 1 and the case studies in the CROWN paper). (10pts)
2. For the linear lower and upper bounds of clip(z), do we have optimizable parameters similar to α in ReLU? If you believe the linear bounds are optimizable, please repeat the above step
Code example: See the Problem 3 folder in the zipped code file.
You can run the ReLU reference code using python3 crown.py data1.pth. The network used is the same as the previous question, and the definition of the input set S is also the same. data1.pth gives the test input t. The program, by default, will print the lower and upper bounds for all 10 output neurons given this input with perturbation size s = 0.01 (changeable in the code).
2. Implement CROWN for hardtanh network using the provided code template. Report the lower and upper bounds for all 10 output neurons when data1.pth is used as the input. The correctness of your program will also be graded on an undisclosed input test.pth by the TA. (15pts)
4. (Bonus) Implement α-CROWN with optimized bounds for hardtanh and report its improvements. (bonus 15pts)