FormalRewardBench - Pointwise: leaderboard
Metric: Pointwise accuracy (%): the model scores the correct and the incorrect Lean proof of each item independently, and the item counts when the correct proof scores higher; temperature 1.0, top-p 0.75; higher is better. Source: arxiv.org. Saturation forecast: Around January 2027. 26 models tracked.
Top models
| # | Model | Score |
|---|---|---|
| 1 | Claude Opus 4.5 | 70.1 |
| 2 | Claude Sonnet 4.5 | 62 |
| 3 | Gemini 2.5 Flash | 50.9 |
| 4 | Claude Sonnet 4 | 49.8 |
| 5 | GPT-5.2 | 48.9 |
| 6 | GPT-4o | 44 |
| 7 | GPT-4.1 | 44 |
| 8 | GPT-5.1 | 41.8 |
| 9 | Qwen 2.5 72B Instruct | 39.8 |
| 10 | Qwen 2.5 Coder 32B Instruct | 36.4 |
| 11 | Qwen2.5-Math-7B-Instruct | 8.9 |
Interactive version: theaggregate.ai/benchmark?slug=formalrewardbench-pointwise · How It Works · Data refreshed daily, snapshot 2026-10-07.