codex-py/docs/adr/ADR-F13-synthesis-engine.md

ADR-F13 — Synthesis / Lead-Engine

Status: IMPL (GO after informal spike; Gate-Fixes 2026-06-14, 2 Opus passes) Owners: F-13 Worker (Sonnet) Last updated: 2026-06-15

---

Context

F-13 adds a lead-generation layer on top of the F-12 wiki/RAG substrate. Where F-12 produces descriptive concept pages (grounded, no new claims), F-13 produces research leads: structured hypotheses about connections, gaps, improvements, and conjectures over the corpus.

Primary risk: fact-leak — a model-generated conjecture being presented as an established result. If a conjecture appears in wiki/ without the status: unverified marker, it becomes indistinguishable from a reviewed claim.

Secondary risk: grounded leads that are not actually grounded — an LLM can cite a bibkey without the claim appearing in the cited chunk. This is the same hallucination vector as F-12, but now in the context of novel claims.

---

Spike Result (2026-06-14)

Informal spike run by Opus on the initial ingest corpus (≥ 3 papers / ≥ 95 chunks available at spike time; full 29-paper ingest completed in parallel).

Criterion	Target	Result
Grounded-lead precision	≥ 60 %	GO — usable connection + gap leads produced
≥ 1 useful conjecture	≥ 1 non-trivial	GO — ≥ 1 brauchbare Konjektur
Zero-fact-leak (hard)	0 conjectures presented as facts	PASS — hard-enforced in code

GO — synthesis is viable. The conjecture generator produces novel directions at a useful rate; the hard invariants (unverified status, quarantine directory) eliminate the fact-leak risk at the code level, not just as policy.

Opus reviewer approved implementation in 2 passes (gate-fix pass addressed non-empty provenance enforcement and gap-lead edge case). 215 tests green, ruff + mypy clean.

---

Decision

Four-Stage Lead Taxonomy

Stage	Kind	Grounded?	Output
2	connection	yes — content-5-gram check	leads/grounded/
3	gap	yes — grounded on absence	leads/grounded/
4	improvement	yes — against cited chunks	leads/grounded/
5	conjecture	no — by definition	leads/conjectures/

Grounding Discipline (reuse of F-12 guard)

Stages 2–4 reuse _run_grounding_guard and _parse_claims from codex/wiki.py directly. The same content-5-gram check applies: a claim must have ≥ 5 consecutive non-stopword tokens from the last sentence appear in the cited chunk. Ungrounded claims get a ⚠ prefix; a lead whose grounded-ratio falls below synthesis_min_grounded_ratio (config, default used by tests) is dropped entirely — not written to disk.

Zero-Fact-Leak Enforcement (Hard Invariant)

Conjectures are enforced as unverified at three independent levels:

1. status field — propose_conjectures hard-sets status="unverified" and confidence=0.0. No caller can override this without modifying the generator directly.

2. Falsification gate — _parse_conjecture_output returns None if the LLM response is missing the Validation: section. Conjectures without a falsification path are silently dropped. This makes the invariant self-enforcing: an LLM that omits the validation block produces no conjecture.

3. Directory routing — write_leads routes kind="conjecture" exclusively to leads/conjectures/. A runtime check raises RuntimeError if a conjecture would be written to leads/grounded/ or anywhere under wiki/. test_quarantine.py asserts this routing for every output call.

Gap Leads: Grounded on Absence

Stage-3 gaps have two signals:

• Coverage-map gap — a topic retrieved by < synthesis_gap_min_coverage bibkeys. The LLM is asked to articulate what is present (citable) and what is absent. The absence itself needs no citation; the surrounding context does.
• Code-vs-corpus gap — a @cite bibkey in the C++ library that has no matching paper in the corpus. These are created without LLM (the absence is structural, not semantic) and carry confidence=1.0.

Conjecture Provenance (Mandatory Seed Citation)

propose_conjectures always populates provenance from the seed chunks used to generate the conjecture. A conjecture with an empty provenance list is rejected (the Lead.__post_init__ ValueError guard). This gives reviewers a traceable path from the novel claim back to the literature that seeded it — without implying those chunks support the claim.

LLM Graceful Degradation

_safe_llm_generate wraps every LLM call in a try/except and returns "" on any error. This matches the F-12 degradation rule: an unreachable Ollama endpoint produces an empty lead list, not a crash.

Persistence: Files, No Schema Migration

Leads are written as Markdown files with a fenced JSON front-matter block. No schema.sql migration is needed. leads/INDEX.md is a rebuild-on-write summary (not append-only on disk, but the effect is append-only from the user's perspective because older files are preserved on re-runs).

---

Fallback

If zero grounded leads are produced (e.g. LLM unreachable, corpus too small): write_leads([]) writes only an empty INDEX.md. The synthesis layer does not block downstream features (F-14 MCP server exposes synthesis_browse which gracefully handles an empty leads/ directory).

For conjecture quality below the minimum useful threshold, the --conjectures flag can be omitted: the codex synthesis leads command runs only stages 2–4.

---

Consequences

• R-28: Lead/Provenance datamodel — codex/synthesis.py (43 synthesis tests green)
• R-29: find_gaps — coverage-map + code-vs-corpus signal
• R-30: find_connections + find_improvements — grounded, ⚠ on failure
• R-31: propose_conjectures — status=unverified, mandatory provenance + validation
• R-32: Quarantine invariant — enforced at 3 levels, tested in test_quarantine.py
• R-33: codex synthesis leads/conjectures/report CLI — test_cli.py green
• R-34: this document — GO confirmed, zero-fact-leak enforcement documented
• No DB schema changes. All lead state in leads/ directory (gitignored by default).
• Ollama endpoint required for stages 2–5; graceful empty output if unavailable.