A bot for proving.
You can find the paper and talk video at our website.
- Check your python version with
python --versionin the terminal. If your version is older than Python 3.7, or the python command isn't found, install python through the python website. - Make sure pip, the python package manager, is available, by running
in your terminal:
python -m ensurepip. - Install Homebrew from their website.
- Install wget, git, opam, rustup, GNU awk, and graphviz through Homebrew:
brew install wget git opam rustup-init gawk graphviz && rustup-init - On newer MacOS systems, homebrew installs into
/opt/homebrewnot/usr/local, so run:export CPATH=/opt/homebrew/include && export LIBRARY_PATH=/opt/homebrew/lib.
- Check your python version with
python --versionin the terminal. If your version is older than Python 3.7, or the python command isn't found, install python through your package manager.- On Ubuntu, that's:
sudo apt install python3 python3-dev python3-pip - Make sure pip, the python package manager, is available, by running
in your terminal:
python -m ensurepip. - Install git, opam, rustup, and graphviz using your package manager.
- On Ubuntu, that's:
sudo apt install software-properties-common sudo add-apt-repository ppa:avsm/ppa sudo apt update sudo apt install git opam rustup graphviz libgraphviz-dev
Windows support is more experimental, but you can try installing prereqs through:
https://fdopen.github.io/opam-repository-mingw/installation/
https://graphviz.gitlab.io/_pages/Download/Download_windows.html
https://www.python.org/downloads/windows/
or use Windows Subsystem for Linux
The first thing you'll need to do is clone the repository (download the code).
I recommend that you do this over ssh. To clone github projects using git@ urls (over ssh), you'll need to follow the instructions on this github page. Then, open a terminal (windows users can use "Bash on Ubuntu on Windows"), move to the directory you want to work in, and run:
git clone [email protected]:UCSD-PL/proverbot9001.git
Alternatively, you can clone over https without setting up your github keys, with this command:
git clone https://github.com/UCSD-PL/proverbot9001.git
That should give you a new folder called proverbot9001 with all the
code inside. Move into this new directory:
cd proverbot9001
NOTE: There are two ways you can run the project after this, you can either set it up on your machine or use docker and build the container and run the project inside that.
- Install Docker desktop on your machine as it makes things easy for you to manage and run containers.
- Make sure Docker desktop is running. Run the following command from the root of the project (build can take ~1 hour depending on your machine spec and network speed):
docker build -t proverbot:<tag> .
- Run the built container through Docker desktop directly or using the following command:
docker run -i -t proverbot:<tag> /bin/bash
This will run the container and start a bash terminal.
- After this you can start running search commands and interacting with the project.
NOTE: These instructions are for setting up the project on your machine.
Next, you'll need to create a python virtual environment to work in. This is a good idea in general, but is also required for maturin to work properly.
python -m venv proverbot-env
Whenever you want to work with Proverbot from a new shell, you'll have to first activate this environment:
source proverbot-env/bin/activate
Also do that now.
On MacOS, you'll need to install pygraphviz differently, so do that
now: pip install --global-option=build_ext --global-option="-I/usr/local/include/" --global-option="-L/usr/local/lib/" pygraphviz
Then, no matter your platform, run this command to install the dependencies:
make setup
this step will take a while, and might involve having to type y a
few times.
If this step fails, and part of the error message near the bottom says:
pygraphviz/graphviz_wrap.c:2711:10: fatal error: graphviz/cgraph.h: No such file or directory
2711 | #include "graphviz/cgraph.h"
| ^~~~~~~~~~~~~~~~~~~
compilation terminated.
error: command 'x86_64-linux-gnu-gcc' failed with exit status 1
then python needs help finding your graphviz installation. Check out this github issue: pygraphviz/pygraphviz#155, and possibly this one: pypa/setuptools#2740 .
Running Proverbot9001 requires training on existing proof files. Training takes a while, and usually you need some pretty advanced hardware. So to quickly get started, we'll download pre-trained weights instead:
make download-weights
Now you can run Proverbot9001:
make search-report
Which will generate some html in the reports directory.
You should be able to check out the results by opening a web browser
and navigating to the reports directory in the project.
Once you've done that, you might like to try training from scratch
with make scrape and make train, or writing your own
predictor.
The latest Proverbot9001 results can be found
here.
This is a report in the format generated by Proverbot9001's make search-report; you can click on individual files to see exactly which
theorems were proven by Proverbot9001 and what the proofs are.
You can also view the results that were used in the 2020 MAPL paper (linked above) here. However, these results are not up-to-date. If you use these results for a comparison or otherwise write about them, please add a footnote or other comment noting that these results are significantly worse than the latest Proverbot9001 results.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent