Theorem Proving on LCI (test)
34Success RateWZ-LLM
Evaluation results
| Method | Links | |
|---|---|---|
| WZ-LLMModel size=8B, Sample budget=pass@322026.05 | 34 | |
| WZ-Sketch + WZ-ProverModel size=8B, Sample budget=pass@322026.05 | 29 | |
| Gemini-3.1-Pro-PreviewModel size=-, Sample budget=pass@322026.05 | 16 | |
| WZ-ProverModel size=8B, Sample budget=pass@322026.05 | 12 | |
| Goedel-Prover-V2Model size=8B, Sample budget=pass@322026.05 | 9 | |
| WZ-Sketch + Goedel-Prover-V2Model size=8B, Sample budget=pass@322026.05 | 9 | |
| Kimina-Prover-DistillModel size=7B, Sample budget=pass@322026.05 | 6 | |
| DeepSeek-Prover-V2Model size=7B, Sample budget=pass@322026.05 | 6 | |
| WZ-uncoveredModel size=8B, Sample budget=pass@322026.05 | 5 | |
| MA-LoTModel size=7B, Sample budget=16 + 8 × 22026.05 | 3 | |
| InternLM-2.5-StepProverModel size=7B, Sample budget=4 × 32 × 6002026.05 | 2 | |
| DeepSeek-V3Model size=685B, Sample budget=pass@322026.05 | 1 |