Skip to content

Commit

Permalink
remove local robustness method
Browse files Browse the repository at this point in the history
  • Loading branch information
@wu-haoze
wu-haoze committed Aug 23, 2024
1 parent fbf6a10 commit 5b25902
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 202 deletions.
79 changes: 1 addition & 78 deletions maraboupy/MarabouNetwork.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ def calculateBounds(self, filename="", verbose=True, options=None):
if options == None:
options = MarabouCore.Options()
exitCode, bounds, stats = MarabouCore.calculateBounds(ipq, options, str(filename))

if verbose:
print(exitCode)
if exitCode == "":
Expand All @@ -115,83 +115,6 @@ def calculateBounds(self, filename="", verbose=True, options=None):

return [exitCode, bounds, stats]

def evaluateLocalRobustness(self, input, epsilon, originalClass, verbose=True, options=None, targetClass=None):
"""Function evaluating a specific input is a local robustness within the scope of epslion
Args:
input (numpy.ndarray): Target input
epsilon (float): L-inf norm of purturbation
originalClass (int): Output class of a target input
verbose (bool): If true, print out solution after solve finishes
options (:class:`~maraboupy.MarabouCore.Options`): Object for specifying Marabou options, defaults to None
targetClass (int): If set, find a feasible solution with which the value of targetClass is max within outputs.
Returns:
(tuple): tuple containing:
- vals (Dict[int, float]): Empty dictionary if UNSAT, otherwise a dictionary of SATisfying values for variables
- stats (:class:`~maraboupy.MarabouCore.Statistics`): A Statistics object to how Marabou performed
- maxClass (int): Output class which value is max within outputs if SAT.
"""
assert(type(self.inputVars) is list)
if (len(self.inputVars) != 1):
raise NotImplementedError("Operation for %d inputs is not implemented" % len(self.inputVars))
inputVars = self.inputVars[0][0]

if inputVars.shape != input.shape:
raise RuntimeError("Input shape of the model should be same as the input shape\n input shape of the model: {0}, shape of the input: {1}".format(inputVars.shape, input.shape))

assert(type(self.outputVars) is list)
if (len(self.outputVars) != 1):
raise NotImplementedError("Operation for %d outputs is not implemented" % len(self.outputVars))

if options == None:
options = MarabouCore.Options()

# Add constratins to all input nodes
flattenInputVars = inputVars.flatten()
flattenInput = input.flatten()
for i in range(flattenInput.size):
self.setLowerBound(flattenInputVars[i], flattenInput[i] - epsilon)
self.setUpperBound(flattenInputVars[i], flattenInput[i] + epsilon)

maxClass = None
outputStartIndex = self.outputVars[0][0][0]

if targetClass is None:
outputLayerSize = len(self.outputVars[0][0])
# loop for all of output classes except for original class
for outputLayerIndex in range(outputLayerSize):
if outputLayerIndex != originalClass:
self.addMaxConstraint(set([outputStartIndex + outputLayerIndex, outputStartIndex + originalClass]),
outputStartIndex + outputLayerIndex)
exitCode, vals, stats = self.solve(options = options)
if (stats.hasTimedOut()):
break
elif (len(vals) > 0):
maxClass = outputLayerIndex
break
else:
self.addMaxConstraint(set(self.outputVars[0][0]), outputStartIndex + targetClass)
exitCode, vals, stats = self.solve(options = options)
if verbose:
if not stats.hasTimedOut() and len(vals) > 0:
maxClass = targetClass

# print timeout, or feasible inputs and outputs if verbose is on.
if verbose:
if stats.hasTimedOut():
print("TO")
elif len(vals) > 0:
print("sat")
for j in range(len(self.inputVars[0])):
for i in range(self.inputVars[0][j].size):
print("input {} = {}".format(i, vals[self.inputVars[0][j].item(i)]))

for j in range(len(self.outputVars[0])):
for i in range(self.outputVars[0][j].size):
print("output {} = {}".format(i, vals[self.outputVars[0][j].item(i)]))

return [vals, stats, maxClass]

def evaluateWithMarabou(self, inputValues, filename="evaluateWithMarabou.log", options=None):
"""Function to evaluate network at a given point using Marabou as solver
Expand Down
124 changes: 0 additions & 124 deletions maraboupy/test/test_network.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -579,130 +579,6 @@ def test_resize():
for l in range(len(outputVars[i][j][k])):
assert abs(vals[outputVars[i][j][k][l]] - expectedOutputValues[i][j][k][l]) < TOL

def test_local_robustness_unsat():
"""
Tests local robustness of an nnet network. (UNSAT)
"""
filename = "fc_2-2-3.nnet"

network = loadNetwork(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, 0])
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=0.1, originalClass=0, options=options, targetClass=None)

# should be local robustness
assert(len(vals) == 0)

def test_local_robustness_sat():
"""
Tests local robustness of an nnet network. (SAT)
"""
filename = "fc_2-2-3.nnet"

network = loadNetwork(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, -2])
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=0.1, originalClass=0, options=options, targetClass=None)

# should be not local robustness
assert(len(vals) > 0)

def test_local_robustness_unsat_no_opt():
"""
Tests local robustness of an nnet network. (UNSAT)
"""
filename = "fc_2-2-3.nnet"

network = loadNetwork(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, 0])
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=0.1, originalClass=0, targetClass=None)

# should be local robustness
assert(len(vals) == 0)

def test_local_robustness_sat_no_opt():
"""
Tests local robustness of an nnet network. (SAT)
"""
filename = "fc_2-2-3.nnet"

network = loadNetwork(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, -2])
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=0.1, originalClass=0, targetClass=None)

# should be not local robustness
assert(len(vals) > 0)

def test_local_robustness_unsat_of_onnx():
"""
Tests local robustness of an onnx network. (UNSAT)
"""
filename = "fc_2-2-3.onnx"

network = loadNetworkInONNX(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, 0])
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=0.1, originalClass=0, options=options, targetClass=None)

# should be local robustness
assert(len(vals) == 0)

def test_local_robustness_sat_of_onnx():
"""
Tests local robustness of an onnx network. (SAT)
"""
filename = "fc_2-2-3.onnx"

network = loadNetworkInONNX(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, 0])
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=1.0, originalClass=0, options=options, targetClass=None)

# should be not local robustness
assert(len(vals) > 0)

def test_local_robustness_sat_with_target_class():
"""
Tests local robustness of an onnx network. (SAT)
"""
filename = "fc_2-2-3.onnx"

network = loadNetworkInONNX(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.array([1, -2])
targetClass = 1
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=0.1, originalClass=0, options=options, targetClass=targetClass)

# should be not local robustness
assert(len(vals) > 0)

# maxClass should be equal to targetClass
assert(maxClass == targetClass)

def test_local_robustness_sat_of_onnx_3D():
"""
Tests local robustness of an onnx network which input's dimension is 3. (SAT)
"""
filename = "KJ_TinyTaxiNet.onnx"

network = loadNetworkInONNX(filename)
options = Marabou.createOptions(verbosity = 0)

input = np.ones([8, 16, 1]) * 0.5
vals, stats, maxClass = network.evaluateLocalRobustness(input=input, epsilon=1.0, originalClass=0, options=options, targetClass=None)

# should be not local robustness
assert(len(vals) > 0)

def test_calculate_bounds():
"""
Tests calculate bounds of an onnx network
Expand Down

0 comments on commit 5b25902

Please sign in to comment.