Leaky relu

CHANGELOG.md

@@ -1,12 +1,13 @@
 # Changelog
 
 ## Next Release
-* Added support for onnx networks with tanh nodes to command-line interface.
+* Added support for onnx networks with tanh nodes to command-line interface
 * Added proof producing versions of Sign, Max, Absolute Value and Disjunction constraints
-* Added support for properties provided in VNN-LIB format for ONNX networks via the Python API.
+* Added support for properties provided in VNN-LIB format for ONNX networks via the Python API
 * Supported additional non-linear constraints Softmax and Bilinear
 * Removed dependency on torch and drop support for Python3.7
-* Bump ONNX version to >= 1.15.0
+* Bumped ONNX version to >= 1.15.0
+* Added support for Leaky ReLU
 
 ## Version 1.0.0
 * Initial versioned release

CMakeLists.txt

@@ -85,7 +85,7 @@ if (NOT ${Boost_FOUND})
   # bash file that downloads and install boost 1_80_0, the name need to match
   # BOOST_DIR variable
   execute_process(COMMAND ${TOOLS_DIR}/download_boost.${SCRIPT_EXTENSION})
-  find_package(Boost REQUIRED COMPONENTS program_options timer chrono thread)
+  find_package(Boost 1.80.0 REQUIRED COMPONENTS program_options timer chrono thread)
 endif()
 set(LIBS_INCLUDES ${Boost_INCLUDE_DIRS})
 list(APPEND LIBS ${Boost_LIBRARIES})

maraboupy/Marabou.py

@@ -28,7 +28,7 @@
 try:
     from maraboupy.MarabouNetworkONNX import *
 except ImportError:
-    warnings.warn("ONNX parser is unavailable because onnx or onnxruntime packages are not installed")
+    warnings.warn("ONNX parser is unavailable because onnx or onnxruntime or torch packages are not installed")
 
 def read_nnet(filename, normalize=False):
     """Constructs a MarabouNetworkNnet object from a .nnet file

maraboupy/MarabouCore.cpp

@@ -33,6 +33,7 @@
 #include "Engine.h"
 #include "FloatUtils.h"
 #include "InputQuery.h"
+#include "LeakyReluConstraint.h"
 #include "MarabouError.h"
 #include "InputParserError.h"
 #include "MString.h"
@@ -104,6 +105,11 @@ void restoreOutputStream(int outputStream)
     close(outputStream);
 }
 
+void addLeakyReluConstraint(InputQuery& ipq, unsigned var1, unsigned var2, double slope){
+    PiecewiseLinearConstraint* r = new LeakyReluConstraint(var1, var2, slope);
+    ipq.addPiecewiseLinearConstraint(r);
+}
+
 void addReluConstraint(InputQuery& ipq, unsigned var1, unsigned var2){
     PiecewiseLinearConstraint* r = new ReluConstraint(var1, var2);
     ipq.addPiecewiseLinearConstraint(r);
@@ -601,6 +607,16 @@ PYBIND11_MODULE(MarabouCore, m) {
             :class:`~maraboupy.MarabouCore.InputQuery`
         )pbdoc",
         py::arg("filename"));
+    m.def("addLeakyReluConstraint", &addLeakyReluConstraint, R"pbdoc(
+        Add a Relu constraint to the InputQuery
+
+        Args:
+            inputQuery (:class:`~maraboupy.MarabouCore.InputQuery`): Marabou input query to be solved
+            var1 (int): Input variable to Leaky ReLU constraint
+            var2 (int): Output variable to Leaky ReLU constraint
+            slope (float): Slope of the Leaky ReLU constraint
+        )pbdoc",
+          py::arg("inputQuery"), py::arg("var1"), py::arg("var2"), py::arg("slope"));
     m.def("addReluConstraint", &addReluConstraint, R"pbdoc(
         Add a Relu constraint to the InputQuery
 

maraboupy/MarabouNetwork.py

@@ -5,7 +5,7 @@
     - Andrew Wu
     - Kyle Julian
     - Teruhiro Tagomori
-    
+
 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.
@@ -23,11 +23,12 @@
 
 class MarabouNetwork:
     """Abstract class representing general Marabou network
-    
+
     Attributes:
         numVars (int): Total number of variables to represent network
         equList (list of :class:`~maraboupy.MarabouUtils.Equation`): Network equations
         reluList (list of tuples): List of relu constraint tuples, where each tuple contains the backward and forward variables
+        leakyReluList (list of tuples): List of leaky relu constraint tuples, where each tuple contains the backward and forward variables, and the slope
         sigmoidList (list of tuples): List of sigmoid constraint tuples, where each tuple contains the backward and forward variables
         maxList (list of tuples): List of max constraint tuples, where each tuple conatins the set of input variables and output variable
         absList (list of tuples): List of abs constraint tuples, where each tuple conatins the input variable and the output variable
