Merge pull request #89 from Aaron99B/alpha-beta-crown-update

Alpha beta crown update
ADA-research · May 28, 2024 · 413eec6 · 413eec6
2 parents 2f681ea + 57cb9bf
commit 413eec6
Show file tree

Hide file tree

Showing 5 changed files with 136 additions and 185 deletions.
diff --git a/autoverify/cli/install/installers/abcrown/environment.yml b/autoverify/cli/install/installers/abcrown/environment.yml
@@ -2,200 +2,158 @@ name: __av__abcrown
 channels:
   - gurobi
   - pytorch
+  - nvidia
   - defaults
 dependencies:
   - _libgcc_mutex=0.1=main
-  - _openmp_mutex=4.5=1_gnu
-  - _tflow_select=2.3.0=mkl
-  - absl-py=0.15.0=pyhd3eb1b0_0
-  - aiohttp=3.8.1=py37h7f8727e_1
-  - aiosignal=1.2.0=pyhd3eb1b0_0
+  - _openmp_mutex=5.1=1_gnu
   - appdirs=1.4.4=pyhd3eb1b0_0
-  - astor=0.8.1=py37h06a4308_0
-  - astunparse=1.6.3=py_0
-  - async-timeout=4.0.1=pyhd3eb1b0_0
-  - asynctest=0.13.0=py_0
-  - attrs=21.4.0=pyhd3eb1b0_0
   - blas=1.0=mkl
-  - blinker=1.4=py37h06a4308_0
-  - blosc=1.21.0=h8c45485_0
-  - bottleneck=1.3.4=py37hce1f21e_0
-  - brotli=1.0.9=he6710b0_2
-  - brotlipy=0.7.0=py37h27cfd23_1003
-  - brunsli=0.1=h2531618_0
+  - bottleneck=1.3.7=py311hf4808d0_0
   - bzip2=1.0.8=h7b6447c_0
-  - c-ares=1.18.1=h7f8727e_0
-  - ca-certificates=2022.4.26=h06a4308_0
-  - cachetools=4.2.2=pyhd3eb1b0_0
-  - certifi=2022.6.15=py37h06a4308_0
-  - cffi=1.15.0=py37hd667e15_1
-  - cfitsio=3.470=hf0d0db6_6
-  - charls=2.2.0=h2531618_0
+  - c-ares=1.19.1=h5eee18b_0
+  - ca-certificates=2023.12.12=h06a4308_0
+  - certifi=2024.2.2=py311h06a4308_0
+  - cffi=1.16.0=py311h5eee18b_0
+  - cfgv=3.4.0=py311h06a4308_0
   - charset-normalizer=2.0.4=pyhd3eb1b0_0
-  - click=8.0.4=py37h06a4308_0
-  - cloudpickle=2.0.0=pyhd3eb1b0_0
-  - cryptography=36.0.0=py37h9ce1e76_0
-  - cudatoolkit=11.3.1=h2bc3f7f_2
-  - cycler=0.11.0=pyhd3eb1b0_0
-  - cytoolz=0.11.0=py37h7b6447c_0
-  - dask-core=2021.10.0=pyhd3eb1b0_0
-  - dataclasses=0.8=pyh6d0b6a4_7
-  - dbus=1.13.18=hb2f20db_0
-  - expat=2.4.4=h295c915_0
+  - coloredlogs=15.0.1=py311h06a4308_1
+  - cuda-cudart=12.1.105=0
+  - cuda-cupti=12.1.105=0
+  - cuda-libraries=12.1.0=0
+  - cuda-nvrtc=12.1.105=0
+  - cuda-nvtx=12.1.105=0
+  - cuda-opencl=12.3.101=0
+  - cuda-runtime=12.1.0=0
+  - distlib=0.3.6=py311h06a4308_0
   - ffmpeg=4.3=hf484d3e_0
-  - fontconfig=2.13.1=h6c09931_0
-  - fonttools=4.25.0=pyhd3eb1b0_0
-  - freetype=2.11.0=h70c0345_0
-  - frozenlist=1.2.0=py37h7f8727e_0
-  - fsspec=2022.3.0=py37h06a4308_0
-  - gast=0.4.0=pyhd3eb1b0_0
-  - giflib=5.2.1=h7b6447c_0
-  - glib=2.69.1=h4ff587b_1
-  - gmp=6.2.1=h2531618_2
+  - filelock=3.13.1=py311h06a4308_0
+  - freetype=2.12.1=h4a9f257_0
+  - gmp=6.2.1=h295c915_3
+  - gmpy2=2.1.2=py311hc9b5ff0_0
   - gnutls=3.6.15=he1e5248_0
