PaperlayerView exact revision on arXiv

Source-linked AI summary

Not What You Meant: Can LLMs Follow a Specified Negation Semantics?

Qiming Bao, Agnieszka Mensfelt, Michael J. Witbrock, Kostas Stathis

arXiv:2609.27517v1cs.AI

TL;DR

Negation can mean different things across domains, yet evidence is limited on whether LLMs follow a specified reading rather than a default one. NAF-Bench tests this with solver-certified programs across four semantics. Two frontier models answer every evaluated instance correctly when semantics are named, while following the requested reading remains unsolved below the frontier.

  • Problem

    Different legal, regulatory, and medical settings require different readings of negation, but existing benchmarks do not isolate whether models follow a specified reading when semantics disagree.

    Source: Introduction · p. 1

  • Method

    NAF-Bench generates ground programs, certifies labels under four negation semantics, and tests models with semantics unspecified or explicitly named across control and divergent instances.

    Source: Introduction · p. 1, The NAF-Bench Benchmarking Tool · p. 4

  • Results

    Two frontier models answer every evaluated instance correctly when semantics are named, whereas the open panel is substantially weaker and o4-mini’s errors concentrate on well-founded undefined cases.

    Source: Introduction · p. 2

  • Takeaways & Limitations

    The authors conclude that following the requested reading remains unsolved below the frontier and that their mitigations localize the gap to applying the rulebook.

    Source: Conclusion and Future Work · p. 7

    The instances are synthetic and frontier models are tested on a fixed-complexity cell, so the results do not establish competence over arbitrary programs or real-world tasks.

    Source: Limitations · p. 7

Abstract

from arXiv · show

Negation does not carry a uniform interpretation across domains. In legal, regulatory, and medical reasoning, the intended interpretation depends on the reading in force -- open- versus closed-world, two- versus three-valued, and credulous versus skeptical. We study which reading of negation large language models adopt by default and whether they can override that preference when a different reading is explicitly specified. To this end, we introduce NAFBench, a procedural generator of solver-certified instances spanning four semantic viewpoints: SLDNF, well-founded semantics (WFS), and credulous and skeptical reasoning under stable-model semantics. The generator emits ground normal logic programs with controlled depth, width, and cycle structure. Each program is solved under all four viewpoints using SWI-Prolog, a well-founded semantics solver, and clingo, yielding up to four divergent labels. The programs are then verbalized into natural language under multiple framings and rule orderings that leave the answer invariant. The results expose a consistent gap. Across open-source models, following a specified negation semantics remains unsolved: the strongest models score 59--74% across the four semantic viewpoints, while the weakest score 31--67%. All models are order-sensitive on more than half of logically identical rule shufflings, while the two weaker models frequently overcommit on well-founded "undefined." Two frontier models reach 100% on the main fixed-complexity evaluation set, and a third, o4-mini, is near-perfect, falling only to 81% on well-founded "undefined." Delegating reasoning to a solver, fine-tuning on certified traces, or forcing an explicit three-valued verdict each partly closes the gap.

Introduction

Negation can support different conclusions across legal, regulatory, clinical, and safety settings, so systems must follow the specified reading and recognize when it leaves a conclusion undetermined. NAF-Bench tests this behavior with solver-certified examples and finds a marked gap between frontier and open-weight models.

Introduction

  • The study builds on findings about structural sensitivity, prior-belief effects, growing search spaces, and difficulty abstaining when no determinate answer exists.The cited work describes these patterns as logic inertia and limited reliability when abstention is expected.Source: Introduction · p. 1
  • NAF-Bench addresses the lack of benchmarks that isolate negation reading by making semantics a controlled variable and certifying multiple answers per instance.Earlier benchmarks either detect negation in prose or evaluate reasoning under a fixed, usually implicit, reading.Source: Introduction · p. 1
  • The benchmark generates ground normal logic programs with controlled structure, certifies them under four semantics, and varies framing, language, and rule order while preserving answers.It also varies complexity and label divergence independently and records solver hardness per instance.Source: Introduction · pp. 1–2
  • Two frontier models correctly answer every instance once semantics is specified, while o4-mini reaches 94.8% and the open-weight panel is substantially weaker.o4-mini’s errors concentrate on well-founded semantics, where it identifies undefined cycles but collapses undefined to false.Source: Introduction · p. 2
  • Because the instances are synthetic, the benchmark is regenerable and contamination-resistant, but this comes at some cost to ecological validity.The authors ground its difficulty axes in structures that make real legal, diagnostic, and regulatory rulebooks diverge.Source: Introduction · p. 2

Preliminaries

The benchmark compares four readings of default negation on a shared program syntax, distinguishing operational failure, three-valued undefinedness, and two forms of stable-model entailment. It excludes other treatments of negation from scope.

