Design docs missed quality and efficiency targets in retrieval

Retrieval · 400k-line codebase · 5 questions · z3-checked algebra · Result: not supported

Question: Do algebraic design docs improve coding agents' quality, token use, or time against no supplied docs and prose docs?

Before a planned change, the agent explained one part of a large application. Neither design form met the retrospective +0.1 correctness target and reliably saved tokens and time. With gpt-6-sol both forms used more tokens on most questions, while with gpt-6-luna Prose docs used fewer on every question.

Results at a glance

RunArmAverage scoreStages comparedTokensTime
E022 · gpt-6-sol · mediumNo docs0.934 (best in run)5 of 51.23M (best in run)0:09:31 (best in run)
Prose docs0.906 (−0.028)1.56M (+26%)0:09:32 (+0.2%)
Algebraic docs + z30.892 (−0.042)1.51M (+22%)0:09:51 (+3%)
E023 · gpt-6-luna · mediumNo docs0.8005 of 51.35M0:07:14
Prose docs0.820 (+0.020) (best in run)1.05M (−22%) (best in run)0:07:53 (+9%)
Algebraic docs + z30.720 (−0.080)1.23M (−8%)0:06:56 (−4%) (best in run)

Scores average the stages every arm of the run scored: the stages compared. Tokens and time are each run’s builder totals over every stage it worked. Brackets compare with No docs. Highlighted values mark the highest quality score and lowest recorded tokens, time, and Python CC within each run; ties share the highlight. This does not mean the success rule passed.

What changed in this condition

The agent builds nothing. Each stage asks it one question about a part of an existing application inside about 400,000 lines of vendored code: what the part is, what it must keep true, and how a planned change should go. Every arm gets the same instruction: write the answer to the file the prompt names, and change nothing else. The arms differ only in the design records already in the workspace. Each run uses a different builder model, to test the result at different model sizes.

Control

No docs

The code alone. No design records.

Comparison

Prose docs

The application’s finished design, in prose.

Hypothesis arm

Algebraic docs + z3

The application’s finished design in algebra, with its z3 proof files.

Runs: 2 (E022, E023), one per builder model.

  • E022: gpt-6-sol · medium
  • E023: gpt-6-luna · medium

Agent harness: codex-cli. Judge: claude-opus-5-5-high.

Stage evidence

Not supported. Each part of the rule must hold in every run.

Stages:

  1. checks
  2. ontology
  3. operation
  4. telemetry
  5. composition
RunArmMet12345
✗ Algebraic docs + z3 and Prose docs must each score at least 0.1 above No docs in every graded stage, in every run: not met
E022 · gpt-6-sol · mediumAlgebraic docs + z30 of 5−0.07−0.07−0.04−0.07+0.04
E023 · gpt-6-luna · mediumAlgebraic docs + z30 of 5−0.04−0.07−0.18−0.07−0.04
E022 · gpt-6-sol · mediumProse docs0 of 5−0.030.00−0.110.000.00
E023 · gpt-6-luna · mediumProse docs1 of 5+0.03−0.07−0.11+0.22 ✓+0.03
✗ Algebraic docs + z3 and Prose docs must each use fewer tokens than No docs in most stages, in every run: not met
E022 · gpt-6-sol · mediumAlgebraic docs + z31 of 5−7% ✓+36%+18%+64%+6%
E023 · gpt-6-luna · mediumAlgebraic docs + z33 of 5−20% ✓+16%−33% ✓+1%−2% ✓
E022 · gpt-6-sol · mediumProse docs0 of 5+9%+63%+34%+9%+25%
E023 · gpt-6-luna · mediumProse docs5 of 5−12% ✓−43% ✓−21% ✓−42% ✓−2% ✓
✗ Algebraic docs + z3 and Prose docs must each use less time than No docs in most stages, in every run: not met
E022 · gpt-6-sol · mediumAlgebraic docs + z32 of 5−24% ✓+11%+1%+32%−4% ✓
E023 · gpt-6-luna · mediumAlgebraic docs + z31 of 5+31%+5%−37% ✓+2%+8%
E022 · gpt-6-sol · mediumProse docs3 of 5−15% ✓+28%+23%−20% ✓−9% ✓
E023 · gpt-6-luna · mediumProse docs2 of 5+26%+32%−30% ✓−5% ✓+43%
✓ Algebraic docs + z3 must use fewer tokens than Prose docs in most stages, in every run: met
E022 · gpt-6-sol · mediumAlgebraic docs + z34 of 5−15% ✓−16% ✓−12% ✓+51%−16% ✓
E023 · gpt-6-luna · mediumAlgebraic docs + z33 of 5−10% ✓+102%−15% ✓+75%−0.4% ✓

Each cell is the arm’s score minus the other arm’s, or its change in tokens or time at that stage. ✓ marks a stage that meets that part of the rule; Met counts them, of the stages with a value.

Noise. No two runs here repeat the same setup. In this group’s repeated runs, the same arm’s score at the same stage moved by a median of 0.03 and at most 0.11.

Details

Original prediction and revised quality target

The test card names the arms as follows: control is No docs, semantic is Prose docs, algebraic_solver is Algebraic docs + z3; total_tokens is tokens and elapsed_s is time.

Prediction. Each design arm uses fewer total_tokens and less elapsed_s than the control in most stages, and its answer correctness is no more than 0.1 below the control’s. The algebraic arm uses fewer tokens than the semantic arm.

Falsifier. A design arm uses as many or more tokens than the control, or its correctness falls more than 0.1 below the control’s. The harness verdict tests only the correctness floor: supported means the arm’s score is at most 0.1 below the control’s. Tokens and time are compared from the system measurements in the observer.

Measured: Each arm’s judged score at each stage. Quality Δ is the arm’s score minus No docs. A stage meets the quality target at +0.1 or above. Every counted check must pass in every run. The retrieval quality target was applied after the runs; their recorded target was −0.1. The scores and token and time measurements are unchanged.

What went wrong first

In the first run of each experiment, the judge’s copy of the workspace left out the design docs, so it marked the design arms’ citations as missing:

The answer cites design docs under ../docs/design/…, which do not exist in the working directory … those citations were scored as nonexistent paths.

I found this in the judge reports, fixed the grader (c7ac0d7, “Keep the design tree in the retrieval judge’s copy”) and repeated both runs. This page counts only the repeats.

Runs

E022 — gpt-6-sol · medium

Run ID: run-20260924T023130Z-ccbee4e6
Started: 2026-09-24
Harness status: completed

Every arm finished every stage.

E023 — gpt-6-luna · medium

Run ID: run-20260924T023152Z-aa033b06
Started: 2026-09-24
Harness status: completed

Every arm finished every stage.

Limits

  • The two runs used different builder models, so they are not repeats.

Source data

View condition E022-E023 in G001.json. The run IDs above identify the counted runs. See Data and methods for the export method and limits.