search

albertqjiang / draft_sketch_prove

Other
61 stars 8 forks source link

readme

Autoformalization of Proofs

Authors: Sean Welleck, Albert Q. Jiang, Jin Peng Zhou

Implementation for the ICLR 2023 (Oral) paper: Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs.

Update 30 September

Sean has put together a step-by-step tutorial to play with DSP: https://github.com/wellecks/ntptutorial/tree/main/partII_dsp. Check it out!

Results

In the results folder are the names of theorems that can be solved by

It also contains the proofs found with human informal proofs x 100 autoformalizations. Sledgehammer-generated steps are labelled with a \<ATP> \</ATP> tag.

Setup

python setup.py develop

OpenAI keys

First of all, you should go to autoformalization/utils.py to put your openai keys there.

Querying for autoformalizations

We use a slurm/submitit system to execute multiple queries concurrently. Take a loot at scripts/albert/parallel_codex_query_canon.py to see how it's done. Make sure to change the partition names to fit your system.

Evaluating the queried results

Evaluating the outputs requires a Portal-to-ISAbelle to exist. Please take extra caution to verify your installation, or it could fail in surprising ways.

Then, take a look at scripts/albert/eval_script.py to see how mass evaluation is done, also with a slurm/submitit system. Adjust paths, partitions, and specifications where appropriate.

(Warning) Working with Isabelle is not easy. Please be patient with the installations and the setting up. It will pay off.

Citation

@inproceedings{
jiang2023draft,
title={{Draft}, {Sketch}, and {Prove}: {Guiding} Formal Theorem Provers with Informal Proofs},
author={Albert Qiaochu Jiang and Sean Welleck and Jin Peng Zhou and Wenda Li and Jiacheng Liu and Mateja Jamnik and Timoth{\'{e}}e Lacroix and Yuhuai Wu and Guillaume Lample},
booktitle={International Conference on Learning Representations},
year={2023},
url={https://doi.org/10.48550/arXiv.2210.12283}
}