QMFOLBench: leaderboard
Deductive reasoning benchmark in monadic first-order logic (QMFOLBench, Zheng et al., Huazhong University of Science and Technology, 2026): 2,880 generated tasks with controlled proof depth, width and distractor rules, written in natural language about four topics and verified by round-trip translation and an automated theorem prover. From shuffled premises the model labels a conclusion True, False or Unknown (960 tasks per label); the score is Macro-F1 over the three labels in percent, and higher is better.
Metric: Macro-F1 (%; True, False and Unknown labels, 2,880 tasks). Source: arxiv.org. Saturation forecast: Estimated already saturated. 8 models tracked.
Top models
| # | Model | Score | Overall rank |
|---|---|---|---|
| 1 | Gemini 3.1 Pro (Preview) (High) | 99.03 | #91 (Gemini 3.1 Pro (Preview)) |
| 2 | GPT-5.4 (High) | 97.4 | #121 (GPT-5.4) |
| 3 | Qwen 3.5 27B (Thinking) | 92.19 | #358 (Qwen 3.5 27B) |
| 4 | DeepSeek V3.2 (Thinking) | 90.77 | #403 (DeepSeek V3.2) |
| 5 | Claude Sonnet 4.6 (Thinking) | 79.7 | #158 (Claude Sonnet 4.6) |
| 6 | DeepSeek V3.2 (Non-reasoning) | 76.27 | #403 (DeepSeek V3.2) |
| 7 | Qwen 3 32B (Thinking) | 63.29 | #960 (Qwen 3 32B) |
| 8 | GPT-5.4 (Non-reasoning) | 55.08 | #121 (GPT-5.4) |
No result here: #1 Claude Fable 5.2, #2 Gemini 4 Carbon, #5 Claude Opus 5.5.
Interactive version: theaggregate.ai/benchmark?slug=qmfolbench · How It Works · Data refreshed daily, snapshot 2026-11-12.