PaperlayerView exact revision on arXiv

Source-linked AI summary

Detecting Inconsistencies in Model Specifications with LLM-as-Verifier Reasoning

Zichen Xie, Mrigank Pawagi, Lize Shao, Yang Hu, Wenxi Wang

arXiv:2610.01847v1cs.SEcs.AIcs.CL

TL;DR

Model specifications guide LLM behavior, but individually reasonable principles may prescribe incompatible actions in the same situation, while formalization can lose natural-language distinctions. VeriSpec preserves the text in context-aware rules and uses an LLM verifier to detect inconsistencies. Applied to the OpenAI Model Spec, it validated five inconsistencies and outperformed five baselines on precision and cost per validated inconsistency.

  • Problem

    Model specifications can contain individually reasonable principles that prescribe incompatible behavior in the same situation, and formal translation risks losing distinctions in natural-language requirements.

    Source: §1 · pp. 1–2

  • Method

    VeriSpec extracts context-aware natural-language rules, clusters behaviorally related rules at the same authority level, and uses an LLM verifier to test for unresolved conflicts in concrete situations.

    Source: §1 · p. 2

  • Results

    On the OpenAI Model Spec, VeriSpec manually validated five inconsistencies and, against five baselines, achieved the highest precision (38.5%) and lowest cost per validated inconsistency ($11.12).

    Source: §1 · p. 2

  • Takeaways & Limitations

    Direct specification auditing can uncover defects in specifications themselves, complementing approaches that evaluate model behavior.

    Source: §6 · p. 10

    Coverage is limited when principles remain unannotated, since omitted principles may be involved in inconsistencies.

    Source: §4.1.1 · p. 5

Abstract

from arXiv · show

Model specifications define how large language models (LLMs) should behave, guiding alignment training, inference-time behavior, and evaluation. Yet these specifications may themselves contain defects: two individually reasonable principles may prescribe incompatible behavior when applied to the same situation, leaving no response that satisfies both. Detecting such inconsistencies is challenging. Formalizing natural-language specifications risks losing subtle distinctions, while behavior-based testing cannot reliably distinguish specification defects from differences in model behavior. We introduce VeriSpec, the first approach to directly detect inconsistencies in model specifications by auditing the specification text itself. Our key insight is to preserve the specification in natural language while using an LLM as a verifier. VeriSpec extracts structured, context-aware rules, constructs a topic-guided graph to cluster behaviorally related rules at the same authority level, and applies LLM-as-verifier reasoning to detect inconsistencies. Applying VeriSpec to the OpenAI Model Spec, we extract 405 rules and manually validate five inconsistencies, all reported to its developers, who responded positively and have initiated internal discussions. Compared with five baselines, VeriSpec identifies the most validated inconsistencies, achieves the highest precision (38.5%), and incurs the lowest cost per validated inconsistency ($11.12). These results establish direct specification auditing as a practical complement to behavioral alignment evaluation, catching defects at the source before they shape any model. The code is available at https://github.com/HIPREL-Group/VeriSpec.

1 INTRODUCTION

Model specifications guide LLM behavior but can prescribe incompatible responses when individually reasonable principles apply together. VeriSpec audits specification text directly, preserving natural-language rules and their context; on the OpenAI Model Spec, it validated five inconsistencies and outperformed five baselines on precision and cost per validated inconsistency.

Motivation

  • Model specifications guide alignment training, inference-time behavior, and evaluation, and are frequently updated as models and deployment expectations change.Source: §1 · p. 1
  • A transformation request for code-only output can conflict: preserving unrequested text may leave code unrunnable, while fixing it changes text the user did not ask to change.The inconsistency arises only when both principles apply to the same situation.Source: §1 · pp. 1–2
  • Formal translation risks flattening modal distinctions, permissions, defaults, exceptions, and soft obligations, so VeriSpec keeps the specification in natural language for verifier reasoning.Manual formalization at full-specification scale also requires substantial expert effort.Source: §1 · p. 2

Approach

  • VeriSpec extracts context-aware natural-language rules, clusters behaviorally related rules at the same authority level, and uses an LLM verifier requiring a concrete unresolved witness situation.The rules preserve source annotation, authority, precondition, postcondition, and interpretive context.Source: §1 · p. 2

Evaluation

  • Five inconsistencies were manually validated in the OpenAI Model Spec; among five baselines, VeriSpec had the highest precision (38.5%) and lowest cost per validated inconsistency ($11.12).All five were reported to the specification’s developers, who responded positively and initiated internal discussions.Source: §1 · p. 2

2 BACKGROUND: OPENAI MODEL SPEC

The OpenAI Model Spec organizes behavioral principles by themes and authority levels, and includes examples illustrating their application.

Organization

  • Principles are organized into thematic sections and may express hard boundaries, defaults, or decision rubrics for gray areas.Concrete examples show how some principles should be applied in practice.Source: §2 · p. 3

Authority levels

  • The authority hierarchy runs from root through system, developer, and user to guideline; higher-level principles take precedence in conflicts.Source: §2 · p. 3

