LogicSkills - Formal Symbolization (English): leaderboard
Metric: Accuracy (fraction times 100) on 300 formal-symbolization items in controlled English: the model translates one sentence into a two-variable first-order formula with a fixed symbol key, correct when Z3 finds it logically equivalent to the target; greedy decoding, responses normalized by a GPT-4o extractor and checked with the Z3 solver; higher is better. Source: arxiv.org. Saturation forecast: Estimated already saturated. 10 models tracked.
Top models
| # | Model | Score | Overall rank |
|---|---|---|---|
| 1 | O3 | 94 | #121 |
| 2 | Qwen 3 32B (Thinking) | 85 | #424 (Qwen 3 32B) |
| 3 | Qwen2.5-Math-72B-Instruct | 80 | #708 |
| 4 | Gemini 2.5 Flash | 79 | #237 |
| 5 | Claude 3.7 Sonnet | 76 | #241 |
| 6 | GPT-4o | 72 | #333 |
| 7 | Llama 3.1 70B Instruct | 69 | #548 |
| 8 | Phi-4 | 57 | #701 |
| 9 | Llama 3.1 8B Instruct | 14 | #1018 |
No result here: #3 Claude Opus 5.5, #5 GPT-6 Astra, #8 Claude Fable 5.1.
Interactive version: theaggregate.ai/benchmark?slug=logicskills-formal-symbolization-english · How It Works · Data refreshed daily, snapshot 2026-10-11.