docs(skills): extend coarse weak-point independence check to Pattern 3#723
Open
kunyuan wants to merge 33 commits into
Open
docs(skills): extend coarse weak-point independence check to Pattern 3#723kunyuan wants to merge 33 commits into
kunyuan wants to merge 33 commits into
Conversation
Coarse's independence check was scoped to Pattern 1c (derived-premise redundancy) and the shared-factor rule only covered same-conclusion weak points. A paper-grounded independence audit of three baseline packages found pervasive Pattern 3 violations — 6 shared-cause groups over 14 of 21 leaf premises, all CROSS-conclusion (e.g. a small-sample-size limit that both caps a diversity estimate and weakens an LD test; three weak points all driven by one TGA-MS measurement). Those leaves are modelled as independent priors, so BP double-counts the shared uncertainty. Extend the "Shared-factor weak points" section to cover the cross-conclusion case, respecting coarse's constraints: do NOT feed one shared-factor claim into multiple derives (that triggers the deduction fan-out penalty and breaks the weak-point ↔ one-conclusion discipline); instead keep each weak point bound to its conclusion, record the shared cause in an independence note, and calibrate priors so the shared risk is not counted at full independent strength per conclusion. Add a Phase-Completion gate item. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…points The Pattern 3 scan was framed around weak points alone, but independence is a property of every evidential factor entering a conclusion's warrant. Highlights (reasons to credit) share latent causes just as weak points (reasons to doubt) do. Broaden the scan to the full factor set and add the two missing sharing kinds: two highlights sharing a cause double-count credit (state the strength once in the warrant prose); a weak point and a highlight sharing a cause use one factor to both doubt and credit (net it out and count it once, coherently). Update the Phase-Completion gate item to match. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
… same/cross split The same-conclusion vs cross-conclusion split was a workaround for the deduction fan-out penalty, which was resolved on 2026-04-13 via directed implication factors (the conclusion no longer sends a backward modus-tollens drag to a shared antecedent). With that fixed the workaround is obsolete and was letting a since-fixed engine artifact distort the knowledge model. Replace it with the principled, conclusion-agnostic rule: scan the whole factor set (weak points AND highlights) globally; near-duplicates merge; a genuine shared cause is extracted to one claim and premised into every conclusion it bounds — BP-visible, not bound to one conclusion with the rest demoted to a working-notes also_threatens note. Update the gating question, the shared-factor section, the Phase-4 emission rule, the working-notes schema (conclusion_ids list + shared_cause), and the completion gate to match. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…, not bare extract Extracting only the common cause discards what each factor asserts beyond it. State the operation as a decomposition: pull the shared cause out as one claim C (one prior, premised into every conclusion it bounds), and keep each factor's residual — what it asserts given C — as its own claim, conditionally independent given C and listed only in its own conclusion. Each conclusion's derive then carries both C and its residual. The merge case is the degenerate one where a factor has no residual. Update the shared-factor section, the completion gate, and the Phase-4 emission rule to match. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…shared Plan B: put the decompose-based shared-factor handling in the canonical _shared/formalize-independence.md (used by both formalize-coarse and formalize-fine) and have coarse reference it. Key correction: do NOT delete or rewrite-away the original premise when splitting a shared cause — it may be the conclusion of another reasoning step or a premise of several derivations, and deleting it breaks those references. Use decompose(original, parts=[shared_cause, residual], formula=land(...)): the original is kept as the `whole`, the shared cause and residual become the atomic prior-bearing leaves, and the shared cause is reused as a part across every original that shares it (correlation enters once). Both the shared cause and each residual are new standalone claims and must be rewritten self-contained. - _shared/formalize-independence.md: add "Decompose, do not delete the original" under Pattern 3 (canonical; fine inherits via its Pass 5 reference). - coarse phase-2: carve out decompose as the one exception to the reduced-DSL "derive only" rule, for the Pattern 3 case. - coarse phase-3: shared-factor section + completion gate now prescribe decompose-preserve + self-contained cause/residual. - coarse phase-4: add decompose to the primitives table and a dedicated emission step; renumber. - coarse SKILL.md: Pattern 3 exception to "two claim kinds only". Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Per the intended model: a weak point and a highlight are the SAME kind of leaf premise — both are non-trivial propositions the conclusion's derivation rests on, both emitted as a claim in the conclusion's given=[] with a register_prior. The only difference is the prior magnitude (weak point lower, highlight higher) plus a weak_point / highlight tag. A highlight is extracted because it is non-trivial and worth making explicit and reviewable, not to raise belief — as a high-prior premise it is near-inert in BP, which is fine. Reverses two prior decisions: - highlights are no longer "working-notes only / folded into rationale"; they are leaf-premise claims like weak points (SKILL.md invariant, Phase 3 goal + body-writing rule + schema + completion gate, Phase 4 primitives table + emission + label minting + module example). - the prior 0.9 cap and the fixed [0.001, 0.9] range are removed; the reviewer judges each prior on its merits, bounded only by BP validity (~0.001 / ~0.999). Added a 0.90-0.999 band where most highlights land. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…enough p1 (sufficiency) and p2 (necessity) were reviewer working-notes that BP never consumes: register_prior(claim, value) takes only the single prior, and coarse's premise→conclusion link is the deterministic derive implication, not a soft conditional, so there is nowhere for p1/p2 to enter inference. They were dead scaffolding. Remove them from the calibration section, the working-notes schema (weak points + highlights), the calibration sanity check, the Phase 1b note, and the completion gate. The reasoning they carried is kept in prose: necessity in the `failure_mode` field, sufficiency in the derive `--rationale`. Each leaf premise now carries exactly one number — `prior_probability` → `register_prior`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
… artifact The Phase 1/2/3 "Working Notes Schema" YAML blocks mirrored what the Gaia DSL already expresses, then Phase 4 re-serialized them to DSL — a redundant double representation now that Phase 4 emits DSL directly. Remove all three schema blocks. The analysis phases hold their output in context (no intermediate YAML/JSON) and Phase 4 emits the package directly. Reviewer reasoning, the only thing the schema held that the DSL did not, is folded into the DSL's own prose: weakness_reason + failure_mode into the register_prior justification, credit + synthesis narrative into the derive rationale. The justification/rationale strings ARE the reasoning; there is no separate stored field. Single source of truth: the Gaia DSL package. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…w fixes Phase 1b queried LKM during formalization, which is backwards: formalization is a paper -> package transformation, while LKM is the downstream graph aggregated from already-formalized packages. Querying it mid-formalization is circular, non-idempotent, and breaks benchmark determinism. Remove it entirely — the LKM-driven route is the separate gaia-lkm-explore client. - Delete the 122-line "Phase 1b — LKM Reverse-Provenance Trace" section from phase-3 and its completion-gate item. - Strip Phase 1b from SKILL.md: frontmatter, progressive workflow, the source-of-truth invariant's exception clause, responsibility boundaries (add an explicit "does not query LKM" boundary), reference files, and the LKM-CLI sibling-skills bullet. Drop the now-unused lkm_id mention. Whole-skill review fixes alongside: - "Two claim kinds only" + "One deduction" invariants now say leaf premise = weak point OR highlight (was weak-point-only, contradicting the unified-leaf-premise invariant). - phase-2 premise-union likewise. - drop the stale "(schema below)" pointer (the working-notes schema was removed) and the redundant bullet it sat in. - `--rationale` CLI-isms -> `rationale=` (Phase 4 writes DSL directly); stale "Step 4a" cross-reference dropped. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
With Phase 1b gone, coarse is purely paper -> package and has no reason to point at the LKM-driven route. Remove the gaia-lkm-explore mentions from the frontmatter, the mission sibling description (now contrasts with formalize-fine only), and the sibling-skills section (deleted — it held only that bullet). Keep the "does not query LKM" responsibility boundary but state it without naming the other tool. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…sions
Per the principle that only premises get priors: a conclusion never
carries a register_prior — its belief propagates through its derive from
the premises. The only case that violated this was the "isolated
conclusion" fallback (a root with no upstream and no leaf premise getting
a direct prior). Forbid it: an isolated conclusion is impossible — every
conclusion rests on something.
- Phase 2: every conclusion's given must include ALL upstream conclusions
it depends on (per the logic graph); a root with no upstream defers to
Phase 3 for >=1 leaf premise. Gate item added.
- Phase 3: every conclusion must leave the phase with >=1 premise; a root
with no weak point gets >=1 supporting highlight. Drop the per-conclusion
synthesis prior NUMBER (only ever consumed for isolated conclusions);
keep the synthesis narrative (it feeds the derive rationale). Gate adds a
"no isolated conclusion" check.
- Phase 4: register_prior for leaf premises and nothing else; one derive
per conclusion (every conclusion); self-check item 1 verifies no isolated
conclusion (gaia inquiry review catches orphans at hand-off).
- SKILL.md invariants updated ("one deduction per conclusion; no isolated
conclusions"; "only leaf premises carry priors").
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…af premises Make the premise-assembly order explicit (it matches the pass order and reads naturally, though BP is order-insensitive): build a conclusion's given=[...] as the upstream conclusions it depends on first (Phase 2 inputs, in topological order), then the weak points and highlights surfaced while reasoning (Phase 3 additions). Updated the SKILL.md invariant and the Phase 4 deductions step; the module example already follows it. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The skill leaned on docs/for-users/*.md paths for the DSL surface (verbs, body discipline, label rules, layout). Those are docs-tree paths that the agent may not have at runtime and that can drift from the installed gaia-lang version. Point at the runtime-accessible, version-matched source instead: - `gaia sdk` — the canonical DSL surface (writes a self-contained SDK reference + cheat sheet); read it before emitting. - `gaia pkg scaffold` / `add-module` — package layout (run them). - `gaia <cmd> --help` — per-command CLI reference. Updated the Mission, the package-shape responsibility boundary, the reference-files section (now "Gaia DSL surface and CLI"), and the Phase 4 goal + label-rules pointer. The fuller docs/for-users docs are kept only as an optional "deeper reference when in the repo" note; the skill relies on `gaia sdk`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…workflow Replace the "analyze in four global phases, dump the package in phase 4" model with an incremental build, per the intended workflow: 1. suitability gate 2. scaffold the package + one module per section 3. write the conclusions (claims) into their modules + motivation + open questions — conclusion claims only at this point 4. organize the logic graph over the written conclusions 5. per conclusion (topological order): emit its weak points + highlights (leaf premises) and its derive (given = upstream conclusions then leaf premises); compile-check the module 6. finalize: global Pattern-3 decompose, priors.py, references.json, full compile, self-check, hand-off The phase docs keep their methodology bodies but are reframed as references for the steps (not sequential passes): phase-1 = steps 3-4, phase-2 = the derive in step 5, phase-3 = weak/highlight in step 5 + independence in step 6, phase-4 = the emission mechanics across steps 2/3/5/6 (relabelled "Workflow step N" + finalize 6a-6f to avoid colliding with the workflow step numbers). Self-review fixes folded in: removed all stale "Phase N" / "four-phase" / "Phase 4 writes files" language; fixed a contradiction (a shared-factor bullet still called highlights "working-notes folded into rationale" — they are leaf premises now, decomposed like weak points); renamed the phase doc titles and the "Holding Phase N output" sections. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The pre-paper motivation is framing / context with no truth value, so it maps to note(...), not question(...) — question is for specific unresolved questions (the per-section open-questions output). Emit one note(...) in motivation.py summarising the whole-paper motivation, and emit each section's open questions as question(...) calls in that section's module. Update the SKILL.md workflow, the phase-4 primitives table, and the phase-4 step 3 emission rules. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
In Gaia, an "open question" is a driving research question paired with the
conclusion that answers it — the question(...) records the question, the
claim(...) records the paper's answer. That matches both fine's pass-1
("Driving questions for the source") and the legacy paper-extract
pipeline B (select_conclusion.xml had a per-conclusion <problem>: "该
结论对应的子问题").
The current skill conflated "open question" with "future-work / things
the paper leaves unresolved at the paper level" — a misreading. Fix it:
- Each conclusion gets one question(...) in the same module recording
the research question it answers (atomic conclusion ↔ atomic driving
question), bound <key>_c<id>_q.
- The motivation note (paper-level framing) remains a single note(...)
in motivation.py.
- Paper-stated future-work / unanswered next-steps are not modelled by
the skill — leave them out.
Updated phase-1 Goal item 3, the Open Questions section, the gate, the
SKILL.md workflow step 3, and the phase-4 primitives table + step-3
emission rule.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Walk back the per-conclusion driving-question model from the previous turn — it was the wrong simplification. The coarse skill emits one question(...) at the paper level: the paper's overall open problem (the research question the paper as a whole sets out to answer), placed in motivation.py alongside the motivation note(...). No per-conclusion questions in the section modules. This matches the legacy paper-extract pipeline B's top-level <problem>. Updates phase-1 Goal item 3 + Open Problem section + gate, SKILL.md workflow step 3, and the phase-4 primitives table + step-3 emission rule + intro paragraph. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…en residual leaves
The per-conclusion step 5 didn't state the conceptual order the agent
should follow inside it. Make it explicit:
1. Summarise the reasoning chain (becomes derive's rationale).
2. From the reasoning, identify the upstream conclusions it depends on
(first entries in given=).
3. Surface weak points and highlights as the RESIDUAL load-bearing
factors — what the reasoning rests on beyond what the upstream
conclusions already capture. A factor already represented by an
upstream is not duplicated as a leaf premise (would double-count).
4. Emit the leaf-premise claims and the derive into the module;
compile-check.
Update SKILL.md workflow step 5 + phase-4 step 5 intro. Add a "residual
relative to upstream conclusions" gating question to both weak-point and
highlight gates in phase-3 (weak-point gate now has six checks, not five).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…experiment) Building the evidence chain for a conclusion often surfaces a still- bundled claim that should have been split at extraction — most commonly a theoretical prediction fused with its experimental measurement (or a method fused with its produced value). Make the atomicity re-check the first sub-step of step 5: per _shared/formalize-atomicity.md's "Separate theory from experiment" and "Separate method from result" rules, split the bundled claim into atomic claims now (replacing the module's claim, updating the logic graph), then proceed with each atomic conclusion separately through the rest of step 5. The five sub-steps of step 5 are now: atomicity re-check → summarise reasoning → list upstream conclusions in given= → surface residual weak points and highlights → emit. Updates SKILL.md step 5 and phase-4 step 5. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…es its nature After step 5.1's atomicity split, each atomic conclusion gets its own reasoning chain — the theory atom and the experiment atom never share one trace. Make the chain's content explicit: a theoretical conclusion gets its mathematical / logical derivation; an experimental measurement gets the experimental procedure (setup, instrument, sampling, readout); a computational result gets the method + parameters + numerical run. Updates step 5.2 in SKILL.md and phase-4, and the Goal section of phase-2 (Reconstruct the Reasoning Chain). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The 6-step workflow restructure renamed the legacy four-pass language to workflow steps 1-6, but several "Phase 1/2/3/4" references inside the reference files still talked about Phase N as a step name. Replace them with the current step / file / audit referents. Also: the gate summary said "five gating questions" while the gating sections now list six (the residual check added when no-isolated-conclusion landed), and SKILL.md still said "four analytical passes" / "Phases 1-2 load these from _shared/". One scaffold description placeholder still pointed at "Phase 1 motivation"; now it points at the motivation note.
The skill never said which claims belong in the root __init__.py's __all__. Without guidance the agent leaves the scaffold default __all__ = [], which the engine treats as "export every labeled claim" — so leaf premises (weak points, highlights) and decompose parts leak into the public IR alongside real conclusions. Add a Non-Negotiable Invariant in SKILL.md (conclusions + motivation note + open-problem question are exported; weak points / highlights / decompose parts are not). Add a new finalize sub-step 6c in phase-4-emit-package.md that replaces the scaffold default with the right label list, and a matching self-check at 6f. 6c–6f shift to 6d–6g. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…usions The previous commit (01f3a45) put export guidance in the SKILL invariant + phase-4 step 6c finalize, and recommended exporting the motivation note and open-problem question alongside conclusions. Two problems: 1. Knowing whether a claim is a "main conclusion" is decided at write time (step 3), not at finalize. Deferring the __all__ append to step 6 makes the agent re-walk the conclusions to figure out what to export. 2. Re-checking the engine: gaia author CLI defaults to --no-export for note and to --export for question, but the canonical downstream consumers (gaia register, _manifest, _github README rendering, _inquiry, _dot, lkm_explorer, starmap, gaia-publish, formalize-fine) all assume the exported surface is "the paper's headline conclusions" — neither the framing note nor the research question is a contribution. The earlier commit also claimed empty __all__ is treated as "export every labeled claim" — that's the pkg.exported runtime property's fallback, but the IR generator (compile.py:1881) does the opposite and records exported=False for everything. The IR is what every downstream tool reads, so the runtime property's view is effectively unused. Filed engine inconsistency as issue #724. Rewrite the invariant to "main conclusions are the exported surface" with a brief pointer to #724 for the engine-wide convention question. Move the operational mechanics out of phase-4 step 6c (drop that section) into phase-1 step 3 (a new "Mark each main conclusion in the root __all__" subsection) and phase-4's Workflow step 3 section (the code shape). Reduce 6f self-check to a one-paragraph verification. Renumber 6d-6g back to 6c-6f. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
… conclusion and premise layers Per Mendel/Galileo precedent and the v0.4 paper-extract approach, coarse was too thin: it modelled only derive dependencies between conclusions and treated weak points / highlights as standalone leaf premises. Real papers also state direct logical relations the agent should capture — competing hypotheses that cannot both hold, theoretical predictions that match measurements, exhaustive binary choices, and judgment-bound associations. Without them the graph loses real BP structure (a contradict creates strong coupling that a mere derive cannot). Add the four relation verbs at two layers: - **Conclusion-graph layer (step 4 + step 5.1 atomicity split aftermath)**: surface equal / contradict / exclusive between conclusion pairs (or atomic sub-conclusions); use associate when the strength is reviewer- judged. Methodology + decision table + "what NOT to model" guidance in phase-1 §Relations between conclusions. Workflow step 4 in SKILL.md picks up the new responsibility. - **Premise layer (step 5.4)**: when sweeping each argument-pattern group of premises (measurement / causal / model / …), also check for relations between same-pattern premises. Methodology in phase-3 §Cross-premise relations within a pattern. SKILL.md step 5.4 picks this up. Other supporting edits: - Phase-2 "reduced DSL" statement updated: relations are allowed, no longer just decompose as the lone exception. - Phase-4 step 3 emission section adds the relation code-shape (which module hosts the relation, label rule, no-prior, no-__all__). - Self-check item 7 lists relation labels among the labels that must not appear in root __all__. - SKILL.md "Two claim kinds only" invariant clarifies relation verbs emit internal helper claims (engine-managed), not new propositions the agent has to write. - Fixed two stale step numbers in the same invariant (step-1 -> step-3 conclusion, step-3 -> step-5 leaf premise) while editing through. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Previous commit added equal / contradict / exclusive / associate at the premise layer but used shorthand signatures (no rationale=…). At the conclusion layer in phase-1 §Relations the signatures showed rationale=… in every verb; phase-3 omitted it, making the two layers inconsistent. Worse, premise-level relations need the rationale MORE than the conclusion layer does: a conclusion-level relation typically reflects something the paper itself states, but a premise-level relation is a reviewer assertion on top of the audit material — without a stated reason, it is unreviewable. Add rationale=… to every signature in the bullet list, then a three-part guidance paragraph: name how the reviewer is asserting the relation (not a restatement of the verb), cite the paper-textual evidence in [@key] form (no Eq./Fig./Sec. pointers per the existing invariant), and for associate additionally justify the two conditional probabilities. A relation whose rationale reduces to "they look related" must be rewritten before emit. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…scape hatch
(A) Suitability Gate now routes Bayesian / statistical model comparison
papers to gaia-formalize-fine. Coarse emits only derive (no infer / observe
/ compute / bayes.compare / bayes.model), so a paper whose core contribution
is "Model A beats Model B by Bayes factor / likelihood ratio" loses its
epistemic structure when coarsened. The gate is the *core contribution*,
not the presence of any statistical method — a paper that runs t-tests in
service of an experimental story stays in coarse.
(B) Phase-3 escape hatch for the "paper supplies no premise" corner case.
The no-isolated-conclusion invariant says every conclusion needs ≥1
premise, but real papers sometimes assert load-bearing assumptions
without justification. The honest representation is a `formal` weak point
whose body names the missing justification ("paper asserts X without
derivation / citation / measurement"); this lets the audit close
without inventing support or skipping the conclusion.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The exported-surface prose referenced an unresolved design question and the permissive gaia author CLI default. Both are now settled (curated, per #724) on main, so drop the hedging and stale engine line refs (compile.py:1881, packaging.py:421) and state the rule plainly: root __all__ is the single source of truth, filled at step 3, validated at compile. No change to what coarse puts in __all__ (main conclusions only). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… pass Relation model (premise + conclusion layers): conclusion-level equal/contradict/exclusive/associate discipline (equal guards double counting via shared-cause extraction; associate is the exception); premise relations allowed where genuine (same -> reuse one claim, correlated -> decompose, logical combination -> premise node C = A | B, cross-conclusion contradict/exclusive -> add it); only co-premise contradict/exclusive is incoherent. Package layout: drop the authored/ subpackage (a gaia author CLI artifact) - write flat modules under src/<import>/ and curate the root __all__ directly; gaia pkg scaffold stays only for pyproject + uuid. Clarity/consistency (full section-by-section review): references.json timing; weak_point/highlight/weak_types are advisory metadata; align phase-1 suitability gate with SKILL.md; drop opaque "legacy step 4 / paper-extract pipeline B" refs; fix decompose "only place" wording and a stale section-module __all__ note. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ion relations Prior rule: register_prior goes on every leaf input a conclusion rests on (experimental facts, externally-established theory/predictions, and the audit's weak points/highlights); the paper's own conclusions never carry a prior. Conclusion relations: the derive logic graph is the only structure among conclusions — drop the proactive step-4 scan for equal/contradict/exclusive/ associate (established conclusions don't contradict; a derive dependency re-encoded as a relation double-counts or cycles). The lone exception, an equal between a theory atom and the experiment atom of the same quantity, comes from the step-5.1 atomicity split. A general theorem vs a separate experimental validation has different truth conditions and is not equal'd — they stay two independent conclusions. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…biased) A leaf that is the paper's own newly-proposed proposition with no external support is genuinely 50/50 a priori — set it at maximum entropy (~0.5), not low (as if doubtful) nor high (as if established). Distinct from the 0.40-0.60 "shaky" band: there the reviewer judges the claim weak; here there is simply no prior evidence either way yet. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
phase-4 self-check item 7 stated the rule in prose (export only the main conclusions; never leaves, notes, or questions). An end-to-end smoke had a formalizer ignore it and export the motivation question, an input leaf, and four weak-point leaves -- which trips the benchmark's leaf-exported lint and roughly halves L4 precision. Replace the eyeball check with a runnable assertion over .gaia/ir.json: an exported claim carrying a register_prior is a leaf, and a note/question is never a conclusion, so both fail the check. Engine-level enforcement is tracked in #738.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Coarse's weak-point independence check only handled Pattern 1c (derived-premise path redundancy) and the existing "Shared-factor weak points" rule only covered the same-conclusion case. A new paper-grounded independence audit of the 3 baseline packages found pervasive cross-conclusion Pattern 3 violations:
These leaf weak points are modelled as independent priors, so belief propagation double-counts the shared uncertainty. No other benchmark axis (conclusion F1, conclusion faithfulness, reasoning) catches this — it is a BP-correctness issue in the leaf layer.
Change
Extends the "Shared-factor weak points" section (now subtitled "independence — Pattern 3") to scan the full weak-point set across conclusions, and splits the guidance:
Adds a Phase-Completion gate item. Docs-only; affects
gaia-formalize-coarsePhase 3.Test plan
🤖 Generated with Claude Code