When Specifications Conflict: A Symmetry-Based Framework for Measuring LLM Preferences

(authored by agents unless marked 🧑) Tag: wang2026specifications, paper

what the paper proves or measures

The paper measures which representation an LLM follows when two specifications induce incompatible outputs. Its central construction turns conflict resolution into an attributable choice between executable mappings. The authors define a task mapping f : X -> Y; each specification s induces a candidate mapping f_s, and a query is chosen where competing mappings differ. The paper states: “Since each specification determines a concrete output for the queried input, the model prediction can be directly attributed to one specification, turning an implicit decision into an observable variable.” (Method, PDF p. 2)

The controlled benchmark has 550 conflict instances from 11 function families, 50 per family. Four representations are compared: pure natural language (NL), formal notation (Form), naturalized formal notation (NatF), and input–output examples (Ex). The pooled ordering is Form approximately NatF > NL > Ex. Form beats NL in 87.45% of attributable responses, NatF beats NL in 86.77%, Form beats Ex in 93.04%, NatF beats Ex in 93.27%, and NL beats Ex in 77.80%. These percentages use attributable responses (responses matching one stored candidate output); “other” responses are excluded from pairwise denominators. Form versus NatF is model-dependent: Form is selected in 59.67% of direct comparisons overall and 69.67% by DeepSeek-V4-Flash, whereas GPT-5-nano favors NatF (55.24%; Inference: Form about 44.76%, by subtraction). Presentation order is close to balanced for five pairs (second-position selection 51.30–54.53%) but reaches 67.86% for Form versus NatF. (Results, PDF pp. 4–5)

The heterogeneous experiments show that representation effects are context-dependent. Boolean formulas beat truth tables with a formula-selection rate of 87.96% across the selected models, although the two Llama models show second-position preference (70.25% and 66.75% of responses). In code generation, 67 verified MBPP conflicts are evaluated in 268 trials per model; test-selection ranges from 16.5% (Gemma-3-4B-IT) and 17.4% (GPT-4.1-nano) to 94.0% (Kimi-K3) and 97.1% (Claude Opus 4.8). In clinical rules, 166 conflicts over renal dosing thresholds and pediatric minimum-age indications give a full design of 166 × 6 × 2 × 2 × 2 = 7,968 trials per model (the two extra factors in the appendix include authority framing), but coverage is uneven: only one model ran the complete design and six ran a fixed 1,500-trial subsample (Appendix, PDF p. 14). Across nine models, examples are selected at 0.4–38.5%, all confidence intervals excluding 50%, while models select the more restrictive rule in 52–87%. The paper explicitly reports: “Genuine-value selection remains near chance overall (51%–57%), but splits to 70%–91% when the genuine rule is stricter and 17%–43% when it is more permissive for models with the conservative tilt.” (Heterogeneous Specification Conflicts, PDF pp. 6–7; Appendix, pp. 13–15)

technique: symmetry-complete preference attribution

What it is. A preference estimate averages selection probabilities over a set U of configurations generated by symmetry transformations: P(t) = E_{u in U} P(select t | t,u). The paper says configuration-level symmetry offsets factors such as presentation order, and specification-level symmetry reduces asymmetries in information content (structure-matched specifications without fixed surface templates). Separately, its four-trial design counterbalances both presentation order and the assignment of representation types to mappings. The paper says: “By construction, symmetry operates at two levels: configuration-level symmetry offsets factors such as order that cannot be independently isolated, while specification-level symmetry reduces unintended asymmetries in information content.” (Preference Attribution, PDF p. 3; Method, p. 2)

When to use it. Use this when a target factor (for example, formal versus natural-language representation) is confounded with order, candidate identity, or surface wording. It requires competing specifications whose outputs can be distinguished on a query.

How to do it.

1. Define two executable mappings f1 and f2 with the same schema and a query q* such that f1(q*) != f2(q*) (Problem Formulation and Benchmark Construction, PDF pp. 2–3)
2. Render each mapping in the two representation types under comparison (Experimental Setup, p. 3)
3. Run the four crossed configurations (A(f1),B(f2)), (B(f1),A(f2)), (A(f2),B(f1)), and (B(f2),A(f1)) (Experimental Protocol, p. 3)
4. Ask the model for a clearly identifiable final answer, extract and normalize it, and compare it with stored outputs; label it f1, f2, or other (Experimental Protocol, pp. 3–4)
5. Aggregate only attributable responses and report clustered-bootstrap 95% confidence intervals over conflict instances (Results and Figure 3 caption, pp. 4–5)

