Formal Theorem Proving on miniF2F Isabelle (test)
51.2Success RateLyra
Evaluation results
| Method | Links | |
|---|---|---|
| LyraInformal proof source=Human, Attempts=2002023.09 | 51.2 | |
| LEGO-Prover (human informal proof)LLM=ChatGPT, Attempts=100, Informal proof source=human-written2023.10 | 50 | |
| LEGO-Prover*LLM=ChatGPT, Attempts=100, Cumulative pass rate=true2023.10 | 50 | |
| LyraInformal proof source=GPT-4, Attempts=2002023.09 | 47.9 | |
| LyraInformal proof source=Human, Attempts=1002023.09 | 47.1 | |
| Subgoal-based Demonstration LearningVariant=Full Method2023.05 | 45.5 | |
| Subgoal-LearningLLM=ChatGPT2023.10 | 45.5 | |
| LEGO-Prover (model informal proof)LLM=ChatGPT, Attempts=100, Informal proof source=model-generated2023.10 | 45.5 | |
| Subgoal-LearningAttempts=1002023.09 | 45.5 | |
| Subgoal-based Demonstration LearningVariant=Remove Diffusion2023.05 | 44.3 | |
| LyraInformal proof source=GPT-4, Attempts=1002023.09 | 44.2 | |
| Subgoal-based Demonstration LearningVariant=Remove Subgoal2023.05 | 40.6 | |
| Draft, Sketch, and ProveInformal proof source=Human2022.10 | 39.3 | |
| Draft, sketch, and ProveLLM=Codex2023.10 | 39.3 | |
| Draft, Sketch, and Prove (DSP)Informal proof source=Human, Attempts=1002023.09 | 39.3 | |
| Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=540B2022.10 | 38.9 | |
| DSPModel=540B Minerva2023.05 | 38.9 | |
| Draft, Sketch, and Prove (DSP)Informal proof source=540B Minerva, Attempts=1002023.09 | 38.9 | |
| Subgoal-based Demonstration LearningVariant=Remove Subgoal & Diffusion2023.05 | 38.5 | |
| Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=62B2022.10 | 37.7 | |
| Draft, Sketch, and ProveInformal proof source=Human, Ablation=without in-line comments2022.10 | 36.5 | |
| Draft, Sketch, and ProveInformal proof source=Codex2022.10 | 35.3 | |
| Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=8B2022.10 | 35.3 | |
| Thor + expert iterationType=Baseline2022.10 | 35.2 | |
| Thor + expert iterationExpert Iteration=True2023.05 | 35.2 | |
| Thor + expert iterationLLM=Codex2023.10 | 35.2 | |
| ThorExpert iteration=true2023.09 | 35.2 | |
| Draft, Sketch, and ProveInformal proof source=Human, Ablation=without informal proofs2022.10 | 34 | |
| Draft, Sketch, and ProveInformal proof source=Human, Ablation=without automated provers2022.10 | 30.3 | |
| ThorType=Baseline2022.10 | 29.9 | |
| Thor2023.05 | 29.9 | |
| ThorLLM=N/A2023.10 | 29.9 | |
| Thor2023.09 | 29.9 | |
| Sledgehammer + heuristicsType=Baseline2022.10 | 20.9 | |
| Sledgehammer+heuristicHeuristic=True2023.05 | 20.9 | |
| SledgehammerHeuristic tactics=true2023.09 | 20.9 | |
| SledgehammerType=Baseline2022.10 | 10.4 | |
| Sledgehammer2023.05 | 10.4 | |
| Sledgehammer2023.09 | 10.4 |