Formal Theorem Proving on Combibench
48Solve RateSeed-Prover 1.5
Evaluation Results
| Method | Links | |
|---|---|---|
| Seed-Prover 1.5Compute Budget=10 H20 days / problem2025.12 | 48 | |
| Seed-Prover 1.0 (medium)Compute Budget=18 H20 days / problem2025.12 | 39 | |
| HilbertBackbone=Gemini 3.1 Pro, System=Agentic System2026.04 | 2.05 | |
| Goedel-Prover-V2-8BType=Open-source LLM2026.04 | 1.96 | |
| HilbertBackbone=Gemini 2.5 Pro, System=Agentic System2026.04 | 1.89 | |
| Goedel-Prover-V2-32BType=Open-source LLM2026.04 | 1.31 | |
| DreamProverBackbone=Gemini 3.1 Pro, System=Lemma Learning System2026.04 | 0.93 | |
| DreamProverBackbone=Gemini 2.5 Pro, System=Lemma Learning System2026.04 | 0.75 | |
| Gemini 2.5 ProType=Proprietary LLM2026.04 | 0.64 | |
| Gemini 3.1 ProType=Proprietary LLM2026.04 | 0.59 | |
| HilbertBackbone=GPT-5.3-Codex, System=Agentic System2026.04 | 0.58 | |
| DeepSeek-Prover-V2-7BType=Open-source LLM2026.04 | 0.42 | |
| Claude 4.6 OpusType=Proprietary LLM2026.04 | 0.41 | |
| DreamProverBackbone=GPT-5.3-Codex, System=Lemma Learning System2026.04 | 0.32 | |
| GPT-5.3-CodexType=Proprietary LLM2026.04 | 0.12 |