Preliminaries

  • All four semantic frameworks use normal logic programs with default negation only, excluding classical and double negation so differences reflect how default negation is treated.Rules have a head and body of positive and default-negated literals; the language has no biconditional connective.Source: Preliminaries · p. 2
  • SLDNF treats failure to prove as evidence for negation and is operational and loop-sensitive, while well-founded semantics assigns undefined to atoms founded neither true nor false.The well-founded value can arise for atoms in loops over negation.Source: Preliminaries · p. 2
  • Stable-model semantics may admit zero, one, or many models; credulous entailment requires truth in some model, whereas skeptical entailment requires truth in every model.The credulous/skeptical distinction also corresponds to acceptance modes in abstract argumentation.Source: Preliminaries · p. 2
  • The benchmark leaves a wider literature outside its scope, including classical negation, inconsistency-based treatments, constructive and intensional negation, and approaches to removing contradiction within WFS.Its legal and regulatory narratives draw on applications of abstract argumentation to legal reasoning.Source: Preliminaries · p. 2

The NAF-Bench Benchmarking Tool

NAF-Bench generates ground programs, certifies their answers under four semantic viewpoints, and renders them in varied but answer-preserving forms. Its protocol compares model responses when negation semantics are unspecified, named on an agreeing control, or named on a divergent instance.

The NAF-Bench Benchmarking Tool

  • Each instance pairs a ground program with a query atom and receives solver-certified labels under SLDNF, well-founded semantics, and credulous and skeptical stable-model semantics.The label spaces distinguish SLDNF non-termination and WFS undefined; the four readings coincide on acyclic programs, while the benchmark targets divergence requiring cycles.Source: The NAF-Bench Benchmarking Tool · p. 2
  • Programs vary in negation depth, width, and cycle structure, and are assigned to divergence bins by their certified four-viewpoint signatures rather than by syntax.The generator uses clingo, a WFS solver, and SWI-Prolog; the odd bin has no stable model, making skeptical entailment vacuously true and credulous entailment false.Source: The NAF-Bench Benchmarking Tool · p. 3
  • The generator creates structurally distinct programs within each fixed-depth, fixed-width cell, retaining only re-certified programs with the target signature and removing isomorphic duplicates.It varies query attachments, aggregator counts, fact distributions, guard literals, and rule order.Source: The NAF-Bench Benchmarking Tool · p. 3
  • Programs are verbalized using abstract or narrative templates and tested under framing, language, and ordering changes that preserve the program and certified labels.The generated SLDNF controls terminate under tested orders, while divergent instances reach negative cycles without succeeding or finitely failing; answer changes across orders therefore measure model order-sensitivity.Source: The NAF-Bench Benchmarking Tool · p. 3
  • The benchmark varies nominal complexity and label divergence independently while recording solver effort for each instance and semantic viewpoint.Solver effort includes choice points and conflicts for clingo and fixpoint iterations for WFS; loop budgets replace SLDNF derivation counts on loop instances.Source: The NAF-Bench Benchmarking Tool · pp. 3–4
  • C0 elicits a model’s default reading, C1 tests a named semantics on an agreeing control, and C2 tests the same named semantics on a matched divergent instance.C1 isolates instruction-following from choosing among readings, while C2 forces that choice; their accuracy difference is the quantity of interest.Source: The NAF-Bench Benchmarking Tool · p. 4

Experiments

The experiments evaluate six models on a fixed set of 120 programs, then vary program size, semantic divergence, rule order, framing, and mitigation strategies. Across these tests, open models struggle most when the requested semantics diverges from their default reading, while solver delegation and targeted interventions partly improve results.

E1: Semantic following

  • Claude Sonnet 5 and GPT-5.6 Sol score 100% across all four viewpoints; o4-mini reaches 98–100% on credulous, skeptical, and SLDNF but 81% on WFS undefined, while Qwen2.5-coder scores 59–74% and Llama3-8B 31–64%.The trace audit finds certification-contradicting verdicts in 14–38% of adjudicable open-panel traces, versus none among 724 frontier traces.Source: Experiments · p. 5, Table 1 · p. 5

E2: Divergence bins

  • The weaker models score 78% (Llama3-8B) and 81% (DeepSeek-R1) on the control bin but fall to 30–52% across divergent bins, while Qwen2.5-coder stays at 62–72%.The divergent-bin drop reaches about 50 points without a change in program size.Source: Experiments · p. 5, Table 2 · p. 5

E3: Complexity

  • Accuracy is flat and non-monotone as depth and width increase; after controlling for divergence, their standardized coefficients are −0.024 and −0.006, versus −0.42 to −0.63 for divergence bins.The bootstrap interval for the difference between absolute width and depth coefficients includes zero.Source: Experiments · p. 5, Table 3 · p. 5

