Skip to content

Commit

Permalink
Add files via upload
Browse files Browse the repository at this point in the history
  • Loading branch information
Sumon Biswas authored Dec 9, 2022
1 parent a093f4d commit f70c12d
Show file tree
Hide file tree
Showing 68 changed files with 115,622 additions and 0 deletions.
26 changes: 26 additions & 0 deletions relaxed/AC-result.csv
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
,Partition_ID,SAT_count,UNSAT_count,UNK_count,h_attempt,h_success,ST_compression,H_compression,SV-time,HV-Time,Total-Time
0,210,47,157,6,13,7,0.791047619,0.005333333,12.46009048,4.577452381,17.167
4,74,20,45,9,14,5,0.906217568,0.002943243,33.93127027,14.51856757,48.74918919
5,124,84,35,5,10,5,0.827946774,0.002845161,23.55504839,5.977879032,29.71540323
6,30,13,5,12,16,4,0.90015,0.0297,65.263,48.2012,120.9156667
7,27,11,3,13,16,3,0.86707037,0.015225926,78.56551852,54.18792593,134.2951852
8,117,47,56,14,17,3,0.712820513,0.007179487,19.66211966,12.43119658,32.22102564
9,44,0,31,13,19,6,0.748,0.036,52.08634091,31.17302273,84.47340909
10,402,182,220,0,3,3,0.346200746,0.000226119,8.664828358,0.204554726,8.981094527
11,4811,1294,3517,0,3,3,0.259099418,0,0.62212513,0.015874039,0.74860528
1,164,34,128,2,11,9,0.416094512,0.004645122,19.3667622,3.5445,23.05829268
2,18,0,0,18,18,0,0.185644444,0.031177778,100.1774444,100.2556111,200.8777778
3,53,1,36,16,18,2,0.402786792,0.010241509,37.08790566,31.99898113,69.34264151
,,,,,,,,,,,
12,216,9,193,14,17,3,0.784814815,0.006111111,9.694439815,7.051875,16.88675926
16,75,8,55,12,14,2,0.88846,0.006996,31.0968,17.94189333,49.5652
17,129,34,86,9,13,4,0.813632558,0.003494574,18.94053488,8.731310078,27.92116279
18,41,5,22,14,16,2,0.899390244,0.022939024,44.69692683,36.2724878,91.49804878
19,37,3,18,16,17,1,0.861727027,0.015513514,51.45454054,43.95527027,97.87513514
20,177,28,133,16,17,1,0.710282486,0.005649718,11.60489266,9.084542373,20.83762712
21,66,0,53,13,17,4,0.747636364,0.021333333,32.74569697,20.89736364,55.24939394
22,639,218,418,3,6,3,0.352230516,0.000142254,4.983474178,0.569051643,5.674757433
23,3991,483,3508,0,2,2,0.261200927,0,0.777612378,0.008530193,0.902861438
13,216,19,192,5,15,10,0.416235648,0.00396713,13.70964815,3.6965,17.55435185
14,31,0,13,18,18,0,0.176245161,0.011806452,58.18019355,58.14322581,116.8190323
15,123,0,107,16,17,1,0.432833333,0.005121951,16.09786179,13.06808943,29.4303252
317 changes: 317 additions & 0 deletions relaxed/AC/Verify-AC.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,317 @@
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
import sys
sys.path.append('../../')

from random import shuffle
from z3 import *
from utils.input_partition import *
from utils.verif_utils import *
from utils.prune import *
from importlib import import_module

# In[]

df, X_train, y_train, X_test, y_test = load_adult_ac1()
X = np.r_[X_train, X_test]
single_input = X_test[0].reshape(1, 13)
#print_metadata(df)

# In[]
model_dir = '../../models/adult/'
result_dir = './res/age-'
PARTITION_THRESHOLD = 6

SOFT_TIMEOUT = 100
HARD_TIMEOUT = 1*60*60
HEURISTIC_PRUNE_THRESHOLD = 20

