List your company
ResearchFormerly WizWand

Formal Theorem Proving on miniF2F Isabelle (val)

57Success RateLEGO-Prover*
-2.1770413.1862328.549543.91277Oct 21, 2022Dec 17, 2022Feb 13, 2023Apr 11, 2023Jun 8, 2023Aug 4, 2023Oct 1, 2023
Updated 8mo ago

Evaluation results

MethodLinks
LEGO-Prover*LLM=ChatGPT, Attempts=100, Cumulative pass rate=true2023.1057
LEGO-Prover (human informal proof)LLM=ChatGPT, Attempts=100, Informal proof source=human-written2023.1055.3
LyraInformal proof source=Human, Attempts=2002023.0955.3
LyraInformal proof source=GPT-4, Attempts=2002023.0954.9
LyraInformal proof source=GPT-4, Attempts=1002023.0952.8
LEGO-Prover (model informal proof)LLM=ChatGPT, Attempts=100, Informal proof source=model-generated2023.1052.4
LyraInformal proof source=Human, Attempts=1002023.0952
LEGO-ProverLLM=ChatGPT, Attempts=50, Note=Ablation setting2023.1050.4
Subgoal-based Demonstration LearningVariant=Full Method, Protocol=Cumulative pass rate2023.0548
Subgoal-LearningLLM=ChatGPT2023.1048
Subgoal-LearningAttempts=1002023.0948
Subgoal-based Demonstration LearningVariant=Remove Diffusion2023.0547.5
LEGO-Prover without Skill LibraryLLM=ChatGPT, Attempts=50, Skill Library=removed2023.1047.1
Subgoal-based Demonstration LearningVariant=Remove Subgoal, Protocol=Cumulative pass rate2023.0544.3
DSPModel=540B Minerva2023.0542.6
Draft, sketch, and ProveLLM=Codex2023.1042.6
Draft, Sketch, and Prove (DSP)Informal proof source=Human, Attempts=1002023.0942.6
Draft, Sketch, and Prove (DSP)Informal proof source=540B Minerva, Attempts=1002023.0942.6
Subgoal-based Demonstration LearningVariant=Remove Subgoal & Diffusion2023.0541.8
Thor + expert iterationExpert Iteration=True2023.0537.3
Thor + expert iterationLLM=Codex2023.1037.3
ThorExpert iteration=true2023.0937.3
Thor2023.0528.3
ThorLLM=N/A2023.1028.3
Thor2023.0928.3
Sledgehammer+heuristicHeuristic=True2023.0518
SledgehammerHeuristic tactics=true2023.0918
Sledgehammer2023.059.9
Sledgehammer2023.099.9
Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=62B2022.100.439
Draft, Sketch, and ProveInformal proof source=Human2022.100.426
Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=540B2022.100.426
Draft, Sketch, and ProveInformal proof source=Codex2022.100.406
Draft, Sketch, and ProveInformal proof source=Minerva, Model scale=8B2022.100.406
Draft, Sketch, and ProveInformal proof source=Human, Ablation=without informal proofs2022.100.389
Draft, Sketch, and ProveInformal proof source=Human, Ablation=without in-line comments2022.100.377
Thor + expert iterationType=Baseline2022.100.373
Draft, Sketch, and ProveInformal proof source=Human, Ablation=without automated provers2022.100.328
ThorType=Baseline2022.100.283
Sledgehammer + heuristicsType=Baseline2022.100.18
SledgehammerType=Baseline2022.100.099