trishullab/copra

COPRA: An in-COntext PRoof Agent which uses LLMs like GPTs to prove theorems in formal languages.

copra

COPRA: An in-COntext PRoof Agent which uses LLMs like GPTs to prove theorems in formal languages.

Setup Steps:

1. Install OCaml first. Use the instructions here: https://opam.ocaml.org/doc/Install.html . The opam version used in this project is 2.1.3 (OCaml 4.14.0). Note that OCaml officially only supports Linux installations. One can use WSL on Windows machines.

2. Run the following to install Coq on Linux. The Coq version used in this project is <= 8.15.

sudo apt install build-essential unzip bubblewrap
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

3. Add the following to your .bashrc file: (sometimes the path ~/.opam/default might not exist, so use the directory with version number present in the ~/.opam directory)

export PATH="/home/$USER/.opam/default/bin:$PATH"

4. Create a Miniconda environment and activate it.

5. Change to the project root directory, and run the setup script i.e. ./src/scripts/setup.sh from the root directory.

6. Add the following to your .bashrc file for Lean:

export PATH="/home/$USER/.elan/bin:$PATH"

7. You need to create a file .secrets/openai_key.json in the root directory of the project with the OpenAI API key. The file should contain the following:

{
    "organization": "<your-organization-id>",
    "api_key": "<your-api-key>"
}

8. The experiments are not necessarily thread safe. So, it is recommended to run them sequentially. The commands to run the desired experiments can be found in the file ./src/main/config/experiments.yaml.

copra's Issues

IDE integration for Coq

Is there any work to integrate this into some Coq IDE like company-coq?
if not, can you point out some top-level functions of copra's API that could be used in such an integration?

tree-of-thought style approach

have you tried a tree-of-thought style approach where the LLM is asked to come up multiple possible next steps and to critique each of those steps (and the broader proof strategy behind those steps) before picking the best choice?

results on llama

How are your results on llama, my attempts here have been rather poor.

CompCert Test Dataset

How are the 118 lemmas in CompCert Test Dataset, I can't find a benchmark from your config file that contains 118 lemmas

The Best Result

Can you please show the log file of your best results on GPT-4？I would like to do some analysis. And have you done any testing on the 13 test files presented in Proverbot 9001, and if so, what were the results?

CompCert Test Dataset

Sorry，but the CompCert Test Dataset you gave was only 109 lemma.

The Best Results.

Can you please show the log file of your best results on GPT-4？ And have you done any testing on the 13 test files presented in Proverbot 9001, and if so, what were the results?

what‘s the single.meta.json ？

What does single.meta.json look like, can you give an example?