# In[]
## Domain
default_range = [0, 1]
range_dict = {}
range_dict['age'] = [10, 100]
range_dict['workclass'] = [0, 6]
range_dict['education'] = [0, 15]
range_dict['education-num'] = [1, 16]
range_dict['marital-status'] = [0, 6]
range_dict['occupation'] = [0, 13]
range_dict['relationship'] = [0, 5]
range_dict['race'] = [0, 4]
range_dict['sex'] = [0, 1]
range_dict['capital-gain'] = [0, 19]
range_dict['capital-loss'] = [0, 19]
range_dict['hours-per-week'] = [1, 100]
range_dict['native-country'] = [0, 40]

A = range_dict.keys()
PA = ['race']

RA = ['age']
RA_threshold = 5

sim_size = 1 * 1000

p_dict = partition(range_dict, PARTITION_THRESHOLD)
p_list = partitioned_ranges(A, PA, p_dict, range_dict)
print('Number of partitions: ', len(p_list))
shuffle(p_list)

# In[]

model_files = os.listdir(model_dir)
for model_file in model_files:
if not model_file.endswith('.h5'):
continue;
print('================== STARTING MODEL ' + model_file)
model_name = model_file.split('.')[0]
if model_name == '':
continue

model_funcs = 'utils.' + model_name + '-Model-Functions'
mod = import_module(model_funcs)
layer_net = getattr(mod, 'layer_net')
net = getattr(mod, 'net')
z3_net = getattr(mod, 'z3_net')

w = []
b = []

model = load_model(model_dir + model_file)

for i in range(len(model.layers)):
w.append(model.layers[i].get_weights()[0])
b.append(model.layers[i].get_weights()[1])

print('###################')
partition_id = 0
sat_count = 0
unsat_count = 0
unk_count = 0
cumulative_time = 0

for p in p_list:
heuristic_attempted = 0
result = []
start_time = time.time()

partition_id += 1
simulation_size = 1*1000


# In[]
# sd = s
neuron_bounds, candidates, s_candidates, b_deads, s_deads, st_deads, pos_prob, sim_X_df = \
sound_prune(df, w, b, simulation_size, layer_net, p)

b_compression = compression_ratio(b_deads)
s_compression = compression_ratio(s_deads)
st_compression = compression_ratio(st_deads)

pr_w, pr_b = prune_neurons(w, b, st_deads)


# In[]
# Create properties
in_props = []
out_props = []

x = np.array([Int('x%s' % i) for i in range(13)])
x_ = np.array([Int('x_%s' % i) for i in range(13)])

y = z3_net(x, pr_w, pr_b) # y is an array of size 1
y_ = z3_net(x_, pr_w, pr_b)

# Basic fairness property - must include
for attr in A:
if(attr in PA):
in_props.extend(in_const_adult(df, x, attr, 'neq', x_))
elif(attr in RA):
in_props.extend(in_const_diff_adult(df, x, x_, attr, RA_threshold))
else:
in_props.extend(in_const_adult(df, x, attr, 'eq', x_))

in_props.extend(in_const_domain_adult(df, x, x_, p, PA))

# In[]
s = Solver()
#s.reset()

if(len(sys.argv) > 1):
s.set("timeout", int(sys.argv[1]) * 1000) # X seconds
else:
s.set("timeout", SOFT_TIMEOUT * 1000)


for i in in_props:
s.add(i)

s.add(Or(And(y[0] < 0, y_[0] > 0), And(y[0] > 0, y_[0] < 0)))

print('Verifying ...')
res = s.check()

print(res)
if res == sat:
m = s.model()
inp1, inp2 = parse_z3Model(m)

sv_time = s.statistics().time
s_end_time = time.time()
s_time = compute_time(start_time, s_end_time)
hv_time = 0
# In[]
h_compression = 0
t_compression = st_compression
h_success = 0
if res == unknown:
heuristic_attempted = 1

h_deads, deads = heuristic_prune(neuron_bounds, candidates,
s_candidates, st_deads, pos_prob, HEURISTIC_PRUNE_THRESHOLD, w, b)

del pr_w
del pr_b

pr_w, pr_b = prune_neurons(w, b, deads)
h_compression = compression_ratio(h_deads)
print(round(h_compression*100, 2), '% HEURISTIC PRUNING')
t_compression = compression_ratio(deads)
print(round(t_compression*100, 2), '% TOTAL PRUNING')

y = z3_net(x, pr_w, pr_b) # y is an array of size 1
y_ = z3_net(x_, pr_w, pr_b)