E4: Robustness

  • Open models change answers across logically equivalent rule orders on 54–67% of groups and across framings on 23–41%, while frontier order-flip rates are 0–15%.The framing flips occur despite unchanged logic; the open-model rates are 41% for Qwen2.5-coder, 41% for Llama3-8B, and 23% for DeepSeek-R1.Source: Experiments · p. 6, Table 4 · p. 6

E5: Undefined cases

  • On WFS-undefined items, the two weaker models usually give a definite yes/no; Qwen2.5-coder correctly abstains on 91%.For DeepSeek-R1, 80% of audited traces reach an undefined conclusion, but only 26% render it as the scored choice.Source: Experiments · p. 6, Table 5 · p. 6

E6: Solver delegation

  • Translate-then-solve lifts every open model above direct WFS accuracy on 44 programs, but performance remains capped by parseable translations of 44/44, 42/44, and 38/44 programs.The results indicate that applying the specified semantics is a major bottleneck, while translation fidelity remains a limit.Source: Experiments · p. 6, Table 6 · p. 6

E6: Fine-tuning

  • LoRA fine-tuning on solver-certified reasoning yields near-perfect held-out WFS accuracy and 100% divergent accuracy, but gains do not transfer to an unseen abstract framing.On the trained narrative framing, accuracy rises from 18/44 to 40/44 (91%); on the unseen abstract framing it changes from 30/44 to 28/44 (64%).Source: Experiments · p. 6, Table 7 · p. 6

E6: Verification and language robustness

  • A verify-before-answer scaffold improves every open model on the 44-program WFS set, and the pattern persists when programs are rendered in Chinese.Qwen2.5-coder rises from 59% to 82%, DeepSeek-R1 from 62% to 69%, and Llama3-8B from 49% to 62% parsed accuracy.Source: Experiments · pp. 6–7

Related Work

Prior work studies sentence-level negation, logical inference, solver-assisted reasoning, and training interventions; NAF-Bench instead isolates specified negation semantics while preserving formal content across surface variations.

Related Work

  • Sentence-level negation detection is orthogonal to testing whether models apply a specified formal semantics to structured rules.Nguyen et al. (2023) and So et al. (2026) study sentence-level negation understanding.Source: Related Work · p. 7
  • Existing rule-based and reading-comprehension benchmarks fix a single, usually implicit, closed-world reading, while perturbation and scaling studies report brittleness.ProofWriter, PARARULE-Plus, ReClor, and abductive benchmarks address related but different tasks.Source: Related Work · p. 7
  • NAF-Bench varies semantic viewpoint alongside complexity and measures robustness to label-preserving framing, language, and rule-order changes.Its verbalizations range from abstract conditionals to structured narratives and controlled-English interfaces.Source: Related Work · p. 7
  • Unlike end-to-end ASP benchmarks, NAF-Bench holds the program fixed to isolate whether models follow a specified negation semantics when viewpoints diverge.It also uses translate-then-solve as a mitigation baseline.Source: Related Work · p. 7
  • Training research on logical transformations, preference optimization, and structured priors motivates testing whether prompting and fine-tuning across framings improve semantics-following.The cited work includes logic-driven augmentation (Bao et al. 2024), preference optimization (Bao et al. 2026), and structured priors for logic inertia (Bao, Fu, and Witbrock 2025).Source: Related Work · p. 7

Discussion

With semantics unspecified, two frontier models share a coherent default policy that matches none of the four certified viewpoints; naming a viewpoint changes their performance, while open models remain weaker.

Discussion

  • Two frontier models assert a value only when at least one consistent cycle resolution exists and all resolutions share that value; otherwise they decline.They agree on every unspecified item, and no constant-answer baseline reproduces the policy.Source: Discussion · p. 7
  • The shared default matches none of the four certified viewpoints, but both frontier models follow named viewpoints correctly at the evaluated program size.o4-mini instead drops under WFS, mainly by collapsing undefined to false.Source: Discussion · p. 7
  • The open panel is substantially weaker; fine-tuning improves performance without transferring to an unseen abstract framing, while autoformalization remains promising.Source: Discussion · p. 7

Limitations

The evaluation's synthetic instances and fixed-complexity frontier-model setting constrain how broadly its results can be generalized.

Limitations

  • Synthetic instances and fixed-complexity evaluation of frontier models do not establish competence over arbitrary programs.Source: Limitations · p. 7
  • Deeper programs, interacting cycles, other forms of negation, and real-world validation remain outside the study's scope.Source: Limitations · p. 7
  • Trace analysis is approximate because it relies on pattern-based extraction.Source: Limitations · p. 7

Conclusion and Future Work

The paper introduces a solver-certified generator for testing specified default-negation readings and concludes that following the requested reading remains unsolved below the frontier.