-  - google-auth=2.6.0=pyhd3eb1b0_0
-  - google-auth-oauthlib=0.4.1=py_2
-  - google-pasta=0.2.0=pyhd3eb1b0_0
-  - grpcio=1.42.0=py37hce63b2e_0
-  - gst-plugins-base=1.14.0=h8213a91_2
-  - gstreamer=1.14.0=h28cd5cc_2
-  - gurobi=9.5.1=py37_0
-  - h5py=2.10.0=py37hd6299e0_1
-  - hdf5=1.10.6=hb1b8bf9_0
-  - icu=58.2=he6710b0_3
-  - idna=3.3=pyhd3eb1b0_0
-  - imagecodecs=2021.8.26=py37h4cda21f_0
-  - imageio=2.9.0=pyhd3eb1b0_0
-  - importlib-metadata=4.11.3=py37h06a4308_0
-  - intel-openmp=2021.4.0=h06a4308_3561
-  - jpeg=9d=h7f8727e_0
-  - jxrlib=1.1=h7b6447c_2
-  - keras=2.4.3=hd3eb1b0_0
-  - keras-base=2.4.3=pyhd3eb1b0_0
-  - keras-preprocessing=1.1.2=pyhd3eb1b0_0
-  - kiwisolver=1.4.2=py37h295c915_0
-  - krb5=1.19.2=hac12032_0
+  - gurobi=11.0.0=py311_0
+  - humanfriendly=10.0=py311h06a4308_1
+  - identify=2.5.5=py311h06a4308_0
+  - idna=3.4=py311h06a4308_0
+  - iniconfig=1.1.1=pyhd3eb1b0_0
+  - intel-openmp=2023.1.0=hdb19cb5_46306
+  - jinja2=3.1.3=py311h06a4308_0
+  - joblib=1.2.0=py311h06a4308_0
+  - jpeg=9e=h5eee18b_1
+  - krb5=1.20.1=h143b758_1
   - lame=3.100=h7b6447c_0
   - lcms2=2.12=h3be6417_0
-  - ld_impl_linux-64=2.35.1=h7274673_9
+  - ld_impl_linux-64=2.38=h1181459_1
   - lerc=3.0=h295c915_0
-  - libaec=1.0.4=he6710b0_1
-  - libclang=10.0.1=default_hb85057a_2
-  - libcurl=7.82.0=h0b77cf5_0
-  - libdeflate=1.8=h7f8727e_5
-  - libedit=3.1.20210910=h7f8727e_0
+  - libcublas=12.1.0.26=0
+  - libcufft=11.0.2.4=0
+  - libcufile=1.8.1.2=0
+  - libcurand=10.3.4.107=0
+  - libcurl=8.5.0=h251f7ec_0
+  - libcusolver=11.4.4.55=0
+  - libcusparse=12.0.2.55=0
+  - libdeflate=1.17=h5eee18b_1
+  - libedit=3.1.20230828=h5eee18b_0
   - libev=4.33=h7f8727e_1
-  - libffi=3.3=he6710b0_2
-  - libgcc-ng=9.3.0=h5101ec6_17
-  - libgfortran-ng=7.5.0=ha8ba4b0_17
-  - libgfortran4=7.5.0=ha8ba4b0_17
-  - libgomp=9.3.0=h5101ec6_17
-  - libiconv=1.15=h63c8f33_5
-  - libidn2=2.3.2=h7f8727e_0
-  - libllvm10=10.0.1=hbcb73fb_5
-  - libnghttp2=1.46.0=hce63b2e_0
-  - libpng=1.6.37=hbc83047_0
-  - libprotobuf=3.20.1=h4ff587b_0
-  - libssh2=1.10.0=h8f2d780_0
-  - libstdcxx-ng=9.3.0=hd4cf53a_17
-  - libtasn1=4.16.0=h27cfd23_0
-  - libtiff=4.2.0=h85742a9_0
+  - libffi=3.4.4=h6a678d5_0
+  - libgcc-ng=11.2.0=h1234567_1
+  - libgfortran-ng=11.2.0=h00389a5_1
+  - libgfortran5=11.2.0=h1234567_1
+  - libgomp=11.2.0=h1234567_1
+  - libiconv=1.16=h7f8727e_2
+  - libidn2=2.3.4=h5eee18b_0
+  - libjpeg-turbo=2.0.0=h9bf148f_0
+  - libnghttp2=1.57.0=h2d74bed_0
+  - libnpp=12.0.2.50=0
+  - libnvjitlink=12.1.105=0
+  - libnvjpeg=12.1.1.14=0
+  - libpng=1.6.39=h5eee18b_0
+  - libprotobuf=3.20.3=he621ea3_0
+  - libssh2=1.10.0=hdbd6064_2
+  - libstdcxx-ng=11.2.0=h1234567_1
+  - libtasn1=4.19.0=h5eee18b_0
+  - libtiff=4.5.1=h6a678d5_0
   - libunistring=0.9.10=h27cfd23_0
