Statement generation on ProofNet N = 186 (test)
98.4CH@100FormalEvolve (K=1)
Evaluation Results
| Method | Links | ||||
|---|---|---|---|---|---|
| FormalEvolve (K=1)K=1, Repair model=Qwen32026.03 | 98.4 | 86.6 | 0.362 | 19.8 | |
| Hybrid controlArchive=None, Generation model=Kimina-7B, Repair model=Qwen3-30B-A3B2026.03 | 97.3 | 82.8 | 0.505 | 24.1 | |
| FormalEvolve (K=2)K=2, Repair model=Qwen32026.03 | 97.3 | 84.9 | 0.443 | 22.9 | |
| FormalEvolve (K=2; w/o EvolAST)K=2, EvolAST=False, Repair model=Qwen32026.03 | 97.3 | 87.1 | 0.454 | 23.6 | |
| Compile RepairBaselines=Kimina, Archive=None, Model=Kimina-7B2026.03 | 90.9 | 72 | 0.566 | 26.3 | |
| Compile+Semantic RepairBaselines=Kimina, Archive=None, Model=Kimina-7B2026.03 | 90.9 | 78 | 0.555 | 26.4 | |
| SampleBaselines=Kimina, Archive=None, Model=Kimina-7B2026.03 | 90.3 | 71.5 | 0.537 | 24.3 | |
| FormalEvolve (K=2; w/o patch repair)K=2, Patch repair=False, Repair model=Qwen32026.03 | 90.3 | 78 | 0.449 | 21.1 | |
| Qwen3 + Compile+Semantic RepairBaselines=Qwen3, Archive=None, Model=Qwen3-30B-A3B2026.03 | 68.8 | 54.8 | 0.802 | 65.6 | |
| Qwen3 SampleBaselines=Qwen3, Archive=None, Model=Qwen3-30B-A3B2026.03 | 38.7 | 24.2 | 0.896 | 87.6 | |
| Qwen3 + Compile RepairBaselines=Qwen3, Archive=None, Model=Qwen3-30B-A3B2026.03 | 37.1 | 23.7 | 0.912 | 91.1 |