Merge pull request #91 from dlshriver/update-verifier-installs

fix: include explicit max version for protobuf

dnnv/_manage/linux/verifiers/eran.py

@@ -99,7 +99,7 @@ def main():
 
 class ELINAInstaller(Installer):
     def run(self, env: Environment, dependency: Dependency):
-        commit_hash = "7e0e6fef43c9676c869199782f4beadd542449f6"
+        commit_hash = "eaefbbd9b42e0e80c0701b5c20b7906e88fbb954"
         name = "elina"
 
         cache_dir = env.cache_dir / f"{name}-{commit_hash}"
@@ -165,7 +165,7 @@ def run(self, env: Environment, dependency: Dependency):
 
 class ERANInstaller(Installer):
     def run(self, env: Environment, dependency: Dependency):
-        commit_hash = "d60cf5767da31e7834b202fbcbb840e9c7d3ef5e"
+        commit_hash = "8771d3158b2c64a360d5bdfd4433490863257dd6"
         name = "eran"
 
         cache_dir = env.cache_dir / f"{name}-{commit_hash}"
@@ -207,6 +207,7 @@ def run(self, env: Environment, dependency: Dependency):
                 ' "torchvision>=0.9,<0.12"'
                 ' "mpmath>=1.2,<1.3"'
                 ' "pillow>=8.1"'
+                ' "protobuf<=3.20"'
             ),
             f"cd {gurobi_path}",
             "python setup.py install",

dnnv/_manage/linux/verifiers/marabou.py

@@ -39,7 +39,7 @@ def main(args):
     network = Marabou.read_onnx(args.model)
 
     inputVars = network.inputVars[0]
-    outputVars = network.outputVars
+    outputVars = network.outputVars[0]
 
     for x, l, u in zip(inputVars.flatten(), lb, ub):
         network.setLowerBound(x, l)
@@ -53,21 +53,20 @@ def main(args):
 
     options = MarabouCore.Options()
     options._numWorkers = args.num_workers
-    result = network.solve(options=options)
-
-    is_unsafe = bool(result[0])
-    print("UNSAFE" if is_unsafe else "SAFE")
+    result_str, vals, stats = network.solve(options=options)
+    print(result_str)
+    is_unsafe = result_str == "sat"
 
     if args.output is not None:
         cex = None
         if is_unsafe:
             cex = np.zeros_like(inputVars, dtype=np.float32)
             for flat_index, multi_index in enumerate(np.ndindex(cex.shape)):
-                cex[multi_index] = result[0][flat_index]
+                cex[multi_index] = vals[flat_index]
             print(cex)
         np.save(
             args.output,
-            (is_unsafe, cex),
+            (result_str, cex),
         )
 
 
@@ -78,7 +77,7 @@ def main(args):
 
 class MarabouInstaller(Installer):
     def run(self, env: Environment, dependency: Dependency):
-        commit_hash = "c179c5db1af2cb66bc45c4ed7fbb7a1897e67233"
+        commit_hash = "492c1b8c703c8a383f421468a104c34710e6d26d"
 
         cache_dir = env.cache_dir / f"marabou-{commit_hash}"
         cache_dir.mkdir(exist_ok=True, parents=True)
@@ -93,12 +92,15 @@ def run(self, env: Environment, dependency: Dependency):
         assert libopenblas_path is not None
         openblas_path = libopenblas_path.parent.parent
 
-        python_major_version, python_minor_version = sys.version_info[:2]
+        python_major_version, python_minor_version, *_ = sys.version_info
         python_version = f"python{python_major_version}.{python_minor_version}"
         site_packages_dir = f"{verifier_venv_path}/lib/{python_version}/site-packages/"
 
         marabou_url = "https://github.com/NeuralNetworkVerification/Marabou.git"
 