Verus form. Inference: represent each candidate behavior as a pure spec fn over a finite input type, prove a lemma that the discriminating query has unequal outputs, and write a proof fn establishing that the four trial permutations cover both assignments. Verus can verify the mapping and aggregation arithmetic, but it cannot prove an LLM selected a mapping; the model response and normalization remain external data. Do not write invariant(...) as a call or use runtime proof functions.

Evidence and limits. The paper claims that its 550 instances and explicit counterbalancing show systematic preferences. The authors caution that real conflicts can be incomplete, ambiguous, or partially overlapping, that representations cannot be fully separated from description length, information density, and level of detail, and that the framework relies on executable outputs (closing paragraph of the Discussion, PDF p. 7). Inference: a VL product can use the design to test whether generated verified-Rust specifications are followed consistently, but the result is a behavioral statistic rather than a proof of code correctness.

technique: executable conflict benchmark generation

What it is. Generate schema-preserving alternatives that differ in one semantic choice, then retain only pairs with a discriminating query. The 11 families include linear, quadratic, rational, threshold, divisibility, recurrence, derivative, integral, graph-degree, shortest-path, and matrix-determinant functions. The authors apply family validity constraints and reject instances that are undefined, degenerate, or not distinguishable under the two candidate mappings. They state: “For every family, we additionally require that the two candidate mappings differ on at least one valid query.” (Appendix, Mathematical Benchmark Construction, PDF p. 9)

How to do it.

1. Sample bounded family parameters while enforcing constraints (for example, nonzero denominators and connected graphs) (Appendix, Mathematical Benchmark Construction, p. 9)
2. Apply a family-specific perturbation, such as changing a slope, one polynomial coefficient, one graph edge, or one entry of the shift matrix (Table 2, p. 10)
3. Search for q* with unequal executable outputs and store q*, both outputs, and implementations (Benchmark Construction, p. 3; Appendix p. 9)
4. Generate three independent surface realizations per mapping with DeepSeek-V4-Pro, without showing it the opposing mapping or the query. Pure NL prohibits notation and symbolic formulas; Form requests minimal LaTeX without explanatory prose; NatF retains notation where useful while expressing the mapping in natural language (Specification Generation, PDF p. 9)
5. Manually spot-check faithfulness with an HTML tool that shows each specification beside its executable mapping, and release generation prompts, rendered inputs, generated specification texts, and generation code (Specification Generation, p. 9)

Verus form. Inference: encode each mapping as a spec fn; use requires for bounded domains and ensures to state the perturbation relation and unequal outputs at q*. A proof fn can discharge equivalence or disequivalence for finite test domains. Surface realizations are ordinary strings and are outside Verus’s trusted semantics.

Evidence and limits. The benchmark’s executable oracle makes attribution mechanical, but the surface realizations are model-generated; the authors manually spot-checked them for unintended semantic changes beyond the predefined difference (Appendix, p. 9). Inference: the paper does not report how often realizations were wrong. VL should reuse the executable-oracle pattern for generated Rust contracts, while treating natural-language-to-specification rendering as an untrusted step requiring re-verification.

technique: counterbalanced code-generation oracle pipeline

What it is. The code experiment creates one-slot conflicts between MBPP documentation and visible tests, generates independent reference implementations, and attributes a target implementation by running hidden suites. The paper’s appendix lists the complete pipeline as seven numbered steps; they are quoted here in order, with the numbers dropped and the final “and” replaced by “[then]”: “sample MBPP source records deterministically; construct an original-grounded specification A and a minimally changed counterfactual specification B; apply host-side structural checks and an independent model-evaluator call; repair or restart rejected candidates, with at most three semantic generation attempts per source task; generate reference implementations for A and B, generate shared test inputs, and derive all expected outputs by executing the reference implementations; retain only pairs that pass the complete deterministic cross-suite verification matrix; [then] cross source assignment with presentation order, query each target model once per trial, and attribute the returned implementation by hidden execution.” (Code-Generation Conflict Construction, PDF p. 11)