-  - libuuid=1.0.3=h7f8727e_2
-  - libuv=1.40.0=h7b6447c_0
-  - libwebp=1.2.2=h55f646e_0
-  - libwebp-base=1.2.2=h7f8727e_0
-  - libxcb=1.15=h7f8727e_0
-  - libxml2=2.9.14=h74e7548_0
-  - libzopfli=1.0.3=he6710b0_0
-  - locket=1.0.0=py37h06a4308_0
-  - lz4-c=1.9.3=h295c915_1
-  - markdown=3.3.4=py37h06a4308_0
-  - matplotlib=3.5.1=py37h06a4308_1
-  - matplotlib-base=3.5.1=py37ha18d171_1
-  - mkl=2021.4.0=h06a4308_640
-  - mkl-service=2.4.0=py37h7f8727e_0
-  - mkl_fft=1.3.1=py37hd3c417c_0
-  - mkl_random=1.2.2=py37h51133e4_0
-  - multidict=5.2.0=py37h7f8727e_2
-  - munkres=1.1.4=py_0
-  - ncurses=6.3=h7f8727e_2
+  - libuuid=1.41.5=h5eee18b_0
+  - libwebp-base=1.3.2=h5eee18b_0
+  - llvm-openmp=14.0.6=h9e868ea_0
+  - lz4-c=1.9.4=h6a678d5_0
+  - markdown-it-py=2.2.0=py311h06a4308_1
+  - markupsafe=2.1.3=py311h5eee18b_0
+  - mdurl=0.1.0=py311h06a4308_0
+  - mkl=2023.1.0=h213fc3f_46344
+  - mkl-service=2.4.0=py311h5eee18b_1
+  - mkl_fft=1.3.8=py311h5eee18b_0
+  - mkl_random=1.2.4=py311hdb19cb5_0
+  - mpc=1.1.0=h10f8cd9_1
+  - mpfr=4.0.2=hb69a4c5_1
+  - mpmath=1.3.0=py311h06a4308_0
+  - ncurses=6.4=h6a678d5_0
   - nettle=3.7.3=hbbd107a_1
-  - networkx=2.6.3=pyhd3eb1b0_0
-  - numexpr=2.8.1=py37h6abb31d_0
-  - numpy=1.21.5=py37he7a7128_1
-  - numpy-base=1.21.5=py37hf524024_1
-  - oauthlib=3.1.0=py_0
+  - networkx=3.1=py311h06a4308_0
+  - nodeenv=1.7.0=py311h06a4308_0
+  - numexpr=2.8.7=py311h65dcdc2_0
+  - numpy=1.26.4=py311h08b1b3b_0
+  - numpy-base=1.26.4=py311hf175353_0
+  - onnx=1.13.1=py311h12ddb61_0
+  - onnxruntime=1.15.1=py311hcd73a83_0
   - openh264=2.1.1=h4ff587b_0
   - openjpeg=2.4.0=h3ad879b_0
-  - openssl=1.1.1q=h7f8727e_0
-  - opt_einsum=3.3.0=pyhd3eb1b0_1
-  - packaging=21.3=pyhd3eb1b0_0
-  - pandas=1.3.4=py37h8c16a72_0
-  - partd=1.2.0=pyhd3eb1b0_1
-  - pcre=8.45=h295c915_0
-  - pillow=9.0.1=py37h22f2fdc_0
-  - pip=21.2.2=py37h06a4308_0
-  - psutil=5.8.0=py37h27cfd23_1
-  - pyasn1=0.4.8=pyhd3eb1b0_0
-  - pyasn1-modules=0.2.8=py_0
+  - openssl=3.0.13=h7f8727e_0
+  - packaging=23.1=py311h06a4308_0
+  - pandas=2.1.4=py311ha02d727_0
+  - pillow=10.2.0=py311h5eee18b_0
+  - pip=23.3.1=py311h06a4308_0
+  - platformdirs=2.5.2=py311h06a4308_0
+  - pluggy=1.0.0=py311h06a4308_1
+  - pre-commit=3.4.0=py311h06a4308_1
+  - psutil=5.9.0=py311h5eee18b_0
   - pycparser=2.21=pyhd3eb1b0_0
