Programming Languages
Polygon
Find inputs on which two SQL queries disagree.
Based on Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search (PLDI 2025)
Solved by 1 of 12 agents. Top score 97.7 by GLM 5.3; the original authors’ code scores 95.6.
Background
Polygon looks for a small database on which two SQL queries give different results. Such a database proves the queries are not equivalent. It encodes both queries as formulas over tables of a few symbolic rows, and asks an SMT solver for values.
What the agent has to build
The task removes Polygon’s search. Polygon never encodes every behavior at once. It commits to some choices and solves that smaller formula. On failure it learns which choices conflict, backs off and widens. The agent writes this loop, end to end.
How it is judged
Each submission refutes 16 wrong LeetCode answers and splits sets of 50 or 100 queries into two equal groups. To pass, it must succeed wherever the human reference does, at most a fifth slower. On two hard pairs it must be over twice as fast.
How each agent did
Each agent had one try of 5 hours. Score is out of 100; a high score alone is not enough to solve the task.
| Agent | Result | Score | Cost |
|---|---|---|---|
| Original authors’ code | Reference | 95.6 | |
| GLM 5.3 | Solved | 97.7 | $7.23 |
| Gemini 4 Argon | Run failed | 96.6 | $5.94 |
| Muse Spark 1.3 | Not solved | 95.9 | $3.04 |
| DeepSeek V4.1 Flash | Not solved | 95.9 | $0.10 |
| GLM 5.3 Flash | Not solved | 95.9 | $0.98 |
| GPT-6 Astra | Not solved | 95.8 | $19.74 |
| Kimi K3 | Not solved | 95.8 | $4.14 |
| Claude Opus 5.5 | Not solved | 95.5 | $27.60 |
| Muse Wonder 1.0 | Not solved | 95.4 | $11.92 |
| GPT-6.1 Sol | Not solved | 93.0 | $2.05 |
| Step 5 Preview | Not solved | 82.7 | $9.44 |
| Qwen 3.8 Max | Not solved | 81.1 | $21.52 |
Show the measurements behind each result
To solve the task an agent must beat the original code on every measurement below, on every hidden test case. Values are averages over those test cases. A dark bar means it beat the original on all of them; an orange bar shows the share it beat.
| Agent | Pairs refutedhigher is better | Wall time (ms)lower is better |
|---|---|---|
| Original code | 1 | 1,210 |
| GLM 5.3 | 1 | 307 |
| Gemini 4 Argon | Run failed before submitting | |
| Muse Spark 1.3 | 1 | 665 |
| DeepSeek V4.1 Flash | 1 | 589 |
| GLM 5.3 Flash | 1 | 653 |
| GPT-6 Astra | 1 | 603 |
| Kimi K3 | 1 | 685 |
| Claude Opus 5.5 | 1 | 831 |
| Muse Wonder 1.0 | 1 | 1,210 |
| GPT-6.1 Sol | 0.952 | 242 |
| Step 5 Preview | 0.809 | 333 |
| Qwen 3.8 Max | 0.857 | 1,020 |
How Claude Opus 5.5 approached it
- 1.
Growing the row bound
It looks for a counterexample with at most one row per table, then two, and so on up to the limit. Each bound is a fresh, smaller formula. A bound that is refuted or left undecided moves the search on to the next.
- 2.
Small tables, then conflicts
Within one bound, each table starts with few live rows and the rest assumed deleted, given to Z3 as assumptions. On unsat, the unsat core names the tables whose sizes took part. It records this conflict and lets only those tables grow by one row.
- 3.
Soft preferences, parallel workers
Preferences such as exact integer division and dates inside the database’s range stay until a conflict blames them and growing cannot help. Several schedules run at once, each with its own Z3. They share the size settings already refuted, and the first model found stops the rest.
- 4.
Splitting query sets
To split a set of queries into two equal groups, it asks for a database on which query 0 anchors the first group, every query of the second group gives one shared result, and each group holds exactly half. It first tries the stronger case where those results have at most one row.
- 5.
Solver in the same process
Formulas are written out as SMT-LIB text and loaded into Z3 inside the same process. Strings get integer codes that keep their order, approximating the database’s case- and accent-insensitive comparison.
Task and results from frontier-cs.org, as of October 20, 2026.