Annotations

  • Focus-area annotations are not officially documented, and some principles lack annotations.The authors note that they address missing annotations in Section 4.1.1.Source: §2 · p. 3

3 RELATED WORK

Prior work evaluates model compliance, studies behavior under competing values, or uses behavioral disagreement to stress-test specifications. VeriSpec instead analyzes whether specification text itself is internally consistent.

Evaluating Model Alignment

  • Prior specification-alignment work measures whether models comply with provider specifications, whereas this paper asks whether the specification itself is internally consistent.Source: §3 · p. 3

Value Conflicts in Model Behavior

  • Value-conflict studies examine how models prioritize competing values; this work asks whether written principles prescribe incompatible behavior before guiding or training a model.Source: §3 · pp. 3–4

Behavior-Based Specification Testing

  • Behavioral disagreement can reflect training, alignment, or capability differences, while defects that models resolve consistently may produce no observable disagreement; VeriSpec audits the text directly.Its reports use structured verifier reasoning and manual validation.Source: §3 · p. 4

4 METHODOLOGY

VeriSpec preserves specification rules in natural language, attaches context, clusters related rules at the same authority level, and uses an LLM verifier to check for inconsistencies.

4 METHODOLOGY

  • The pipeline adds rule context, forms compact same-authority analysis units, and reports a conflict only with a concrete witness and evidence that context does not resolve it.Provider and model references were anonymized with synthetic names, with static checks limiting edits to substitutions.Source: §4 · p. 4

4.1.1 ANNOTATING ALL PRINCIPLES

  • Many principles lack focus-area annotations, limiting coverage; the authors added 126 annotations to bring the total to 405.Source: §4.1.1 · p. 5

4.1.2 TRANSFORMING PRINCIPLES TO RULES

  • Each natural-language rule records its annotation, authority, precondition, and required postcondition, with examples, definitions, and trade-off guidance attached as interpretive context.Source: §4.1.2 · p. 5

4.2 GRAPH-BASED RULE CLUSTERING

  • Topic edges connect rules governing shared behavior, while syntactic edges link document-related rules; same-authority clustering yields 32 analysis units instead of checking over 80,000 pairs.Source: §4.2 · pp. 5–6

4.3 LLM-AS-VERIFIER DETECTION

  • For each unit, the verifier requires a witness, both-rule applicability, joint unsatisfiability, and unresolved context, then aggregates five independent passes for manual review.Source: §4.3 · pp. 6–7

5 EXPERIMENTS

VERISPEC’s evaluation on the OpenAI Model Spec validated five candidate inconsistencies and compared its detection and cost outcomes with five baselines. The results also show that context-aware verification and behavior-based grouping address failure modes of whole-spec and section-based detection.

5.1 EXPERIMENTAL SETUP

  • The setup compared methods over five attempts and assessed reported and validated inconsistencies, precision, total cost, and cost per validated inconsistency.All methods used Claude Opus 5; two reviewers independently judged each reported rule pair, witness, and supporting context, resolving disagreements by discussion and consensus.Source: §5.1 · pp. 7–8

5.2 MAIN RESULTS

  • VERISPEC produced 17 raw reports, consolidated into 13 candidates from 160 detection requests across 32 analysis units; candidates saturated by attempt five.The units came from 405 extracted rules, with five detection runs per unit.Source: §5.2 · p. 8, Figure 4 · p. 8

5.4 VALIDATED INCONSISTENCIES

  • The five validated cases span legal constraints, code transformations, output-only tasks, fictional portrayals, and sycophantic reassurance; Figure 6 presents four beyond the running example.The validated cases came from system- and user-level rules; root- and guideline-level candidates did not survive validation.Source: §5.2 · p. 8, Figure 6 · p. 9, §5.4 · p. 10

5.2 MAIN RESULTS

  • 5 of 13 candidates were validated (38.5% precision); VERISPEC’s $11.12 cost per validated inconsistency was lowest among five baselines.Its total cost was $55.62.Source: §5.2 · p. 8, §5.3 · p. 9

5.3 BASELINE COMPARISON

  • DIRECTAGENT and DIRECTPROMPT validated none, while section-based methods validated only the same-section legal-disclosure case and missed cross-section cases.Section-based grouping thus missed the code-transformation example; the small difference between SECTIONTEXT and SECTIONGROUP suggests source-section grouping adds little over section text alone.Source: §5.3 · p. 9
  • PLAINDETECT validated 3 of 221 candidates (1.4% precision), whereas verifier checks reduced candidates to 13 and raised precision to 38.5%.VERISPEC requires a witness, an unsatisfiability argument, and an argument that context does not resolve the conflict.Source: §5.3 · p. 9

6 CONCLUSION

The paper concludes that VERISPEC can directly detect inconsistencies in natural-language model specifications and finds five validated cases in the OpenAI Model Spec. It frames specification auditing as complementary to evaluating model behavior and argues that specifications themselves should not be treated as unquestioned ground truth.