@@ -49,6 +50,7 @@ def clear(self):
         self.equList = []
         self.additionalEquList = [] # used to store user defined equations
         self.reluList = []
+        self.leakyReluList = []
         self.sigmoidList = []
         self.maxList = []
         self.softmaxList = []
@@ -118,6 +120,16 @@ def addRelu(self, v1, v2):
         """
         self.reluList += [(v1, v2)]
 
+    def addLeakyRelu(self, v1, v2, slope):
+        """Function to add a new Leaky Relu constraint
+
+        Args:
+            v1 (int): Variable representing input of Leaky Relu
+            v2 (int): Variable representing output of Leaky Relu
+            slope (float): Shope of the Leaky ReLU
+        """
+        self.leakyReluList += [(v1, v2, slope)]
+
     def addBilinear(self, v1, v2, v3):
         """Function to add a bilinear constraint to the network
         Args:
@@ -275,6 +287,11 @@ def getMarabouQuery(self):
             assert r[1] < self.numVars and r[0] < self.numVars
             MarabouCore.addReluConstraint(ipq, r[0], r[1])
 
+        for r in self.leakyReluList:
+            assert r[1] < self.numVars and r[0] < self.numVars
+            assert(r[2] > 0 and r[2] < 1)
+            MarabouCore.addLeakyReluConstraint(ipq, r[0], r[1], r[2])
+
         for r in self.bilinearList:
             assert r[2] < self.numVars and r[1] < self.numVars and r[0] < self.numVars
             MarabouCore.addBilinearConstraint(ipq, r[0], r[1], r[2])
@@ -323,7 +340,7 @@ def getMarabouQuery(self):
         for u in self.upperBounds:
             assert u < self.numVars
             ipq.setUpperBound(u, self.upperBounds[u])
-            
+
         return ipq
 
     def solve(self, filename="", verbose=True, options=None, propertyFilename=""):

maraboupy/MarabouNetworkONNX.py

@@ -278,6 +278,8 @@ def makeMarabouEquations(self, nodeName, makeEquations):
             self.resizeEquations(node, makeEquations)
         elif node.op_type == 'Tanh':
             self.tanhEquations(node, makeEquations)
+        elif node.op_type == 'LeakyRelu':
+            self.leakyReluEquations(node, makeEquations)
         elif node.op_type == 'Softmax':
             self.softmaxEquations(node, makeEquations)
         elif node.op_type == 'Sub':
@@ -1259,6 +1261,28 @@ def reluEquations(self, node, makeEquations):
         for f in outputVars:
             self.setLowerBound(f, 0.0)
 
+    def leakyReluEquations(self, node, makeEquations):
+        """Function to generate equations corresponding to pointwise LeakyRelu
+        Args:
+            node (node): ONNX node representing the LeakyRelu operation
+            makeEquations (bool): True if we need to create new variables and add new LeakyRelus
+        :meta private:
+        """
+        nodeName = node.output[0]
+        inputName = node.input[0]
+        self.shapeMap[nodeName] = self.shapeMap[inputName]
+        if not makeEquations:
+            return
+
+        # Get variables
+        inputVars = self.varMap[inputName].reshape(-1)
+        outputVars = self.makeNewVariables(nodeName).reshape(-1)
+        assert len(inputVars) == len(outputVars)
+
+        # Generate equations
+        for i in range(len(inputVars)):
+            self.addLeakyRelu(inputVars[i], outputVars[i], 0.1)
+
     def subEquations(self, node, makeEquations):
         """Function to generate equations corresponding to subtraction
 
@@ -1417,6 +1441,10 @@ def reassignOutputVariables(self):
         for i, variables in enumerate(self.reluList):
             self.reluList[i] = tuple([self.reassignVariable(var, numInVars, outVars, newOutVars) for var in variables])
 
+        # Adjust relu list
+        for i, variables in enumerate(self.leakyReluList):
+            self.leakyReluList[i] = tuple([self.reassignVariable(var, numInVars, outVars, newOutVars) for var in variables])
+
         # Adjust sigmoid list
         for i, variables in enumerate(self.sigmoidList):
             self.sigmoidList[i] = tuple([self.reassignVariable(var, numInVars, outVars, newOutVars) for var in variables])

maraboupy/test/test_onnx.py

@@ -254,6 +254,13 @@ def test_resize():
     filename =  "resize/resize_4dims.onnx"
     evaluateFile(filename, inputNames = ['X'], outputNames = 'Y')
 
+def test_leaky_relu():
+    """
+    Test a network with Leaky ReLUs
+    """
+    filename = "mnist5x20_leaky_relu.onnx"
+    evaluateFile(filename)
+
 def test_errors():
     """
     This function tests that the ONNX parser catches errors.