diff --git a/app.py b/app.py new file mode 100644 index 0000000..4822002 --- /dev/null +++ b/app.py @@ -0,0 +1,61 @@ +import plotly.graph_objects as go +import pandas as pd + +# Corrected data with equal lengths for all arrays +data = { + 'Dataset': ['BM1', 'BM2', 'BM3', 'BM4', 'BM5', 'BM6', 'BM7', 'BM8', + 'GC1', 'GC2', 'GC3', 'GC4', 'GC5', + 'AC1', 'AC2', 'AC3', 'AC4', 'AC5', 'AC6', 'AC7', 'AC8', 'AC9', 'AC10', 'AC11', 'AC12'], + 'Model': ['Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', '[8]', + 'Kaggle', '[1, 24]', 'Kaggle', 'Kaggle', '[8]', + 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', 'Kaggle', '[8]', '[27, 28]', '[27, 28]', '[27, 28]', '[27, 28]', '[27, 28]'], + 'Source': ['', '', '[1, 24]', '', '', '', '', '', + '', '[1, 24]', '', '', '', + '', '[1, 24]', '', '', '', '', '', '', '', '', '', ''], + 'Layers': [4, 4, 3, 5, 4, 4, 4, 7, + 3, 3, 3, 4, 4, + 4, 3, 3, 4, 4, 4, 7, 4, 6, 6, 6, 11], + 'Neurons': [97, 65, 117, 318, 49, 35, 145, 141, + 64, 114, 23, 24, 138, + 45, 121, 71, 221, 149, 45, 145, 10, 12, 20, 40, 45], + 'Accuracy': [89.20, 88.76, 88.22, 89.55, 88.90, 88.94, 88.70, 89.20, + 72.67, 74.67, 75.33, 70.67, 69.33, + 85.24, 84.70, 84.52, 84.86, 85.19, 84.77, 84.85, 82.15, 81.22, 78.56, 79.25, 81.46] +} + +df = pd.DataFrame(data) + +# Create the figure +fig = go.Figure() + +# Add bar trace for accuracy +fig.add_trace(go.Bar( + x=df['Dataset'], + y=df['Accuracy'], + name='Accuracy', + marker_color='blue', + text=df['Accuracy'], + textposition='outside' +)) + +# Add scatter trace for neurons and layers +fig.add_trace(go.Scatter( + x=df['Dataset'], + y=df['Neurons'], + mode='markers', + name='Neurons', + marker=dict(color='green', symbol='circle'), + text=df.apply(lambda row: f'Neurons: {row["Neurons"]}, Layers: {row["Layers"]}', axis=1), + hoverinfo='text' +)) + +# Customize layout +fig.update_layout( + title='Neurons, Layers, and Accuracy Visualization', + xaxis=dict(title='Dataset'), + yaxis=dict(title='Value'), + barmode='group' +) + +# Show the figure +fig.show() diff --git a/requirements.txt b/requirements.txt index ffa6114..3b62d54 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,3 +1,3 @@ z3-solver tensorflow==2.5.0 -aif360 \ No newline at end of file +aif360 diff --git a/src/AC/Verify-AC.py b/src/AC/Verify-AC.py index b2ec250..39bbbd9 100644 --- a/src/AC/Verify-AC.py +++ b/src/AC/Verify-AC.py @@ -19,7 +19,7 @@ # In[] model_dir = '../../models/adult/' -result_dir = './libra/sex-' +result_dir = './res-' PARTITION_THRESHOLD = 10 SOFT_TIMEOUT = 100 @@ -303,7 +303,7 @@ import csv file_exists = os.path.isfile(file) - with open(file, "a", newline='') as fp: + with open(file, "w", newline='') as fp: if not file_exists: wr = csv.writer(fp, dialect='excel') wr.writerow(res_cols) diff --git a/stress/AC/Verify-AC.py b/stress/AC/Verify-AC.py index b550dcb..5105dd1 100644 --- a/stress/AC/Verify-AC.py +++ b/stress/AC/Verify-AC.py @@ -18,7 +18,7 @@ #print_metadata(df) # In[] -model_dir = './AC-Model/' +model_dir = './../models/adult' result_dir = './res/sex-' PARTITION_THRESHOLD = 6 diff --git a/stress/BM/Verify-BM.py b/stress/BM/Verify-BM.py index 33f24ee..bce8297 100644 --- a/stress/BM/Verify-BM.py +++ b/stress/BM/Verify-BM.py @@ -18,7 +18,7 @@ #print_metadata(df) # In[] -model_dir = './../BM-Model/' +model_dir = './../models/bank' result_dir = './age-' PARTITION_THRESHOLD = 10 diff --git a/targeted2/AC/Verify-AC.py b/targeted2/AC/Verify-AC.py index cd100e7..b27a096 100644 --- a/targeted2/AC/Verify-AC.py +++ b/targeted2/AC/Verify-AC.py @@ -68,7 +68,7 @@ if model_name == '': continue - model_funcs = 'utils.' + model_name + '-Model-Functions' + model_funcs = 'utils.' + 'Model-Functions' mod = import_module(model_funcs) layer_net = getattr(mod, 'layer_net') net = getattr(mod, 'net') diff --git a/targeted2/BM/Verify-BM.py b/targeted2/BM/Verify-BM.py index c1bd7af..91e9bc7 100644 --- a/targeted2/BM/Verify-BM.py +++ b/targeted2/BM/Verify-BM.py @@ -71,7 +71,7 @@ if model_name == '': continue - model_funcs = 'utils.' + model_name + '-Model-Functions' + model_funcs = 'utils.' + 'Model-Functions' mod = import_module(model_funcs) layer_net = getattr(mod, 'layer_net') net = getattr(mod, 'net') diff --git a/targeted2/GC/Verify-GC.py b/targeted2/GC/Verify-GC.py index 2aae1ab..511aa57 100644 --- a/targeted2/GC/Verify-GC.py +++ b/targeted2/GC/Verify-GC.py @@ -73,7 +73,7 @@ print('================== STARTING MODEL ' + model_file) model_name = model_file.split('.')[0] - model_funcs = 'utils.' + model_name + '-Model-Functions' + model_funcs = 'utils.' + 'Model-Functions' mod = import_module(model_funcs) layer_net = getattr(mod, 'layer_net') net = getattr(mod, 'net') diff --git a/utils/AC-1-Model-Functions.py b/utils/AC-1-Model-Functions.py deleted file mode 100644 index 7c6640b..0000000 --- a/utils/AC-1-Model-Functions.py +++ /dev/null @@ -1,48 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - x3 = w[2].T @ y2 + b[2] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x3 - -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - - for i in range(len(x)): - fl_x[i] = ToReal(x[i]) - - - x1 = w[0].T @ fl_x + b[0] - y1 = z3Relu(x1) - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - x3 = w[2].T @ y2 + b[2] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x3 \ No newline at end of file diff --git a/utils/AC-10-Model-Functions.py b/utils/AC-10-Model-Functions.py deleted file mode 100644 index 2fa05a2..0000000 --- a/utils/AC-10-Model-Functions.py +++ /dev/null @@ -1,101 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - return x5 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - return x5 - - - - diff --git a/utils/AC-11-Model-Functions.py b/utils/AC-11-Model-Functions.py deleted file mode 100644 index 2fa05a2..0000000 --- a/utils/AC-11-Model-Functions.py +++ /dev/null @@ -1,101 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - return x5 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - return x5 - - - - diff --git a/utils/AC-12-Model-Functions.py b/utils/AC-12-Model-Functions.py deleted file mode 100644 index 33cf9b1..0000000 --- a/utils/AC-12-Model-Functions.py +++ /dev/null @@ -1,131 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = relu(x5) - - x6 = w[5].T @ y5 + b[5] - y6 = relu(x6) - - x7 = w[6].T @ y6 + b[6] - y7 = relu(x7) - - x8 = w[7].T @ y7 + b[7] - y8 = relu(x8) - - x9 = w[8].T @ y8 + b[8] - y9 = relu(x9) - - x10 = w[9].T @ y9 + b[9] - return x10 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = z3Relu(x5) - - x6 = w[5].T @ y5 + b[5] - y6 = z3Relu(x6) - - x7 = w[6].T @ y6 + b[6] - y7 = z3Relu(x7) - - x8 = w[7].T @ y7 + b[7] - y8 = z3Relu(x8) - - x9 = w[8].T @ y8 + b[8] - y9 = z3Relu(x9) - - x10 = w[9].T @ y9 + b[9] - return x10 - - - - diff --git a/utils/AC-2-Model-Functions.py b/utils/AC-2-Model-Functions.py deleted file mode 100644 index f218308..0000000 --- a/utils/AC-2-Model-Functions.py +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 - -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - - for i in range(len(x)): - fl_x[i] = ToReal(x[i]) - - - x1 = w[0].T @ fl_x + b[0] - y1 = z3Relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 \ No newline at end of file diff --git a/utils/AC-3-Model-Functions.py b/utils/AC-3-Model-Functions.py deleted file mode 100644 index f218308..0000000 --- a/utils/AC-3-Model-Functions.py +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 - -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - - for i in range(len(x)): - fl_x[i] = ToReal(x[i]) - - - x1 = w[0].T @ fl_x + b[0] - y1 = z3Relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 \ No newline at end of file diff --git a/utils/AC-4-Model-Functions.py b/utils/AC-4-Model-Functions.py deleted file mode 100644 index 61e9009..0000000 --- a/utils/AC-4-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/AC-5-Model-Functions.py b/utils/AC-5-Model-Functions.py deleted file mode 100644 index 61e9009..0000000 --- a/utils/AC-5-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/AC-6-Model-Functions.py b/utils/AC-6-Model-Functions.py deleted file mode 100644 index 61e9009..0000000 --- a/utils/AC-6-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/AC-7-Model-Functions.py b/utils/AC-7-Model-Functions.py deleted file mode 100644 index 86dc8f7..0000000 --- a/utils/AC-7-Model-Functions.py +++ /dev/null @@ -1,110 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = relu(x5) - - x6 = w[5].T @ y5 + b[5] - # y6 = softmax(y1) - return x6 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = z3Relu(x5) - - x6 = w[5].T @ y5 + b[5] - - # y6 = softmax(y1) - return x6 - - - - diff --git a/utils/AC-8-Model-Functions.py b/utils/AC-8-Model-Functions.py deleted file mode 100644 index 82f3dec..0000000 --- a/utils/AC-8-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/AC-9-Model-Functions.py b/utils/AC-9-Model-Functions.py deleted file mode 100644 index 2fa05a2..0000000 --- a/utils/AC-9-Model-Functions.py +++ /dev/null @@ -1,101 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - return x5 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - return x5 - - - - diff --git a/utils/AC-A-Model-Functions.py b/utils/AC-A-Model-Functions.py deleted file mode 100644 index c6e80e0..0000000 --- a/utils/AC-A-Model-Functions.py +++ /dev/null @@ -1,109 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = relu(x5) - - x6 = w[5].T @ y5 + b[5] - # y6 = softmax(y1) - return x6 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(13)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = z3Relu(x5) - - x6 = w[5].T @ y5 + b[5] - # y6 = softmax(y1) - return x6 - - - - diff --git a/utils/BM-1-Model-Functions.py b/utils/BM-1-Model-Functions.py deleted file mode 100644 index 6be1434..0000000 --- a/utils/BM-1-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/BM-2-Model-Functions.py b/utils/BM-2-Model-Functions.py deleted file mode 100644 index 6be1434..0000000 --- a/utils/BM-2-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/BM-3-Model-Functions.py b/utils/BM-3-Model-Functions.py deleted file mode 100644 index 7e5d86d..0000000 --- a/utils/BM-3-Model-Functions.py +++ /dev/null @@ -1,86 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - # y6 = softmax(y1) - return x2 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - - # y6 = softmax(y1) - return x2 - - - - diff --git a/utils/BM-4-Model-Functions.py b/utils/BM-4-Model-Functions.py deleted file mode 100644 index 43961ff..0000000 --- a/utils/BM-4-Model-Functions.py +++ /dev/null @@ -1,98 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - # y6 = softmax(y1) - return x4 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - - # y6 = softmax(y1) - return x4 - - - - diff --git a/utils/BM-5-Model-Functions.py b/utils/BM-5-Model-Functions.py deleted file mode 100644 index 6be1434..0000000 --- a/utils/BM-5-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/BM-6-Model-Functions.py b/utils/BM-6-Model-Functions.py deleted file mode 100644 index 6be1434..0000000 --- a/utils/BM-6-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/BM-7-Model-Functions.py b/utils/BM-7-Model-Functions.py deleted file mode 100644 index 6be1434..0000000 --- a/utils/BM-7-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(16)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/BM-8-Model-Functions.py b/utils/BM-8-Model-Functions.py deleted file mode 100644 index 60ad74e..0000000 --- a/utils/BM-8-Model-Functions.py +++ /dev/null @@ -1,110 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = relu(x5) - - x6 = w[5].T @ y5 + b[5] - # y6 = softmax(y1) - return x6 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(16)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = z3Relu(x5) - - x6 = w[5].T @ y5 + b[5] - - # y6 = softmax(y1) - return x6 - - - - diff --git a/utils/GC-1-Model-Functions.py b/utils/GC-1-Model-Functions.py deleted file mode 100644 index 2588218..0000000 --- a/utils/GC-1-Model-Functions.py +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 - -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(20)]) - - for i in range(len(x)): - fl_x[i] = ToReal(x[i]) - - - x1 = w[0].T @ fl_x + b[0] - y1 = z3Relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 \ No newline at end of file diff --git a/utils/GC-3-Model-Functions.py b/utils/GC-3-Model-Functions.py deleted file mode 100644 index 2588218..0000000 --- a/utils/GC-3-Model-Functions.py +++ /dev/null @@ -1,44 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 - -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(20)]) - - for i in range(len(x)): - fl_x[i] = ToReal(x[i]) - - - x1 = w[0].T @ fl_x + b[0] - y1 = z3Relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 \ No newline at end of file diff --git a/utils/GC-4-Model-Functions.py b/utils/GC-4-Model-Functions.py deleted file mode 100644 index 4d3fcfe..0000000 --- a/utils/GC-4-Model-Functions.py +++ /dev/null @@ -1,92 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - # y6 = softmax(y1) - return x3 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(20)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - - # y6 = softmax(y1) - return x3 - - - - diff --git a/utils/GC-5-Model-Functions.py b/utils/GC-5-Model-Functions.py deleted file mode 100644 index e6d0644..0000000 --- a/utils/GC-5-Model-Functions.py +++ /dev/null @@ -1,110 +0,0 @@ -#!/usr/bin/env python3 -# -*- coding: utf-8 -*- - -# reinterpret network symbolically using z3 variables. -import sys -from z3 import * -import numpy as np -import pandas as pd -import collections -import time -import datetime - -from utils.verif_utils import * - - -def ground_net(x): - layer_outs = [] - for i in range(len(w)): - layer = [] - for j in range(len(w[i][0])): - sum = 0 - for k in range(len(x)): - sum += x[k] * w[i][k][j] - sum += b[i][j] - layer.append(sum) - layer = np.asarray(layer, dtype=np.float64) - y = layer if i == len(w)-1 else relu(layer) - layer_outs.append(y) - x = y - return y - - -def layer_net(x, w, b): - layers = [] - for i in range(len(w)): - x1 = w[i].T @ x + b[i] - y1 = x1 if i == len(w)-1 else relu(x1) - layers.append(y1) - x = y1 - return layers - -def net(x, w, b): -# for i in range(len(w)): -# x1 = w[i].T @ x + b[i] -# y1 = x1 if i == len(w)-1 else relu(x1) -# x = y1 - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = relu(x5) - - x6 = w[5].T @ y5 + b[5] - # y6 = softmax(y1) - return x6 - -#x = FP('x', FPSort(8, 24)) -#fl_x = np.array([FP('fl_x%s' % i, FPSort(8, 24)) for i in range(13)]) -def z3_net(x, w, b): - - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(20)]) - #fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - - - for i in range(len(x)): -# RealSort().cast(x) -# FPSort(8, 24).cast - - - #fl_x[i] = FPSort(8, 24).cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = Float32().cast(x[i]) # gives unsat quick. wrong by coersion - #fl_x[i] = RealSort().cast(x[i]) - - fl_x[i] = ToReal(x[i]) - - - - x1 = w[0].T @ fl_x + b[0] - #x1 = w[0].T @ x + b[0] - y1 = z3Relu(x1) - - x2 = w[1].T @ y1 + b[1] - y2 = z3Relu(x2) - - x3 = w[2].T @ y2 + b[2] - y3 = z3Relu(x3) - - x4 = w[3].T @ y3 + b[3] - y4 = z3Relu(x4) - - x5 = w[4].T @ y4 + b[4] - y5 = z3Relu(x5) - - x6 = w[5].T @ y5 + b[5] - - # y6 = softmax(y1) - return x6 - - - - diff --git a/utils/GC-2-Model-Functions.py b/utils/Model-Functions.py similarity index 68% rename from utils/GC-2-Model-Functions.py rename to utils/Model-Functions.py index 2588218..071a497 100644 --- a/utils/GC-2-Model-Functions.py +++ b/utils/Model-Functions.py @@ -23,22 +23,24 @@ def layer_net(x, w, b): return layers def net(x, w, b): - x1 = w[0].T @ x + b[0] - y1 = relu(x1) - x2 = w[1].T @ y1 + b[1] - # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 + return layer_net(x, w, b)[-1] def z3_net(x, w, b): - fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(20)]) + fl_x = np.array([FP('fl_x%s' % i, Float32()) for i in range(len(x))]) for i in range(len(x)): fl_x[i] = ToReal(x[i]) - x1 = w[0].T @ fl_x + b[0] - y1 = z3Relu(x1) - x2 = w[1].T @ y1 + b[1] + # x1 = w[0].T @ fl_x + b[0] + # y1 = z3Relu(x1) + # x2 = w[1].T @ y1 + b[1] + # y2 = z3Relu(x2) + # x3 = w[2].T @ y2 + b[2] + for i in range(len(w)): + x1 = w[i].T @ fl_x + b[i] + y1 = x1 if i == len(w)-1 else z3Relu(x1) + fl_x = y1 # y = 1 / (1 + math.exp(-x3)) # WP computer for sigmoid - return x2 \ No newline at end of file + return fl_x \ No newline at end of file diff --git a/utils/prune.py b/utils/prune.py index a0e4233..5e95121 100644 --- a/utils/prune.py +++ b/utils/prune.py @@ -1,4 +1,4 @@ -# -*- coding: utf-8 -*- +# -- coding: utf-8 -- import sys sys.path.append('../') @@ -24,39 +24,17 @@ def z3Relu(x): return np.vectorize(lambda y: If(y >= 0 , y, 0))(x) -def z3_layer1_ws_net(x, w, b): - fl_x = np.array([Real('fl_x%s' % i) for i in range(13)]) - for i in range(len(x)): - fl_x[i] = ToReal(x[i]) - x1 = w[0].T @ fl_x + b[0] - return x1 -def z3_layer2_ws_net(x, w, b): - x2 = w[1].T @ x + b[1] - return x2 -def z3_layer3_ws_net(x, w, b): - x3 = w[2].T @ x + b[2] - return x3 -def z3_layer4_ws_net(x, w, b): - x4 = w[3].T @ x + b[3] - return x4 -def z3_layer5_ws_net(x, w, b): - x5 = w[4].T @ x + b[4] - return x5 -def z3_layer6_ws_net(x, w, b): - x6 = w[5].T @ x + b[5] - return x6 -def z3_layer7_ws_net(x, w, b): - x7 = w[6].T @ x + b[6] - return x7 -def z3_layer8_ws_net(x, w, b): - x8 = w[7].T @ x + b[7] - return x8 -def z3_layer9_ws_net(x, w, b): - x9 = w[8].T @ x + b[8] - return x9 -def z3_layer9_ws_net(x, w, b): - x9 = w[8].T @ x + b[8] - return x9 + + +def z3_layer_ws_net(x, w, b, i): + fl_x = x + if i == 1: + print(type(x)) + fl_x = np.array([Real('fl_x%s' % it) for it in range(len(x))]) + for it in range(len(x)): + fl_x[it] = ToReal(x[it]) + xi = w[i - 1].T @ fl_x + b[i - 1] + return xi def z3_layer1_ws_net_german(x, w, b): fl_x = np.array([Real('fl_x%s' % i) for i in range(20)]) @@ -280,51 +258,17 @@ def singular_verification(cand, df, weight, bias, ranges, pl_lb, pl_ub): if candidates[layer_index][neuron_index] == 0: continue - if(layer_index == 0): + if (layer_index == 0): x = np.array([Int('x%s' % i) for i in range(len(weight[layer_index]))]) in_props = input_domain_constraint(df, x, ranges) - y = z3_layer1_ws_net(x, weight, bias) - - elif(layer_index == 1): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer2_ws_net(x, weight, bias) - - elif(layer_index == 2): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer3_ws_net(x, weight, bias) - - elif(layer_index == 3): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer4_ws_net(x, weight, bias) + y = z3_layer_ws_net(x, weight, bias, layer_index + 1) - elif(layer_index == 4): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer5_ws_net(x, weight, bias) - - elif(layer_index == 5): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer6_ws_net(x, weight, bias) - - elif(layer_index == 6): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer7_ws_net(x, weight, bias) - - elif(layer_index == 7): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer8_ws_net(x, weight, bias) - - elif(layer_index == 8): + else: x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer9_ws_net(x, weight, bias) + y = z3_layer_ws_net(x, weight, bias, layer_index + 1) + s = Solver() for i in in_props: @@ -340,12 +284,6 @@ def singular_verification(cand, df, weight, bias, ranges, pl_lb, pl_ub): else: dead_node_mask[layer_index][neuron_index] = 0 -# s.reset() -# for i in in_props: -# s.add(i) -# s.add(y[neuron_index] < 0) -# if res == unsat: -# print('ACTIVE: ', neuron_index) return dead_node_mask, candidates, count_finds/total_counts @@ -373,27 +311,12 @@ def singular_verification_german(cand, df, weight, bias, ranges, pl_lb, pl_ub): if(layer_index == 0): x = np.array([Int('x%s' % i) for i in range(len(weight[layer_index]))]) in_props = input_domain_constraint(df, x, ranges) - y = z3_layer1_ws_net_german(x, weight, bias) - - elif(layer_index == 1): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer2_ws_net(x, weight, bias) - - elif(layer_index == 2): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer3_ws_net(x, weight, bias) + y = z3_layer_ws_net(x, weight, bias, layer_index + 1) - elif(layer_index == 3): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer4_ws_net(x, weight, bias) - - elif(layer_index == 4): + else: x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer5_ws_net(x, weight, bias) + y = z3_layer_ws_net(x, weight, bias, layer_index + 1) s = Solver() @@ -443,27 +366,13 @@ def singular_verification_bank(cand, df, weight, bias, ranges, pl_lb, pl_ub): if(layer_index == 0): x = np.array([Int('x%s' % i) for i in range(len(weight[layer_index]))]) in_props = input_domain_constraint(df, x, ranges) - y = z3_layer1_ws_net_bank(x, weight, bias) + y = z3_layer_ws_net(x, weight, bias, layer_index + 1) - elif(layer_index == 1): + else: x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer2_ws_net(x, weight, bias) + y = z3_layer_ws_net(x, weight, bias, layer_index + 1) - elif(layer_index == 2): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer3_ws_net(x, weight, bias) - - elif(layer_index == 3): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer4_ws_net(x, weight, bias) - - elif(layer_index == 4): - x = np.array([Real('x%s' % i) for i in range(len(weight[layer_index]))]) - in_props = intermediate_domain_constraint(x, pl_lb, pl_ub, layer_index) - y = z3_layer5_ws_net(x, weight, bias) s = Solver() @@ -532,6 +441,9 @@ def sound_prune(df, weight, bias, simulation_size, layer_net, range_dict): b_dead_node_mask, b_candidates, b_compression = \ dead_node_from_bound(candidates, weight, bias, range_dict, ws_ub) + print(b_dead_node_mask) + for w in weight: + print(w.shape) for l in b_dead_node_mask: if not 0 in l: l[0] = 0 @@ -722,7 +634,7 @@ def prune_neurons(weight, bias, candidates): pr_w = copy.deepcopy(weight) pr_b = copy.deepcopy(bias) -# print('++++++++') +# \ print('++++++++') for i in range(len(weight)): # layer i # print(np.shape(weight[i])) @@ -744,5 +656,4 @@ def prune_neurons(weight, bias, candidates): # print(pr_w[0].shape) print('Pruning done!') - return pr_w, pr_b - + return pr_w, pr_b \ No newline at end of file diff --git a/utils/verif_utils.py b/utils/verif_utils.py index 5c66f90..c60fc06 100644 --- a/utils/verif_utils.py +++ b/utils/verif_utils.py @@ -186,7 +186,7 @@ def load_german(): 'foreign_worker', 'credit'] na_values=[] df = pd.read_csv(filepath, sep=' ', header=None, names=column_names,na_values=na_values) - df['age'] = df['age'].apply(lambda x: np.float(x >= 26)) + df['age'] = df['age'].apply(lambda x: np.float64(x >= 26)) df = german_custom_preprocessing(df) feat_to_drop = ['personal_status'] df = df.drop(feat_to_drop, axis=1) @@ -242,7 +242,7 @@ def load_bank(): df = dropped columns = ['education=Assoc-acdm', 'education=Assoc-voc', 'education=Bachelors',] - df['age'] = df['age'].apply(lambda x: np.float(x >= 25)) + df['age'] = df['age'].apply(lambda x: np.float64(x >= 25)) ## Feature selection # features_to_keep = []