-
Notifications
You must be signed in to change notification settings - Fork 0
/
tutorial.py
233 lines (176 loc) · 7.53 KB
/
tutorial.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
import warnings; warnings.filterwarnings("ignore")
""" Import our framework `sytorch`
==============================
We implement our framework `sytorch`, which extends PyTorch with symbolic
execution. It supports
- Symbolic forward execution of concrete (or symbolic) input tensors with
some DNN parameters considered as symbolic variables.
- Encoding encoding of symbolic constraints on (array of) symbolic
expressions to formulate an LP problem.
- Optimize the LP problem using Gurobi and update the DNN parameters
using the optimal solution.
And `sytorch` inherits everything from `torch.*`.
We implement the repair approaches APRNN and PRDNN experiments using
`sytorch` in scripts, just like implementing a new training approach in a
`torch` training script.
"""
import sytorch as st
""" Working device and data type.
=============================
- `device` specifies the working device. Our framework `sytorch` supports
tensors or parameters on GPU (`cuda`) and handle them properly.
- `dtype` specifies the working data type. Because Gurobi internally uses
double precision (`float64`), we recommend to use `float64` when encoding
the LP problem. After repair, user could cast the DNN back to the desired
data type.
"""
device = st.device('cpu')
dtype = st.float64
""" Loading the buggy DNN.
======================
`st.nn` extends `torch.nn` and provides the exact same interface to
construct a DNN. For example, the following code constructs a
fully-connected ReLU DNN.
One could also take a PyTorch DNN `torch_dnn_object` and convert it to a
SyTorch-compatible DNN using `st.nn.from_torch`:
```
dnn = st.nn.from_torch(torch_dnn)
```
Moreover, one could take an saved ONNX DNN `onnx_dnn_path` and load it as a
SyTorch-compatible DNN using `st.nn.from_file`:
```
dnn = st.nn.from_file(onnx_dnn_path)
```
Although for now we only support sequential ONNX DNNs, i.e., no skip
connections.
"""
dnn = st.nn.Sequential(
st.nn.Linear(1, 3),
st.nn.ReLU(),
st.nn.Linear(3, 1),
).to(device=device, dtype=dtype)
""" Here we load the example DNN `N1` used in the overview of our paper. """
with st.no_grad():
dnn[0].weight[:] = st.tensor([-1.0, 1.0, 0.5], device=device, dtype=dtype)[:,None]
dnn[0].bias [:] = st.tensor([0.0, -2.0, 0.0], device=device, dtype=dtype)
dnn[2].weight[:] = st.tensor([0.5, -0.5, 1.,], device=device, dtype=dtype)[None,:]
dnn[2].bias [:] = -0.5
""" Load buggy inputs.
==================
Just like PyTorch, SyTorch takes any tensor of compatible shape as input,
and symbolically forwards it through the network. One could also use
existing torch datasets and dataloaders from training scripts.
Here we load the buggy input point from Section 3.1 of our paper.
"""
points = st.tensor([ [-1.5], [-0.5], ], dtype=dtype, device=device)
""" Create a new Gurobi-based solver.
================================
- `solver.solver` is the underlying gurobipy solver (model).
- `GurobiSolver` provides
- `.reals(shape)` to create a symbolic array (`numpy.ndarray`) of
gurobipy variables.
- `add_constraints(constrs)` to add constraints.
- `minimize(obj)` and `maximize(obj)` to add an objective.
- `solve()` to solve the model.
- A symbolic array overrides the following operators for constructing
symbolic expressions and formulas (constraints):
- arithmetic operators `+`, `-`, `*`, `/`,
- matrix multiplication `@`,
- logical operators `==`, `>`, `>=`, `<`, `<=`,
and provides the following methods for constructing symbolic expressions
- `sum()`,
- `abs_ub()`,
- `max_ub()`,
- `norm_ub()`.
"""
solver = st.GurobiSolver()
""" Attach the DNN to the solver.
=============================
- `.deepcopy()` returns a deepcopy of the DNN to repair. This is optional.
- `.to(solver)` attaches the DNN to the solver, just like how you attach a
DNN to a device in PyTorch.
- `.repair()` turns on the repair mode and enables symbolic execution. It
works just like `.train()` in PyTorch, which turns on the training mode.
"""
N = dnn.deepcopy().to(solver).repair()
""" Specify the symbolic weights.
==============================
SyTorch extends PyTorch's `parameter` and `module` with a
`.requires_symbolic_(...)` method, which makes the parameter or the
module's parameters symbolic.
For example, the following code makes the first layer weight and bias
symbolic:
```
dnn[1].weight.requires_symbolic_(lb=-3., ub=3.)
```
The following code makes the first layer weight and bias symbolic:
```
dnn[1].requires_symbolic_(lb=-3., ub=3.)
```
The following code makes the first layer weight and all layers' bias symbolic:
```
dnn.requires_symbolic_weight_and_bias(lb=-3., ub=3.)
```
"""
N.requires_symbolic_weight_and_bias(lb=-3., ub=3.)
""" Calculate the original output for minimization.
==============================================
- The `st.no_symbolic()` context turns off the symbolic execution, just like
`torch.no_grad()` turns off the gradient computation in PyTorch.
"""
with st.no_symbolic(), st.no_grad():
reference_outputs = N(points)
""" Calculate the symbolic output.
===========================
`N(points)` symbolically forwards `points` through `N` with the default
reference points `points`. It is equivalent to
```
pattern = N.activation_pattern(points)
symbolic_output = N(points, pattern=pattern)
```
`symbolic_output` is a `numpy.ndarray` of symbolic expressions with the
same shape as `reference_outputs`.
"""
symbolic_outputs = N(points)
""" Construct the minimization objective.
====================================
- `param_deltas` is the concatenation of all parameter delta in a 1D array.
- `output_deltas` is the symbolic output delta flatten into 1D array.
- `all_deltas` is the concatenation of `output_deltas` and `param_deltas`.
- `.alias()` creates a corresponding array of variables that equals to
the given array of symbolic expressions.
- `.norm_ub('linf+l1_normalized')` encodes the (upper-bound) of
the sum of L^inf norm and normalized L^1 norm.
- `solver.minimize(obj)` sets the minimization objective.
"""
param_deltas = N.parameter_deltas(concat=True)
output_deltas = (symbolic_outputs - reference_outputs).flatten().alias()
all_deltas = st.cat([output_deltas, param_deltas])
obj = all_deltas.norm_ub('linf+l1_normalized')
""" Solve the constraints while minimizing the objective.
====================================================
Here we constrain the `symbolic_outputs` to be within `[-0.1, 0.1]`.
`solver.solve(*constrs, minimize=obj)` solves the constraints `constrs`
while minimizing `obj`. Here `constrs=(-0.1 <= symbolic_outputs,
symbolic_outputs <= 0.1)`.
"""
feasible = solver.solve(
-0.1 <= symbolic_outputs,
symbolic_outputs <= 0.1,
minimize=obj
)
""" Update `N` with new parameters.
===============================
- `.update_()` inplace updates `N`'s parameters with the solution.
- `.repair(False)` turns off the repair (symbolic execution) mode.
"""
if feasible:
N.update_().repair(False)
print("Succeed.")
with st.no_grad():
print(f"Original output which is outside [-0.1, 0.1]:")
print(dnn(points))
print(f"Repaired output which is within [-0.1, 0.1]:")
print(N(points))
else:
print("Infeasible.")