Automated Theorem Proving on miniF2F-test

60개 결과 · ⬇ CSV · JSON

cumulative

Rank	Model	cumulative	Pass@1	Pass@32	Pass@64	Pass@100	ITP	pass@1024	pass@8192	Extra Training Data	Paper	Code	Year
1	Kimina-Prover-Preview	80.74	52.94	68.85	–	–	Lean	77.87	80.74	✓	Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning	moonshotai/kimina-prover-preview · cmu-l3/llmlean	2025
2	ProofAug	66.0	36.5	–	–	52.5	Isabelle	–	–		Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis	haoxiongliu/proofaug	2025
3	DeepSeek-Prover-V1.5	63.5	–	50.0	50.7	–	Lean	–	–	✓	DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search	deepseek-ai/deepseek-prover-v1.5 · augustepoiroux/LeanInteract	2024
4	Subgoal-XL	56.1	–	39.3	–	–	Isabelle	–	–	✓	SubgoalXL: Subgoal-based Expert Learning for Theorem Proving	zhaoxlpku/subgoalxl	2024
5	DeepSeek-Prover	52.0	30.0	–	46.3	–	Lean	–	–	✓	DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data		2024
6	Lyra + GPT-4	47.1	–	–	–	47.1	Isabelle	–	–		Lyra: Orchestrating Dual Correction in Automated Theorem Proving	chuanyang-zheng/lyra-theorem-prover	2023
6	LEGO-Prover ChatGPT	47.1	–	–	–	47.1	Isabelle	–	–		LEGO-Prover: Neural Theorem Proving with Growing Libraries	wiio12/LEGO-Prover	2023
8	Decomposing the Enigma	45.5	–	–	–	45.5	Isabelle	–	–		Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving	hkunlp/subgoal-theorem-prover	2023
9	Evariste	41	–	–	41	–	Lean	–	–	✓	HyperTree Proof Search for Neural Theorem Proving		2022
10	Evariste-7d	40.6	–	–	40.6	–	Lean	–	–		HyperTree Proof Search for Neural Theorem Proving		2022
11	Evariste-1d	38.9	–	–	38.9	–	Lean	–	–		HyperTree Proof Search for Neural Theorem Proving		2022
11	DSP (540B Minerva informal)	38.9	–	–	–	38.9	Isabelle	–	–		Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs	facebookresearch/minif2f · albertqjiang/draft_sketch_prove · rah4927/lean-dojo-mew	2022
13	Lean Expert Iteration	36.6	29.6	34.5	36.6	–	Lean	–	–	✓	Formal Mathematics Statement Curriculum Learning	openai/lean-gym	2022
13	GPT-f	36.6	–	–	36.6	–	Metamath	–	–		HyperTree Proof Search for Neural Theorem Proving		2022
15	Thor + expert iteration on autoformalised theorems	35.2	35.2	–	–	–	Isabelle	–	–	✓
16	COPRA + GPT-4-turbo	30.7	30.7	–	–	–	Lean	–	–		An In-Context Learning Agent for Formal Theorem-Proving	trishullab/copra	2023
17	Thor	29.9	29.9	–	–	–	Isabelle	–	–		Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers		2022
18	Lean GPT-f	29.2	24.6	29.2	–	–	Lean	–	–		MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics	openai/minif2f · facebookresearch/minif2f · yangky11/minif2f-lean4 · +1	2021
19	MMOS-DeepSeekMath-7B	28.3	28.3	–	–	–	Lean	–	–		An Empirical Study of Data Ability Boundary in LLMs' Math Reasoning	cyzhh/MMOS	2024
20	ReProver	26.5	–	26.5	–	–	Lean	–	–