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.
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!
In the results folder are the names of theorems that can be solved by
- Hammer + heuristics
- Human informal proofs x 100 autoformalizations
- Minerva informal proofs x 100 autoformalizations
- Minerva informal proofs x 200 autoformalizations.
It also contains the proofs found with human informal proofs x 100 autoformalizations. Sledgehammer-generated steps are labelled with a <ATP> </ATP> tag.
python setup.py developFirst of all, you should go to autoformalization/utils.py to put your openai keys there.
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 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.
@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}
}