MarabouNetworkTF

Top contributors (to current version):

  • Kyle Julian

  • Christopher Lazarus

  • Shantanu Thakoor

  • Chelsea Sidrane

This file is part of the Marabou project. Copyright (c) 2017-2019 by the authors listed in the file AUTHORS in the top-level source directory) and their institutional affiliations. All rights reserved. See the file COPYING in the top-level source directory for licensing information.

MarabouNetworkTF represents neural networks with piecewise linear constraints derived from tensorflow formats

class maraboupy.MarabouNetworkTF.MarabouNetworkTF(filename, inputNames=None, outputName=None, modelType='frozen', savedModelTags=[])[source]

Bases: maraboupy.MarabouNetwork.MarabouNetwork

Constructs a MarabouNetworkTF object from a frozen Tensorflow protobuf or SavedModel

Parameters

  • filename (str) – Path to tensorflow network

  • inputNames (list of str, optional) – List of operation names corresponding to inputs

  • outputName (str, optional) – Name of operation corresponding to output

  • modelType (str, optional) – Type of model to read. The default is “frozen” for a frozen graph. Can also use “savedModel_v1” or “savedModel_v2” for the SavedModel format created from either tensorflow versions 1.X or 2.X respectively.

  • savedModelTags (list of str, optional) – If loading a SavedModel, the user must specify tags used, default is []

addAbsConstraint(b, f)[source]

Function to add a new Abs constraint

Parameters

  • b (int) – Variable representing input of the Abs constraint

  • f (int) – Variable representing output of the Abs constraint

addDisjunctionConstraint(disjuncts)[source]

Function to add a new Disjunction constraint

Parameters

disjuncts (list of list of Equations) – Each inner list represents a disjunct

addEquality(vars, coeffs, scalar)[source]

Function to add equality constraint to network

\[\sum_i vars_i * coeffs_i = scalar\]
Parameters

  • vars (list of int) – Variable numbers

  • coeffs (list of float) – Coefficients

  • scalar (float) – Right hand side constant of equation

addEquation(x)[source]

Function to add new equation to the network

Parameters

x (Equation) – New equation to add

addInequality(vars, coeffs, scalar)[source]

Function to add inequality constraint to network

\[\sum_i vars_i * coeffs_i \le scalar\]
Parameters

  • vars (list of int) – Variable numbers

  • coeffs (list of float) – Coefficients

  • scalar (float) – Right hand side constant of inequality

addMaxConstraint(elements, v)[source]

Function to add a new Max constraint

Parameters

  • elements (set of int) – Variable representing input to max constraint

  • v (int) – Variable representing output of max constraint

addRelu(v1, v2)[source]

Function to add a new Relu constraint

Parameters

  • v1 (int) – Variable representing input of Relu

  • v2 (int) – Variable representing output of Relu

addSignConstraint(b, f)[source]

Function to add a new Sign constraint

Parameters

  • b (int) – Variable representing input of Sign

  • f (int) – Variable representing output of Sign

clear()[source]

Reset values to represent empty network

evaluate(inputValues, useMarabou=True, options=None, filename='evaluateWithMarabou.log')[source]

Function to evaluate network at a given point

Parameters

  • inputValues (list of np arrays) – Inputs to evaluate

  • useMarabou (bool) – Whether to use Marabou solver or TF/ONNX, defaults to True

  • options (Options) – Object for specifying Marabou options, defaults to None

  • filename (str) – Path to redirect output if using Marabou solver, defaults to “evaluateWithMarabou.log”

Returns

Values representing the output of the network or None if output cannot be computed

Return type

(np array)

evaluateWithMarabou(inputValues, filename='evaluateWithMarabou.log', options=None)[source]

Function to evaluate network at a given point using Marabou as solver

Parameters

  • inputValues (list of np arrays) – Inputs to evaluate

  • filename (str) – Path to redirect output if using Marabou solver, defaults to “evaluateWithMarabou.log”

  • options (Options) – Object for specifying Marabou options, defaults to None

Returns

Values representing the output of the network or None if system is UNSAT

Return type

(np array)

evaluateWithoutMarabou(inputValues)[source]

Function to evaluate network at a given point using Tensorflow

Parameters

inputValues – (list of np arrays) representing inputs to network

Returns

(np array) representing output of network

Return type

outputValues

findError(inputValues, options=None, filename='evaluateWithMarabou.log')[source]

Function to find error between Marabou solver and TF/Nnet at a given point

Parameters

  • inputValues (list of np arrays) – Input values to evaluate

  • options (Options) –

  • filename (str) – Path to redirect output if using Marabou solver, defaults to “evaluateWithMarabou.log”

Returns

Values representing the error in each output variable

Return type

(np array)

getMarabouQuery()[source]

Function to convert network into Marabou InputQuery

Returns

InputQuery

lowerBoundExists(x)[source]

Function to check whether lower bound for a variable is known

Parameters

x (int) – Variable to check

readTF(filename, inputNames, outputName, modelType, savedModelTags)[source]

Read a tensorflow file to create a MarabouNetworkTF object

Parameters

  • filename (str) – Path to tensorflow network

  • inputNames (list of str, optional) – List of operation names corresponding to inputs

  • outputName (str, optional) – Name of operation corresponding to output

  • modelType (str, optional) – Type of model to read. The default is “frozen” for a frozen graph. Can also use “savedModel_v1” or “savedModel_v2” for the SavedModel format created from either tensorflow versions 1.X or 2.X respectively.

  • savedModelTags (list of str, optional) – If loading a SavedModel, the user must specify tags used, default is []

saveQuery(filename='')[source]

Serializes the inputQuery in the given filename

Parameters

filename – (string) file to write serialized inputQuery

setLowerBound(x, v)[source]

Function to set lower bound for variable

Parameters

  • x (int) – Variable number to set

  • v (float) – Value representing lower bound

setUpperBound(x, v)[source]

Function to set upper bound for variable

Parameters

  • x (int) – Variable number to set

  • v (float) – Value representing upper bound

solve(filename='', verbose=True, options=None)[source]

Function to solve query represented by this network

Parameters

  • filename (string) – Path for redirecting output

  • verbose (bool) – If true, print out solution after solve finishes

  • options (Options) – Object for specifying Marabou options, defaults to None

Returns

tuple containing:

  • vals (Dict[int, float]): Empty dictionary if UNSAT, otherwise a dictionary of SATisfying values for variables

  • stats (Statistics): A Statistics object to how Marabou performed

Return type

(tuple)

upperBoundExists(x)[source]

Function to check whether upper bound for a variable is known

Parameters

x (int) – Variable to check