NAF-Bench Leaderboard 🧠

Can a language model follow a specified reading of negation — instead of falling back on its own default?

solver-certified contamination-free (fresh hidden set) JOINT accuracy  ·  GitHub · Inputs · Submit

⬇️ Download all data + submit guide (one zip) train · validation · test (hidden-set inputs) · README with submit steps

What it tests

The word "not" doesn't mean one thing. In law, regulation, and medicine, the intended meaning depends on the reading in force: open- vs closed-world, two- vs three-valued, credulous vs skeptical. NAF-Bench gives a model a small logic program and tells it which reading to use, then checks whether it applies that reading rather than its gut default. Every instance is generated and certified by solvers (SWI-Prolog, a well-founded solver, and clingo), so the answer key is ground truth, and the test set is regenerated with fresh seeds to stay contamination-free.

Each program is asked under four specified readings:

• closed_world (SLDNF / negation-as-failure)
• cred — credulous stable-model: true in at least one answer set
• skept — skeptical stable-model: true in every answer set
• wfs — the well-founded (three-valued) model

Answers are A (definitely yes), B (definitely no), or C (cannot be determined). The primary metric is JOINT accuracy: a program counts only if all four readings are correct — this strips the lucky/vacuous coincidences a per-prompt average would reward.

Subtasks (benchmark versions)

NAF-Bench is generated by one solver-certified pipeline; it has grown through versions. The guess-baseline is what a program-blind constant (best fixed answer per reading) scores — a subtask is only meaningful when models beat it, so this column is the honest test of a version's validity.

The Frontier column is the tell: on v2 even o4-mini (83.3%) scores below the 100% constant — a frontier model loses to a program-blind guess, so the subtask measures nothing. On hard_v3 o4-mini (68.8%) clearly clears the 22.1% baseline, so the subtask is real. That is why hard_v3 is the scored competition; v1/v2 are kept for provenance. (Open models track the same story: 5.8–12.5% on the paper's base set, and no better than the guess on v1/v2.)

hard_v3 is a single set of 77 programs (385 prompts). It keeps the small 3-SAT search tier cnf_n8 but excludes the prohibitively-large instances cnf_n14/cnf_n22 (search spaces of 2¹⁴–2²²): those are not informative — every model just fails or runs out of context — so dropping them makes the cnf condition sharper.

Families: decided/loopy (read the program, resolve a negation cycle), parity/coupled (combinatorial bookkeeping), cnf_n8 (genuine but bounded 3-SAT search), plus a propagation-decidable control.

Live competition — hard_v3 (hidden test set — auto-scored on submission)

Ranked by JOINT % only. The trace-sound % column is auxiliary information, not a ranking criterion: if you submit a trace, we check whether its reasoning commits to the certified query verdict. The check is regex-based and imperfect — a rough approximation of soundness, not a verified proof audit. – = answer-only submission. For closed frontier models (o4-mini, sonnet-5) the trace is the model's visible output only (hidden chain-of-thought is not returned), so their trace-sound can understate and is not directly comparable to the open models.

Reference results — hard_v3 (public dev set)

These are baselines, not a ceiling — initial reference points we measured on the public hard_v3 set (o4-mini is a closed frontier reference; the rest are open-weight). Beat them by submitting to the live competition above.

Values are JOINT accuracy (%) on the public dev set. Decoding: temperature 0 for all, with a per-model token budget large enough to conclude. * Qwen3.6's 1.3 is a non-termination result, not a reasoning score: even at its recommended temperature with a 16k budget it fails to finish ~50% of readings (per-reading it concludes ~49%). On loopy, the open models V4-Flash (19/20) and Gemma4 (16/20) actually beat o4-mini (11/20); o4-mini's edge is the search family cnf_n8.

Data & downloads

Everything flows from one open-source generator, so data is unlimited and contamination-free — the test gold is the only thing held back. Can't reach GitHub (blocked in some regions)? The dataset is also fully on Hugging Face above, or email bqmbill714@gmail.com and we'll send it.

Submit

Run your model on the public inputs, produce a JSONL of {"id": ..., "prediction": "A|B|C"}, add it as submissions/<team>__<subtask>.jsonl and open a PR on GitHub. A GitHub Action scores it against the hidden gold (never public) and updates this board automatically.