6 CONCLUSION

  • VERISPEC detects specification inconsistencies through context-aware rule extraction, graph-based clustering, and LLM-as-verifier reasoning.Source: §6 · p. 10
  • The authors propose extending specification auditing toward continuous verification, repair, and incremental checks across model providers.They argue that checking whether models follow specifications is only part of the challenge; the specifications themselves must also be consistent.Source: §6 · p. 10

A RULE INVENTORY CONSTRUCTION

The rule inventory supplements existing annotations while preserving the specification text, with rules retaining links to their source statements and interpretive examples. Annotation criteria, granularity, review, and authority resolution determine which principles enter the inventory and how they are represented.

A RULE INVENTORY CONSTRUCTION

  • A principle is added only when it prescribes assistant behavior in a sufficiently specific situation for compliance to be judged.Requirements, recommendations, prohibitions, and explicit permissions qualify; examples, commentary, definitions, rationales, and statements governing other parties do not.Source: A RULE INVENTORY CONSTRUCTION · p. 12
  • Normative sentences generally remain one principle; sentences are split when policies are separable, while narrowing qualifications stay attached to their principle.Among 26 sentences with multiple annotations, 23 splits were already in the original specification.Source: A RULE INVENTORY CONSTRUCTION · p. 12
  • Reviewers checked for missed principles and over-fragmentation, while static checks ensured completion only added annotations without changing specification text.Extracted rules were checked for one-to-one annotation coverage and links to source statements and examples.Source: A RULE INVENTORY CONSTRUCTION · p. 12
  • Rules inherit authority from the nearest labeled enclosing section; seven rules under unlabeled containers were assigned manually, six to root and one to system authority.The inheritance rule resolved 398 of the 405 rules.Source: A RULE INVENTORY CONSTRUCTION · p. 12

B TOPIC REGISTRY AND RULE GRAPH

The topic registry assigns behavior-related topics to rules to support graph-based analysis units. Small same-authority groups are merged to create analysis units of usable size for verification.

B TOPIC REGISTRY AND RULE GRAPH

  • The topic registry contains 45 leaf topics, built from candidate topics, agreement checks, revisions, and subtopic refinement.Cross-referenced rule pairs shared a topic 7.16× more often than random pairs (permutation test, p ≤0.001).Source: B TOPIC REGISTRY AND RULE GRAPH · p. 13
  • Of 405 rules, 162 received multiple topics; 21 unclear cases were assigned to their closest topic as residue to maintain coverage.Most residue rules concern conflict resolution, which the registry excludes by design.Source: B TOPIC REGISTRY AND RULE GRAPH · p. 13
  • Merging small groups within each authority level produced 32 analysis units from 113 initial authority-and-topic groups.Each merged group had at most 28 nodes; the final units comprised 14 root, 8 user, 8 guideline, 1 system, and 1 developer unit.Source: B TOPIC REGISTRY AND RULE GRAPH · p. 13

C BASELINE IMPLEMENTATION DETAILS

The appendix describes five baselines that vary which VeriSpec components they retain, along with shared run settings and candidate consolidation. It also defines the topic-registry table’s counts.

C BASELINE IMPLEMENTATION DETAILS

  • All methods use Claude Opus 5 for five independent attempts; direct LLM calls use high reasoning effort, while DIRECTAGENT runs through Claude Code.DIRECTAGENT therefore differs from the other baselines in execution, not model.Source: C BASELINE IMPLEMENTATION DETAILS · p. 13
  • DIRECTAGENT and DIRECTPROMPT receive the anonymized whole specification once per attempt, without extracted rules or structured detection fields.DIRECTAGENT uses a fresh Claude Code session to search for inconsistencies; DIRECTPROMPT uses one non-agentic LLM call with the same task instruction.Source: C BASELINE IMPLEMENTATION DETAILS · p. 13
  • SECTIONTEXT removes rule extraction, splitting the specification into 42 second-level-heading units and applying LLM-as-verifier detection to source text.Its prompt retains VeriSpec’s inconsistency definition and authority background; the model identifies statements by quoting them.Source: C BASELINE IMPLEMENTATION DETAILS · p. 14
  • SECTIONGROUP retains rule extraction and LLM-as-verifier detection but groups rules by authority and source section, yielding 39 units covering 399 of 405 rules.Groups with a single rule are skipped because they contain no rule pair to compare.Source: C BASELINE IMPLEMENTATION DETAILS · p. 15
  • PLAINDETECT uses the same extracted rules, contexts, and 32 rule-graph units as VeriSpec, but omits LLM-as-verifier detection and its structured fields.It instead asks for inconsistent rule pairs and a free-text explanation.Source: C BASELINE IMPLEMENTATION DETAILS · p. 15
  • Candidate consolidation removes duplicate reports across attempts and units, then merges reports describing the same inconsistency; the merged candidates appear in Table 1.In the topic registry, leaves counts refined leaf topics, while rules counts assignments and a rule may belong to multiple topics.Source: Table 4 · p. 14, C BASELINE IMPLEMENTATION DETAILS · p. 15
Loading 2610.01847v1…