Conclusion and Future Work

  • NAF-Bench is a solver-certified generator for testing whether models apply a specified reading of default negation.Source: Conclusion and Future Work · p. 7
  • The conclusion identifies following the requested reading as unsolved below the frontier and says the mitigations localize the gap to applying the rulebook.Source: Conclusion and Future Work · p. 7
  • Future work will expand program complexity, improve trace analysis, and evaluate transfer to real-world legal, medical, and regulatory tasks.Source: Conclusion and Future Work · p. 7

Technical Appendix

The technical appendix documents NAF-Bench’s release and leaderboard, and presents analyses and worked traces examining model answers and reasoning under different negation semantics, including examples involving q and negation cycles. It also covers trace soundness and mitigation strategies, with analyses noting divergence from certified semantics and improved performance from verification and solver-backed translation.

Public leaderboard and released dataset

  • NAF-Bench releases a 77-program, 385-prompt hard set and seed-disjoint train, validation, and test splits, using six solver-certified families that include genuine search problems.A public leaderboard ranks submissions by JOINT; trace-sound is an approximate auxiliary signal, not a ranking criterion. Verify prompts require stating the semantics, assigning atom values, and evaluating the query; translate-then-solve sends a generated program to a certified solver.Source: Public leaderboard and released dataset · p. 10, Mitigation Prompt Templates · p. 13

Default Reading

  • Claude Sonnet 5 and GPT-5.6 Sol share a coherent default pattern, but neither certified reading explains it: WFS and closed-world each match 90 of 120 prompts, yet both require C where the models answer A.Open models vary across and within divergence bins, so no single qualitative default describes the whole panel.Source: Default Reading · pp. 10–11, Table 10 · p. 11, Table 9 · p. 11

Trace Analysis

  • Among correct answers with auditable traces, contradiction rates are 14.0% for Qwen2.5-coder, 22.9% for DeepSeek-R1, and 39.4% for Llama3; none is found for the three frontier models.Unverifiable traces and responses without a derivation are excluded, so these rates apply only to the auditable subset.Source: Table 11 · p. 12, Trace Analysis · p. 12
  • Claude Sonnet 5 and GPT-5.6 Sol are sound on every auditable trace across four conditions; o4-mini is perfect in three readings but scores 74/96 under WFS.The WFS shortfall is consistent with o4-mini collapsing an undefined value to false.Source: Table 12 · p. 12, Trace Analysis · p. 12
  • In odd-cycle cases, nearly all frontier answers are earned, versus 1 of Qwen2.5-coder’s 23 and 0 of Llama3’s 25 correct skeptical answers supported by explicit no-stable-model reasoning.An odd negative cycle has no stable model, making skeptical entailment vacuously true; a correct answer alone may therefore arise without the decisive reasoning.Source: Table 13 · p. 12, Trace Analysis · p. 12

Expanded Mitigation Analysis

  • On 44 WFS programs, verify improves parsed accuracy by 7–23 percentage points, while T2S improves it by 25–36 points and reaches 95% for Qwen2.5-coder.T2S translates the scenario for a certified solver; its remaining errors include failed or incorrect translations. Parsed accuracy excludes unparseable or non-committal responses, which strict accuracy counts as incorrect.Source: Table 14 · p. 13, Expanded Mitigation Analysis · p. 13

Technical Appendix

  • Other traces derive q as true by selecting a consistent x-variable scenario in which cq is true and propagating truth through the t-chain.They also establish wide as true from the p conditions before concluding q is true.Source: Sound · p. 17
  • The appendix gives conflicting outcomes for q: some traces derive it as true, while a Well-Founded-semantics trace concludes it is undefined.The undefined verdict follows from the x-variable cycle leaving cq and downstream t variables undefined.Source: Sound · p. 17, DeepSeek-R1 32B · p. 19
  • Under Well-Founded semantics, the x-variable negation cycle makes cq and downstream t variables undefined, leaving q undefined.The trace specifically says t0 requires undefined t1, so q cannot be determined as true or false.Source: DeepSeek-R1 32B · p. 19

Sound, and Why That Label Is Narrow

  • One trace resolves a four-atom negation cycle as x0 and x2 true, then propagates cq through t7, wide, and the t-chain to conclude q is true.It assumes x3 is false, derives x2 true, x1 false, and x0 true, then checks the remaining dependencies.Source: DeepSeek-R1 32B · pp. 22–23
  • Other traces conclude q is true by tracing its t0–t3 dependencies to an already true t3 or by finding a set of atoms that satisfies the rules.These excerpts present alternative justifications for the same label without specifying a general result about their soundness.Source: Llama3-8B · p. 23
  • In an etrue example, the trace derives x0 and x3, then cq and the remaining t-dependencies, concluding that q is true.The stated derivation uses etrue together with x1 not being true to establish x0.Source: Llama3-8B · p. 24
Loading 2609.27517v1…