Encoding Forward pass of a Neural Network in Z3

Encoding Forward pass of a Neural Network in Z3

Author: codersguild

Code Examples/Z3 Examples/z3_Neural_Networks.py

@@ -1,83 +1,118 @@
-# Encoding of a Neural Network in Z3. 
+# Encoding of a Neural Network in Z3 
+# A custom loss function.
+# A Forward pass over one hiddebn layer.
 from z3 import *
 import numpy as np
 
 if __name__ == "__main__":
 
+ MIDDLE_LAYER_OUT = 6
+ # Z3 Sovler instance. 
  S = z3.Solver()
 
- inputs = [z3.Real(f"{i}_l1") for i in ["x_input","y_input","n_input","a_input"]]
- outputs1 = [z3.Real(f"activation_{i}") for i in range(10)]
- 
- outputs = [z3.Real(f"{i}_l1") for i in ["C_0","C_1","C_2","C_3"]]
+ # Inputs to the neural network, loss and intermediate sumVal.
+ inputs = [z3.Real(f"{i}_l1") for i in ["x_input","y_input","n_input","a_input"]] 
  sumVal = z3.Real("sumVal")
  loss = z3.Real("loss")
 
+ # First Fully Connected Layer. weigths, bias and outputs
  layer_1_weights = [[z3.Real(f"weight_l1_{i}_{j}")
- for j in range(10)]
+ for j in range(MIDDLE_LAYER_OUT)]
  for i in range(4)]
 
- layer_1_bias = [z3.Real(f"bias_l1_{i}") for i in range(10)]
+ layer_1_bias = [z3.Real(f"bias_l1_{i}") for i in range(MIDDLE_LAYER_OUT)]
+ outputs1 = [z3.Real(f"activation_{i}") for i in range(MIDDLE_LAYER_OUT)]
 
+ # Second Fully Connected Layer. weigths, bias and outputs
  layer_2_weights = [[z3.Real(f"weight_l2_{i}_{j}")
  for j in range(4)]
- for i in range(10)]
+ for i in range(MIDDLE_LAYER_OUT)]
 
  layer_2_bias = [z3.Real(f"bias_l2_{i}") for i in range(4)]
+ outputs = [z3.Real(f"{i}_l1") for i in ["C_0","C_1","C_2","C_3"]]
 
+ # Convert to np.matrix, np.array
+ # Just to make doing the math easier.
  weights1 = np.matrix(layer_1_weights)
  bias1 = np.matrix(layer_1_bias)
- activation1 = np.matrix(outputs1)
  weights2 = np.matrix(layer_2_weights)
  bias2 = np.matrix(layer_2_bias)
  inp = np.matrix(inputs)
 
+ # Single Forward pass on the first layer.
  layer_1_out = weights1.T * inp.T + bias1.T
 
+ # Apply ReLU() to output of layer-1.
  for index, elems in enumerate(layer_1_out):
  rhs = elems.tolist()[0][0]
  lhs = outputs1[index]
  # ReLU Activation
  S.add(z3.If(rhs >= 0, lhs == rhs, lhs == 0))
  if index == 0:
  print(z3.If(rhs >= 0, lhs == rhs, lhs == 0))
- # print(f"{lhs} == {rhs}", end="\n\n")
 
+ # Single Forward pass on the second layer.
+ # Use the activations from the first layer.
+ activation1 = np.matrix(outputs1)
  layer_2_out = activation1 * weights2 + bias2
 
+ # Apply ReLU() to output to layer-2.
  for index, elems in enumerate(layer_2_out):
  rhs = elems.tolist()[0][0]
  lhs = outputs[index]
  # ReLU Activation
  S.add(z3.If(rhs >= 0, lhs == rhs, lhs == 0))
  if index == 0:
  print(z3.If(rhs >= 0, lhs == rhs, lhs == 0))
- # print(f"{lhs} == {rhs}", end="\n\n")
 
+ # dot product of coefficients
+ # This is the case for the specific loss function
+ # we are trying to use here.
  sumVal = z3.Sum([(inputs[index] * outputs[index]) for index in range(4)])
  print(sumVal)
 
+ # Put some restrictions on what the values for 
+ # the weights and the biases can be for both the layers.
  weights_constraint = []
  [[weights_constraint.append(j > 2) for j in i] for i in layer_1_weights]
  S.add(z3.And(weights_constraint))
+ 
  weights_constraint = []
  [[weights_constraint.append(j > 3) for j in i] for i in layer_2_weights]
  S.add(z3.And(weights_constraint))
 
+ # Put some restrictions on what the values for 
+ # the weights and the biases can be for both the layers.
  [S.add(elem > 1) for elem in layer_1_bias]
  [S.add(elem > 7) for elem in layer_2_bias]
 
- [S.add(j > 14) for j in inputs]
+ # Specifying a range of values that the
+ # can be passed as input to the neural network.
+ [S.add(j > 0) for j in inputs]
+ [S.add(j <= 1024) for j in inputs]
+ 
+ # We want to enforce that none of the 
+ # last layer neurons give zero output.
+ # this is a requirement for this 
+ # specific problem. 
  [S.add(j != 0) for j in outputs]
 
- # Loss
+ # Final Loss function that uses inputs and the sumVal computed above. 
  S.add(loss == sumVal ** 2 + 10000 * z3.If(inputs[1] - inputs[-1] >= 0, inputs[1] - inputs[-1], 0)) 
- S.add(loss == 0)
+ S.add(z3.ForAll([x for x in inputs], (sumVal ** 2 + 10000 * z3.If(inputs[1] - inputs[-1] >= 0, inputs[1] - inputs[-1], 0)) == 0))
 
- # print(S.assertions())
- print(S.check())
- print(S.model())
+ # Write query to the file and check 
+ # with z3. 
+ # z3 -v:5 -st -smt2 ...
+ with open("query.smt2", mode="w") as smt_writer:
+ smt_writer.write(S.to_smt2())
+ 
+ # Uncomment if needed.
+ # # print(S.assertions())
+ # print(S.check())
+ # print(S.model())
 
+# A possible answer after 210 hours.
 # [weight_l1_3_3 = 131073/65536,
 # weight_l2_2_2 = 4,
 # n_input_l1 = 15,