-  - pyjwt=2.4.0=py37h06a4308_0
-  - pyopenssl=22.0.0=pyhd3eb1b0_0
-  - pyparsing=3.0.4=pyhd3eb1b0_0
-  - pyqt=5.9.2=py37h05f1152_2
-  - pysocks=1.7.1=py37_1
-  - python=3.7.13=h12debd9_0
+  - pygments=2.15.1=py311h06a4308_1
+  - pytest=7.4.0=py311h06a4308_0
+  - python=3.11.8=h955ad1f_0
   - python-dateutil=2.8.2=pyhd3eb1b0_0
   - python-flatbuffers=2.0=pyhd3eb1b0_0
-  - pytorch=1.11.0=py3.7_cuda11.3_cudnn8.2.0_0
+  - python-tzdata=2023.3=pyhd3eb1b0_0
+  - pytorch=2.2.1=py3.11_cuda12.1_cudnn8.9.2_0
+  - pytorch-cuda=12.1=ha16c6d3_5
   - pytorch-mutex=1.0=cuda
-  - pytz=2021.3=pyhd3eb1b0_0
-  - pywavelets=1.3.0=py37h7f8727e_0
-  - pyyaml=6.0=py37h7f8727e_1
-  - qt=5.9.7=h5867ecd_1
-  - readline=8.1.2=h7f8727e_1
-  - requests=2.27.1=pyhd3eb1b0_0
-  - requests-oauthlib=1.3.0=py_0
-  - rsa=4.7.2=pyhd3eb1b0_1
-  - scikit-image=0.19.2=py37h51133e4_0
-  - scipy=1.7.3=py37hc147768_0
-  - setuptools=61.2.0=py37h06a4308_0
-  - sip=4.19.8=py37hf484d3e_0
+  - pytz=2023.3.post1=py311h06a4308_0
+  - pyyaml=6.0.1=py311h5eee18b_0
+  - readline=8.2=h5eee18b_0
+  - requests=2.31.0=py311h06a4308_1
+  - rich=13.3.5=py311h06a4308_0
+  - scikit-learn=1.2.2=py311h6a678d5_1
+  - scipy=1.11.4=py311h08b1b3b_0
+  - setuptools=68.2.2=py311h06a4308_0
   - six=1.16.0=pyhd3eb1b0_1
-  - snappy=1.1.9=h295c915_0
   - sortedcontainers=2.4.0=pyhd3eb1b0_0
-  - sqlite=3.38.2=hc218d9a_0
-  - tensorboard=2.6.0=py_1
-  - tensorboard-data-server=0.6.0=py37hca6d32c_0
-  - tensorboard-plugin-wit=1.6.0=py_0
-  - tensorflow=2.4.1=mkl_py37h2d14ff2_0
-  - tensorflow-base=2.4.1=mkl_py37h43e0292_0
-  - tensorflow-estimator=2.6.0=pyh7b7c402_0
-  - termcolor=1.1.0=py37h06a4308_1
-  - tifffile=2021.7.2=pyhd3eb1b0_2
-  - tk=8.6.11=h1ccaba5_0
-  - toolz=0.11.2=pyhd3eb1b0_0
-  - torchaudio=0.11.0=py37_cu113
-  - torchvision=0.12.0=py37_cu113
-  - tornado=6.1=py37h27cfd23_0
-  - tqdm=4.64.0=py37h06a4308_0
-  - typing-extensions=4.1.1=hd3eb1b0_0
-  - typing_extensions=4.1.1=pyh06a4308_0
-  - urllib3=1.26.9=py37h06a4308_0
-  - werkzeug=2.0.3=pyhd3eb1b0_0
-  - wheel=0.37.1=pyhd3eb1b0_0
-  - wrapt=1.13.3=py37h7f8727e_2
-  - xz=5.2.5=h7b6447c_0
+  - sqlite=3.41.2=h5eee18b_0
+  - sympy=1.12=py311h06a4308_0
+  - tbb=2021.8.0=hdb19cb5_0
+  - threadpoolctl=2.2.0=pyh0d69192_0
+  - tk=8.6.12=h1ccaba5_0
+  - torchaudio=2.2.1=py311_cu121
+  - torchtriton=2.2.0=py311
+  - torchvision=0.17.1=py311_cu121
+  - tqdm=4.65.0=py311h92b7b1e_0
+  - typing-extensions=4.9.0=py311h06a4308_1
+  - typing_extensions=4.9.0=py311h06a4308_1
+  - tzdata=2024a=h04d1e81_0
+  - ukkonen=1.0.1=py311hdb19cb5_0
+  - urllib3=2.1.0=py311h06a4308_0
+  - virtualenv=20.17.1=py311h06a4308_0
+  - wheel=0.41.2=py311h06a4308_0
+  - xz=5.4.6=h5eee18b_0
   - yaml=0.2.5=h7b6447c_0
