Formal Theorem Proving on miniF2F Isabelle (val)
57Success RateLEGO-Prover*
Evaluation Results
| Method | Links | |
|---|---|---|
| LEGO-Prover*LLM=ChatGPT, Attempts=100, Cumulative pass rate=true2023.10 | 57 | |
| LEGO-Prover (human informal proof)LLM=ChatGPT, Attempts=100, Informal proof source=human-written2023.10 | 55.3 | |
| LyraInformal proof source=Human, Attempts=2002023.09 | 55.3 | |
| LyraInformal proof source=GPT-4, Attempts=2002023.09 | 54.9 | |
| LyraInformal proof source=GPT-4, Attempts=1002023.09 | 52.8 | |
| LEGO-Prover (model informal proof)LLM=ChatGPT, Attempts=100, Informal proof source=model-generated2023.10 | 52.4 | |
| LyraInformal proof source=Human, Attempts=1002023.09 | 52 | |
| LEGO-ProverLLM=ChatGPT, Attempts=50, Note=Ablation setting2023.10 | 50.4 | |
| Subgoal-based Demonstration LearningVariant=Full Method, Protocol=Cumulative pass rate2023.05 | 48 | |
| Subgoal-LearningLLM=ChatGPT2023.10 | 48 | |
| Subgoal-LearningAttempts=1002023.09 | 48 | |
| Subgoal-based Demonstration LearningVariant=Remove Diffusion2023.05 | 47.5 | |
| LEGO-Prover without Skill LibraryLLM=ChatGPT, Attempts=50, Skill Library=removed2023.10 | 47.1 | |
| Subgoal-based Demonstration LearningVariant=Remove Subgoal, Protocol=Cumulative pass rate2023.05 | 44.3 | |
| DSPModel=540B Minerva2023.05 | 42.6 | |
| Draft, sketch, and ProveLLM=Codex2023.10 | 42.6 | |
| Draft, Sketch, and Prove (DSP)Informal proof source=Human, Attempts=1002023.09 | 42.6 | |
| Draft, Sketch, and Prove (DSP)Informal proof source=540B Minerva, Attempts=1002023.09 | 42.6 | |
| Subgoal-based Demonstration LearningVariant=Remove Subgoal & Diffusion2023.05 | 41.8 | |
| Thor + expert iterationExpert Iteration=True2023.05 | 37.3 | |
| Thor + expert iterationLLM=Codex2023.10 | 37.3 | |
| ThorExpert iteration=true2023.09 | 37.3 | |
| Thor2023.05 | 28.3 | |
| ThorLLM=N/A2023.10 | 28.3 | |
| Thor2023.09 | 28.3 | |
| Sledgehammer+heuristicHeuristic=True2023.05 | 18 | |
| SledgehammerHeuristic tactics=true2023.09 | 18 | |
| Sledgehammer2023.05 | 9.9 | |
| Sledgehammer2023.09 | 9.9 | |
| Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=62B2022.10 | 0.439 | |
| Draft, Sketch, and ProveInformal proof source=Human2022.10 | 0.426 | |
| Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=540B2022.10 | 0.426 | |
| Draft, Sketch, and ProveInformal proof source=Codex2022.10 | 0.406 | |
| Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=8B2022.10 | 0.406 | |
| Draft, Sketch, and ProveInformal proof source=Human, Ablation=without informal proofs2022.10 | 0.389 | |
| Draft, Sketch, and ProveInformal proof source=Human, Ablation=without in-line comments2022.10 | 0.377 | |
| Thor + expert iterationType=Baseline2022.10 | 0.373 | |
| Draft, Sketch, and ProveInformal proof source=Human, Ablation=without automated provers2022.10 | 0.328 | |
| ThorType=Baseline2022.10 | 0.283 | |
| Sledgehammer + heuristicsType=Baseline2022.10 | 0.18 | |
| SledgehammerType=Baseline2022.10 | 0.099 |