s = Solver()

if(len(sys.argv) > 1):
s.set("timeout", int(sys.argv[1]) * 1000) # X seconds
else:
s.set("timeout", SOFT_TIMEOUT * 1000)

for i in in_props:
s.add(i)

s.add(Or(And(y[0] < 0, y_[0] > 0), And(y[0] > 0, y_[0] < 0)))
print('Verifying ...')
res = s.check()

print(res)
if res == sat:
m = s.model()
inp1, inp2 = parse_z3Model(m)

if res != unknown:
h_success = 1
hv_time = s.statistics().time

# In[]
h_time = compute_time(s_end_time, time.time())
total_time = compute_time(start_time, time.time())

cumulative_time += total_time

# In[]
print('V time: ', s.statistics().time)
file = result_dir + model_name + '.csv'

# In[]
c_check_correct = 0
accurate = 0
d1 = ''
d2 = ''
if res == sat:
sat_count += 1
d1 = np.asarray(inp1, dtype=np.float32)
d2 = np.asarray(inp2, dtype=np.float32)
print(inp1)
print(inp2)
res1 = net(d1, pr_w, pr_b)
res2 = net(d2, pr_w, pr_b)
print(res1, res2)
pred1 = sigmoid(res1)
pred2 = sigmoid(res2)
class_1 = pred1 > 0.5
class_2 = pred2 > 0.5

res1_orig = net(d1, w, b)
res2_orig = net(d2, w, b)
print(res1_orig, res2_orig)
pred1_orig = sigmoid(res1_orig)
pred2_orig = sigmoid(res2_orig)
class_1_orig = pred1_orig > 0.5
class_2_orig = pred2_orig > 0.5

if class_1_orig != class_2_orig:
accurate = 1
if class_1 == class_1_orig and class_2 == class_2_orig:
c_check_correct = 1
elif res == unsat:
unsat_count += 1
else:
unk_count +=1


d = X_test[0]
res1 = net(d, pr_w, pr_b)
pred1 = sigmoid(res1)
class_1 = pred1 > 0.5

res1_orig = net(d, w, b)
pred1_orig = sigmoid(res1_orig)
class_1_orig = pred1_orig > 0.5

sim_X = sim_X_df.to_numpy()
sim_y_orig = get_y_pred(net, w, b, sim_X)
sim_y = get_y_pred(net, pr_w, pr_b, sim_X)


orig_acc = accuracy_score(y_test, get_y_pred(net, w, b, X_test))
pruned_acc = accuracy_score(sim_y_orig, sim_y)

# In[]
res_cols = ['Partition_ID', 'Verification', 'SAT_count', 'UNSAT_count', 'UNK_count', 'h_attempt', 'h_success', \
'B_compression', 'S_compression', 'ST_compression', 'H_compression', 'T_compression', 'SV-time', 'S-time', 'HV-Time', 'H-Time', 'Total-Time', 'C-check',\
'V-accurate', 'Original-acc', 'Pruned-acc', 'Acc-dec', 'C1', 'C2']

result.append(partition_id)
result.append(str(res))
result.append(sat_count)
result.append(unsat_count)
result.append(unk_count)
result.append(heuristic_attempted)
result.append(h_success)
result.append(round(b_compression, 4))
result.append(round(s_compression, 4))
result.append(round(st_compression, 4))
result.append(round(h_compression, 4))
result.append(round(t_compression, 4))
result.append(sv_time)
result.append(s_time)
result.append(hv_time)
result.append(h_time)
result.append(total_time)
result.append(c_check_correct)
result.append(accurate)
result.append(round(orig_acc, 4))
result.append(round(pruned_acc, 4))
result.append('-')
#result.append(round(orig_acc - pruned_acc, 4))
result.append(d1)
result.append(d2)


import csv
file_exists = os.path.isfile(file)
with open(file, "a", newline='') as fp:
if not file_exists:
wr = csv.writer(fp, dialect='excel')
wr.writerow(res_cols)

wr = csv.writer(fp)
wr.writerow(result)
print('******************')

if(cumulative_time > HARD_TIMEOUT):
print('================== COMPLETED MODEL ' + model_file)
break
Loading

0 comments on commit f70c12d

Please sign in to comment.