Papers with Code · CC BY-SA 4.0

miniF2F-test

아카이브 평가 29건 · 마지막 적재/변경 2026-10-30

평가 기록

과거 수집 기록이며 최신 순위가 아닙니다. 데이터셋 버전·split·실험 조건과 지표 방향이 검증되지 않은 결과는 직접 비교할 수 없습니다. 날짜는 논문 날짜이며 최신 평가일을 뜻하지 않습니다.

표가 화면보다 넓으면 좌우로 스크롤하여 논문과 구현 링크를 확인하세요.

원본 기록 순서 · 순위 미부여
모델	원본 지표·값	논문	구현
Kimina-Prover-Preview	Pass@1 52.94 Pass@32 68.85 cumulative 80.74 ITP Lean pass@8192 80.74 pass@1024 77.87	Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning 2025-04-15	코드 1 · 코드 2
ProofAug	Pass@1 36.5 Pass@100 52.5 cumulative 66.0 ITP Isabelle	Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis 2025-01-30	코드 1
DeepSeek-Prover-V1.5	Pass@32 50.0 Pass@64 50.7 cumulative 63.5 ITP Lean	DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search 2024-08-15	코드 1 · 코드 2
Subgoal-XL	Pass@32 39.3 cumulative 56.1 ITP Isabelle	SubgoalXL: Subgoal-based Expert Learning for Theorem Proving 2024-08-20	코드 1
DeepSeek-Prover	Pass@1 30.0 Pass@64 46.3 cumulative 52.0 ITP Lean	DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data 2024-05-23	연결 없음
Lyra + GPT-4	Pass@100 47.1 cumulative 47.1 ITP Isabelle	Lyra: Orchestrating Dual Correction in Automated Theorem Proving 2023-09-27	코드 1
LEGO-Prover ChatGPT	Pass@100 47.1 cumulative 47.1 ITP Isabelle	LEGO-Prover: Neural Theorem Proving with Growing Libraries 2023-10-01	코드 1
Decomposing the Enigma	Pass@100 45.5 cumulative 45.5 ITP Isabelle	Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving 2023-05-25	코드 1
Evariste	Pass@64 41 cumulative 41 ITP Lean	HyperTree Proof Search for Neural Theorem Proving 2022-05-23	연결 없음
Evariste-7d	Pass@64 40.6 cumulative 40.6 ITP Lean	HyperTree Proof Search for Neural Theorem Proving 2022-05-23	연결 없음
Evariste-1d	Pass@64 38.9 cumulative 38.9 ITP Lean	HyperTree Proof Search for Neural Theorem Proving 2022-05-23	연결 없음
DSP (540B Minerva informal)	Pass@100 38.9 cumulative 38.9 ITP Isabelle	Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs 2022-10-21	코드 1 · 코드 2 · 코드 3
Lean Expert Iteration	Pass@1 29.6 Pass@32 34.5 Pass@64 36.6 cumulative 36.6 ITP Lean	Formal Mathematics Statement Curriculum Learning 2022-02-03	코드 1
GPT-f	Pass@64 36.6 cumulative 36.6 ITP Metamath	HyperTree Proof Search for Neural Theorem Proving 2022-05-23	연결 없음
Thor + expert iteration on autoformalised theorems	Pass@1 35.2 cumulative 35.2 ITP Isabelle	연결 없음 논문 날짜 미기재	연결 없음
COPRA + GPT-4-turbo	Pass@1 30.7 cumulative 30.7 ITP Lean	An In-Context Learning Agent for Formal Theorem-Proving 2023-10-06	코드 1
Thor	Pass@1 29.9 cumulative 29.9 ITP Isabelle	Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers 2022-05-22	연결 없음
Lean GPT-f	Pass@1 24.6 Pass@32 29.2 cumulative 29.2 ITP Lean	MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics 2021-08-31	코드 1 · 코드 2 · 코드 3 · 코드 4
MMOS-DeepSeekMath-7B	Pass@1 28.3 cumulative 28.3 ITP Lean	An Empirical Study of Data Ability Boundary in LLMs' Math Reasoning 2024-02-23	코드 1
ReProver	Pass@32 26.5 cumulative 26.5 ITP Lean	연결 없음 논문 날짜 미기재	연결 없음
LLEMMA-7b	Pass@32 26.2 cumulative 26.2 ITP Lean	Llemma: An Open Language Model For Mathematics 2023-10-16	코드 1 · 코드 2 · 코드 3 · 코드 4
LLEMMA-34b	Pass@32 25.8 cumulative 25.8 ITP Lean	Llemma: An Open Language Model For Mathematics 2023-10-16	코드 1 · 코드 2 · 코드 3 · 코드 4
PACT (reproduced by Thor)	Pass@1 24.6 cumulative 24.6 ITP Isabelle	Proof Artifact Co-training for Theorem Proving with Language Models 2021-02-11	코드 1 · 코드 2 · 코드 3 · 코드 4
COPRA + GPT-4	Pass@1 23.3 cumulative 23.3 ITP Lean	An In-Context Learning Agent for Formal Theorem-Proving 2023-10-06	코드 1
Sledgehammer + heuristics	Pass@1 20.9 cumulative 20.9 ITP Isabelle	Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs 2022-10-21	코드 1 · 코드 2 · 코드 3
Lean tidy	Pass@1 18 cumulative 18 ITP Lean	MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics 2021-08-31	코드 1 · 코드 2 · 코드 3 · 코드 4
COPRA + GPT-3.5	Pass@1 11.9 cumulative 11.9 ITP Lean	An In-Context Learning Agent for Formal Theorem-Proving 2023-10-06	코드 1
Sledgehammer	Pass@1 10.4 cumulative 10.4 ITP Isabelle	Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers 2022-05-22	연결 없음
Metamath GPT-f	Pass@1 1.3 cumulative 1.6 ITP Metamath	MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics 2021-08-31	코드 1 · 코드 2 · 코드 3 · 코드 4