Formal Theorem Proving on miniF2F (Success Rate)
66.31Proof Success RateSegment-level
Evaluation Results
| Method | Links | |
|---|---|---|
| Segment-levelTraining data=NuminaMath-LEAN, Base Model=Qwen2.5-Math-7B2026.05 | 66.31 | |
| Segment-levelTraining data=STP, Base Model=Qwen2.5-Math-7B2026.05 | 64.84 | |
| Whole-proof-segTraining data=STP, Base Model=Qwen2.5-Math-7B2026.05 | 63.52 | |
| Step-levelTraining data=STP, Base Model=Qwen2.5-Math-7B2026.05 | 63.11 | |
| Step-levelTraining data=NuminaMath-LEAN, Base Model=Qwen2.5-Math-7B2026.05 | 63.11 | |
| Whole-proofTraining data=STP, Base Model=Qwen2.5-Math-7B2026.05 | 61.64 | |
| Segment-levelTraining data=LeanWorkbook, Base Model=Qwen2.5-Math-7B2026.05 | 60.9 | |
| Step-levelTraining data=LeanWorkbook, Base Model=Qwen2.5-Math-7B2026.05 | 59.02 | |
| Whole-proofTraining data=NuminaMath-LEAN, Base Model=Qwen2.5-Math-7B2026.05 | 55.9 | |
| Whole-proofTraining data=LeanWorkbook, Base Model=Qwen2.5-Math-7B2026.05 | 54.67 | |
| Whole-proof-segTraining data=LeanWorkbook, Base Model=Qwen2.5-Math-7B2026.05 | 54.51 | |
| Whole-proof-segTraining data=NuminaMath-LEAN, Base Model=Qwen2.5-Math-7B2026.05 | 52.7 |