+        build_dir = cache_dir / f"Marabou/build-{python_version}"
+        openblas_vars = f"-D OPENBLAS_DIR={build_dir}/OpenBlas"
+
         commands = [
             "set -ex",
             f"cd {verifier_venv_path.parent}",
@@ -109,22 +111,24 @@ def run(self, env: Environment, dependency: Dependency):
             (
                 "pip install"
                 ' "numpy>=1.19,<1.22"'
-                ' "onnx>=1.8,<1.11"'
-                ' "onnxruntime>=1.7,<1.11"'
+                ' "onnx>=1.8,<1.12"'
+                ' "onnxruntime>=1.7,<1.12"'
+                ' "protobuf<=3.20"'
             ),
             f"cd {cache_dir}",
-            "if [ ! -e Marabou ]",
-            "then git clone https://github.com/NeuralNetworkVerification/Marabou.git",
+            f"if [ ! -e Marabou ]",
+            f"then git clone {marabou_url}",
             "cd Marabou",
             f"git checkout {commit_hash}",
-            "mkdir -p build",
-            "cd build",
+            "fi",
+            f"if [ ! -e {build_dir} ]",
+            f"then mkdir -p {build_dir}",
+            f"cd {build_dir}",
             "mkdir -p OpenBlas",
-            f"rm -f {cache_dir}/Marabou/build/OpenBlas/installed",
-            f"ln -s {openblas_path} {cache_dir}/Marabou/build/OpenBlas/installed",
-            f"cmake -D OPENBLAS_DIR={cache_dir}/Marabou/build/OpenBlas ..",
+            f"ln -s {openblas_path} {build_dir}/OpenBlas/installed",
+            f"cmake {openblas_vars} ..",
             "cmake --build .",
-            "else cd Marabou/build",
+            f"else cd {build_dir}",
             "fi",
             f"cp -r ../maraboupy {site_packages_dir}",
         ]

dnnv/_manage/linux/verifiers/nnenum.py

@@ -79,7 +79,7 @@ def main(args):
 
 class NnenumInstaller(Installer):
     def run(self, env: Environment, dependency: Dependency):
-        commit_hash = "fd07f2b6c55ca46387954559f40992ae0c9b06b7"
+        commit_hash = "fa1463b6f345ca143662c4143dfb4774e6615672"
         name = "nnenum"
 
         cache_dir = env.cache_dir / f"{name}-{commit_hash}"
@@ -113,6 +113,7 @@ def run(self, env: Environment, dependency: Dependency):
                 ' "skl2onnx==1.7.0"'
                 ' "swiglpk"'
                 ' "termcolor"'
+                ' "protobuf<=3.20"'
             ),
             f"cd {cache_dir}",
             f"if [ ! -e {name} ]",

dnnv/verifiers/marabou/__init__.py

@@ -54,11 +54,11 @@ def build_inputs(self, prop):
         return args
 
     def parse_results(self, prop, results):
-        result, cinput = np.load(self._tmp_output_file.name, allow_pickle=True)
-        if result == False:
+        result_str, cinput = np.load(self._tmp_output_file.name, allow_pickle=True)
+        if result_str == "unsat":
             return UNSAT, None
-        elif result == True:
+        elif result_str == "sat":
             input_shape, input_dtype = prop.op_graph.input_details[0]
             cex = cinput.reshape(input_shape).astype(input_dtype)
             return SAT, cex
-        raise self.translator_error(f"Unknown verification result: {result}")
+        raise self.translator_error(f"Unknown verification result: {result_str}")

tests/system_tests/test_verifiers/test_random.py

@@ -219,6 +219,7 @@ def test_random_conv_2(self):
             ("reluplex", 0.1),  # conv unsupported
             ("reluplex", 0.5),  # conv unsupported
             ("reluplex", 1.0),  # conv unsupported
+            ("marabou", 1.0),  # numerical instability
         }
         for epsilon in [0.01, 0.1, 0.5, 1.0]:
             os.environ["EPSILON"] = str(epsilon)