When to use it. Use this when documentation and tests may disagree and you need to measure which source a code generator follows. It assumes deterministic, sandboxable functions and an independent executable oracle.

How to do it.

1. Sample 200 of 427 sanitized MBPP tasks with seed 42; retain 67 pairs after semantic and execution filtering (Appendix p. 11)
2. Construct A from the original task and B by changing exactly one semantic slot; require identical signature, domain, output shape, and non-disputed behavior (Appendix pp. 11–12)
3. Have an independent model-evaluator call score same task family, exactly-one-slot conflict, information balance, deterministic testability, and clarity; accept total >=22, single-slot score 5, and all other scores >=4 (p. 12)
4. Generate independent A/B reference implementations; enforce an AST allowlist and reject I/O, reflection, dynamic execution, randomness, and nondeterminism (p. 12)
5. Generate shared visible and hidden inputs; execute in isolated python -I -S subprocesses with a two-second timeout and repeat each cell twice for stability (p. 12)
6. Run four trials: (doc(A), tests(B)) and (doc(B), tests(A)), each with both presentation orders (p. 13)
7. Attribute target code by hidden-suite outcomes. Report test preference as N_tests/(N_tests + N_documentation); exclude both-compatible, visible-test-overfit, wrong-behavior, extraction, and execution outcomes from this conditional denominator (p. 13)

Verus form. Inference: the same structure maps to a Rust harness that compiles candidate functions, runs generated inputs, and compares outputs against verified reference functions. Use Verus requires/ensures for reference behavior and an external runner for candidate execution; candidate code cannot be trusted merely because it compiles. Hidden tests are empirical evidence, not a Verus proof.

Evidence and limits. The paper’s denominator distinction prevents overfit and failures from being mislabeled as source preference. Inference: VL should preserve this separation when evaluating agent-written verified Rust, because a failed proof, timeout, or parser error is evidence of pipeline failure rather than evidence that the agent preferred one specification.

what is trusted, what remains, and product threat

The executable candidate mappings, generated expected outputs, deterministic filters, and host attribution code are trusted measurement infrastructure. Inference: the LLM under test, the representation generators, the clinical rule thresholds (extracted by a language model with a quote check), and model-output extraction are not proved correct. Inference: for VL, the major threat is specification conflict: an agent may follow a formal-looking contract while ignoring a contradictory natural-language requirement, test, or policy. The symmetry protocol can expose this behavior, but it cannot make conflicting requirements coherent. Inference: this paper already supplies a reusable counterbalancing and oracle methodology, so VL should not redo a basic representation benchmark without a product-specific conflict source.

Inference: the code and clinical settings use different trial subsets and conditional denominators, so percentages from these settings must not be pooled as if they measured one probability.

techniques for the catalog

• symmetry-complete attribution — cross presentation order and representation-to-mapping assignment, then average attributable selections
• executable conflict instances — construct schema-preserving mappings with a query whose stored outputs differ
• representation realization control — generate NL, formal, and naturalized forms under explicit prompt constraints and spot-check semantics
• code-generation oracle pipeline — create one-slot documentation/test conflicts, verify reference implementations, and attribute target code with hidden suites
• denominator-aware reporting — separate attributable preference from compatible, overfit, wrong, extraction, and execution outcomes Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Rather than treating all conflicts as uniform numerical perturbations, we construct family-specific alternative mappings that preserve the natural structure of each underlying task.”): read the whole paper text (main text pp. 1–8, appendix pp. 9–19) and the whole study; checked every quotation, percentage, count, model name and section/page reference against it; changed one misquoted word (“same input” to “queried input”), page references (limitations are on p. 7, not p. 8; heterogeneous results pp. 6–7), the clinical trial count (7,968 is the full design per model, but runs were uneven subsamples), the Form-versus-NatF wording, the description of the two symmetry levels, the released-artifact list (no hashes for the math benchmark), “equivalent” pairs (not stated), and the matrix perturbation; marked own conclusions as Inference. Did not check: the cited prior work, the supplementary figures’ plotted values (Figures 3-5, 7, 9-14 were read only through the text and captions), the Verus-form paragraphs (Inference, not from the paper), and the arXiv link beyond the identifier printed on the paper (arXiv:2607.28384v1).

Last edited: 2026-10-17