ECE 598HZ: Advanced Topics in Machine Learning and Formal Methods Fall 2024


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

Your name, netid Homework 2
Due Oct 31st 11:59pm

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:

In CROWN, since the choice of α (slope of the linear lower bound of ReLU: zˆj (i) ≥ αj (i) zj (i) , where 0 ≤ α ≤ 1) may lead to different answers, in this problem, we use the following “adaptive” rule to choose αj (i) for the linear lower bound of an unstable neuron j in the i-th layer:

Hereand are the preactivation bounds Now, answer the following questions. To get full credit, please show intermediate steps and linear equations (if applicable) that lead to your answer instead of just the final results.
  1. Use interval bound propagation (IBP) to calculate the lower bound of y (5pts)
  2. 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)
  3. Using the intermediate layer bounds you obtained in step 2, calculate CROWN lower bound on the output y. (10pts)
  4. 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)
  5. 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)

Code example: See the Problem 2 folder in the zipped code file.

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:

1. Complete the code for the MILP formulation using the given template. The parts that you need to finish have been marked with TODOs in source files. Using the MILP formulation, you should obtain an exact solution (global minimum) for optimization problems. Submit your completed program mip.py. (15pts)
2. Change the code and allow the integer variables (p ( j i) using the notation in our lecture) to take continuous values from 0 to 1, which gives the LP formulation. Using the LP formulation, you can only obtain a lower bound for the verification objective. Submit your completed program as lp.py. (10pts)
3. Using the data data1.pth, collect the exact solution found by the MILP formulation and the lower bound found by the LP formulate for perturbation size s = {0, 0.001, 0.003, 0.01, 0.03, 0.1}. Plot or list the results showing the gap between the exact solution and the lower bound at dif ferent perturbation sizes for all 9 optimization objectives. If program does not finish within 10 minutes, you can report “timeout”. (10pts)

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)

In our lecture, we discussed how to propagate CROWN linear bounds through a non-linear function in a neural network, such as a ReLU function. In this problem, you will work on developing bound propagation over a network with another commonly used nonlinear function, the clip function defined as:

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

(1) but now writing the linear bounds as a function of αs (hint: unlike ReLU, there can be more than one α to optimize in clip). (5pts)
A special case of the clip function is the hardtanh function (a = −1, b = 1), which is a frequently used neural network activation function:

You are requested to implement this special case. To help you, we provide a reference imple mentation of the CROWN algorithm for feedforward ReLU networks. The hardtanh network you will be working on has the same architecture as the ReLU network, so you just need to focus on changing the activation function part.

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).

1. Please carefully read the provided code files, and understand how CROWN is implemented. Pay particular attention to how the bounds are propagated through each layer. (0pts)

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)

3. As a sanity check, write a simple program to sample 10,000 inputs x randomly and uniformly from S, evaluate the neural network at all 10,000 x, and take the minimum value (per output neuron) as the empirical lower bound for each output neuron. Report the empirical lower bound you found when using data1.pth as the input. If your empirical lower bound is smaller than the CROWN lower bound you found in the previous step, you should double check your implementation. (5pts)

4. (Bonus) Implement α-CROWN with optimized bounds for hardtanh and report its improvements. (bonus 15pts)

Note For Problem 2 and 3, please use the provided code example code example.zip (up loaded to Canvas, along with HW2). The README file provides some useful instructions. For technical questions like package installation, you can contact TA Junyu Zhang ([email protected]) for help.

发表评论

电子邮件地址不会被公开。 必填项已用*标注