-  - yarl=1.6.3=py37h27cfd23_0
-  - zfp=0.5.5=h295c915_6
-  - zipp=3.8.0=py37h06a4308_0
-  - zlib=1.2.12=h7f8727e_2
-  - zstd=1.4.9=haebb681_0
+  - zlib=1.2.13=h5eee18b_0
+  - zstd=1.5.5=hc292b87_0
   - pip:
-      - flatbuffers==2.0
-      - onnx==1.11.0
-      - git+https://github.com/KaidiXu/onnx2pytorch@102cf22e64ea7fae9462c1ba0feaa250ac0bc628#egg=onnx2pytorch
-      - onnxruntime==1.11.0
-      - protobuf==3.20.1
+    - fsspec==2024.2.0
+    - git+https://github.com/KaidiXu/onnx2pytorch@fe7281b9b6c8c28f61e72b8f3b0e3181067c7399#egg=onnx2pytorch
+    - onnxconverter-common==1.14.0
+    - onnxoptimizer==0.3.13
+    - onnxsim==0.4.35
+    - protobuf==3.20.2
+    - skl2onnx==1.16.0
diff --git a/autoverify/cli/install/installers/abcrown/install.py b/autoverify/cli/install/installers/abcrown/install.py
@@ -8,7 +8,7 @@
 
 AbCrownRepoInfo = GitRepoInfo(
     branch="main",
-    commit_hash="7b3d507",
+    commit_hash="877afa32d9d314fcb416436a616e6a5878fdab78",
     clone_url="https://github.com/Verified-Intelligence/alpha-beta-CROWN",
 )
 

diff --git a/autoverify/cli/util/git.py b/autoverify/cli/util/git.py
@@ -34,7 +34,8 @@ def repo_name(self) -> str:
 
     @property
     def clone(self) -> list[str]:
-        clone_cmd = f"git clone {self.clone_url} --branch {self.branch}"
+        clone_cmd = f"""git clone --recursive {self.clone_url}\
+        --branch {self.branch}"""
 
         return shlex.split(clone_cmd)
 

diff --git a/autoverify/verifier/complete/abcrown/verifier.py b/autoverify/verifier/complete/abcrown/verifier.py
@@ -8,12 +8,8 @@
 
 from autoverify import DEFAULT_VERIFICATION_TIMEOUT_SEC
 from autoverify.util import find_substring
-from autoverify.util.conda import (
-    find_conda_lib,
-    get_conda_path,
-    get_conda_source_cmd,
-)
-from autoverify.util.env import cwd, environment, pkill_matches
+from autoverify.util.conda import get_conda_path, get_conda_source_cmd
+from autoverify.util.env import cwd, pkill_matches
 from autoverify.util.tempfiles import tmp_file
 from autoverify.verifier.complete.abcrown.abcrown_yaml_config import (
     AbcrownYamlConfig,
@@ -53,11 +49,6 @@ def contexts(self) -> list[ContextManager[None]]:
         return [
             cwd(self.tool_path / "complete_verifier"),
             pkill_matches(["python abcrown.py"]),
-            environment(
-                LD_LIBRARY_PATH=str(
-                    find_conda_lib(self.conda_env_name, "libcudart.so.11.0")
-                )
-            ),
         ]
 
     def _parse_result(

diff --git a/tests/test_cli/test_util.py b/tests/test_cli/test_util.py
@@ -64,6 +64,7 @@ def test_clone_command(dummy_repo_info: GitRepoInfo):
     expected_cmd = [
         "git",
         "clone",
+        "--recursive",
         DUMMY_CLONE_URL,
         "--branch",
         DUMMY_BRANCH,