From 97adbc7b4f14906748b86642490b7569c5ae2995 Mon Sep 17 00:00:00 2001 From: kunchen Date: Fri, 22 May 2026 20:34:53 +0800 Subject: [PATCH] refactor(skills): orthogonalize formalize-coarse and formalize-fine MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The two paper->package formalization skills had grown large overlapping bodies of duplicated methodology. Make them orthogonal: shared methodology lives once in `_shared/`, each skill keeps only its genuine coarse-vs-fine divergence. Shared core — four new `gaia/_skills/_shared/` reference files: - formalize-extract-conclusions.md — what counts as a conclusion, fidelity, self-contained bodies, figures-as-prose, refs whitelist, citation form. - formalize-reasoning-chains.md — logic graph, topological order, reasoning-trace reconstruction, step-writing rules. - formalize-atomicity.md — one claim = one citable question (unifies coarse's "one question" and fine's "theory/experiment separation" framings), under-splitting traps, the two tests. - formalize-independence.md — no-double-counting check, the four patterns, shared-factor extraction. Both skills now load these instead of duplicating ~360 lines of prose. The coarse-vs-fine divergence (reduced vs full DSL, single-pass vs six-pass) stays per-skill. Also: - Unify fine's package scaffolding onto `gaia pkg scaffold` / `gaia pkg add-module`, matching coarse (it had used the bare `gaia build init`). - Split the 806-line gaia-formalize-fine/SKILL.md into a slim SKILL.md + references/pass-1..6 + priors-analysis-render.md, matching coarse's modular progressive-disclosure form. Co-Authored-By: Claude Opus 4.7 (1M context) --- gaia/_skills/_shared/formalize-atomicity.md | 130 +++ .../_shared/formalize-extract-conclusions.md | 137 +++ .../_skills/_shared/formalize-independence.md | 125 +++ .../_shared/formalize-reasoning-chains.md | 133 +++ gaia/_skills/gaia-formalize-coarse/SKILL.md | 16 + .../references/phase-1-extract-conclusions.md | 197 +---- .../phase-2-build-reasoning-chain.md | 150 +--- gaia/_skills/gaia-formalize-fine/SKILL.md | 812 ++---------------- .../references/pass-1-extract.md | 103 +++ .../references/pass-2-connect.md | 124 +++ .../references/pass-3-completeness.md | 32 + .../references/pass-4-strategy-types.md | 117 +++ .../references/pass-5-structural-integrity.md | 60 ++ .../references/pass-6-polish.md | 71 ++ .../references/priors-analysis-render.md | 120 +++ 15 files changed, 1279 insertions(+), 1048 deletions(-) create mode 100644 gaia/_skills/_shared/formalize-atomicity.md create mode 100644 gaia/_skills/_shared/formalize-extract-conclusions.md create mode 100644 gaia/_skills/_shared/formalize-independence.md create mode 100644 gaia/_skills/_shared/formalize-reasoning-chains.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/pass-1-extract.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/pass-2-connect.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/pass-3-completeness.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/pass-4-strategy-types.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/pass-5-structural-integrity.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/pass-6-polish.md create mode 100644 gaia/_skills/gaia-formalize-fine/references/priors-analysis-render.md diff --git a/gaia/_skills/_shared/formalize-atomicity.md b/gaia/_skills/_shared/formalize-atomicity.md new file mode 100644 index 000000000..4c3b5b0ac --- /dev/null +++ b/gaia/_skills/_shared/formalize-atomicity.md @@ -0,0 +1,130 @@ +# Claim atomicity + +Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. Both +skills decompose a paper into atomic claims; this file is the single canonical +statement of what "atomic" means and how to test for it. Reference, not +procedure — it has no frontmatter and is not itself a skill. + +A claim's *mechanics* — whether it is held in working notes or written +straight to DSL, what label it gets, which module it lands in — belong to the +calling skill. This file owns only the question: **is this one claim, or +several?** + +## The principle + +Each claim states **exactly one thing**: it answers exactly one citable +epistemic question about the paper — one new bound, one new relation, one new +procedure, one new measured value, one new comparison outcome, one new causal +attribution, one new generalization result. If a candidate body answers two, +split it into two claims. + +The rule is **field-agnostic**. The same one-question-per-claim discipline +applies whether the paper is a theorem in pure mathematics, a clinical-trial +endpoint in medicine, a benchmark result in machine learning, a causal +estimate in social science, or a measurement in experimental physics. + +## Two corollaries that catch most violations + +The most common atomicity failures are two specific fusion patterns. Each is +just the one-question test applied to a recurring shape. + +### Separate theory from experiment + +A theoretical prediction and the experimental measurement it is compared +against are **two claims, never one**. They answer different citable +questions, carry different evidence, and have different weak points. A claim +that fuses them also cannot be wired to a verification relation later. + +```python +# BAD — theory and experiment fused +result = claim("The model predicts X, the experimental value is Y, deviation Z%.") + +# GOOD — two independently judgeable claims +prediction = claim("Based on method M, the model predicts quantity Q = X.") +measurement = claim("The experimental measurement of quantity Q is Y.") +``` + +### Separate method from result + +A method or procedure description and the value that applying it produced are +**two claims**. The method is a contribution a later paper could reuse for a +different outcome; the value is an empirical result a different method could +equally have produced. + +```python +# BAD — method and result fused +result = claim("Using method M to compute Q yields Z.") + +# GOOD +method = claim("Method M employs ... strategy ...") +result = claim("The numerical result for Q is Z ± δ.") +``` + +## Common under-splitting traps + +Each trap is illustrated with examples from different fields to make clear +that the trap is structural, not domain-specific. + +- **Definition + headline result.** A new bound (e.g. "the scheme is + parametrically valid when $\omega_D \ll E_F$, $\omega_c^2 \ll \omega_p^2$, + $T \ll \omega_c$") and the downstream result that uses it are *two* claims — + the bound is a citable regime claim on its own. Outside physics, the same + trap appears in a clinical RCT that introduces a new operational criterion + alongside its prevalence: "the protocol's prespecified no-disease-activity + criterion at week 24 (combining OCT central-subfield thickness, BCVA, + hemorrhage status, and investigator judgment) is met by 65% of treated + participants" is two claims — the criterion is a methodological + contribution citable by anyone designing a similar regimen, separate from + the empirical prevalence it yielded in this cohort. +- **Procedure + the value it produced.** "Cluster-DiagMC achieves + γ~$10^5$ at $n=6$ and reproduces $P(0,0)=0.0504(3)$" is two claims: the + algorithm's measured speedup, and the agreement with the polarization + baseline. Each has different evidence and different weak points. Outside + physics, the same trap appears in a clinical RCT conclusion that bundles + regimen with outcome: "faricimab dosed every 16 weeks after a four-monthly + loading phase produces +11.4 ETDRS letters at week 52 with a mean of 6.2 + injections" is two — the dosing regimen is a methodological contribution + downstream trials could reuse for a different outcome, and the measured + BCVA change is an empirical efficacy result a different regimen could + equally have produced. +- **Theorem + worked example.** A general formal claim and the explicit + worked-example calculation that motivates it (e.g. "the third-order + four-diagram cancellation drops by $\sim 3.48 \times 10^{-3}$") are two + claims when the worked example is a separate quantitative finding. Outside + physics, the same trap appears in causal-inference methodology papers: a + new identifiability theorem for an estimand under stated assumptions, and a + worked example applying the resulting estimator to a specific + competing-events dataset to produce a numerical estimate, are two claims — + the theorem is a formal contribution citable by anyone working with that + estimand class, and the worked example is an empirical instantiation. +- **Mechanism + benchmark.** "The downfolded Migdal–Eliashberg equation + reproduces the toy-model $T_c$ to within $0.2\%$" — the mechanism (the + equation) is one claim; the benchmark agreement is another. Outside + physics, the same trap appears in algorithmic system papers: "DVL + pre-integration is linearized in the rotation update, avoiding full + re-integration inside the nonlinear solver, and AQUA-SLAM achieves lower + translation RMSE than five baselines on the WaveTank dataset" is two — the + linearization mechanism is a methodological contribution downstream SLAM + systems could adopt with a different baseline set, and the WaveTank RMSE + comparison is an empirical benchmark result. + +## Two tests + +**Split test.** After writing a candidate body, ask: *if I deleted any one +clause, would I lose an answer to a distinct citable question?* If yes, split +that clause off. If the body merely loses an aside that does not answer its +own citable question, it is one claim. + +**Standalone-citation test.** Would each candidate stand on its own as a +sentence the paper could have published as a stand-alone bullet in the +abstract? If yes, it is atomic. If two candidates can only be cited together +(one is an aside of the other), they are one. + +## Do not pre-classify while splitting + +Atomicity is only about the one-question split. While splitting, do **not** +pre-classify a claim by "type" (analytical / empirical / methodological) and +do **not** pre-assign it a weak-point pattern. A single claim typically rests +on several reasoning patterns at once; type and weak-point classification +happen later, per the calling skill's own workflow. Atomicity work has +exactly one job: enforce the one-question-per-claim split. diff --git a/gaia/_skills/_shared/formalize-extract-conclusions.md b/gaia/_skills/_shared/formalize-extract-conclusions.md new file mode 100644 index 000000000..ce5412666 --- /dev/null +++ b/gaia/_skills/_shared/formalize-extract-conclusions.md @@ -0,0 +1,137 @@ +# Extracting a paper's conclusions + +Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. Both +skills begin by reading the paper and identifying its genuine new +contributions as claims; this file is the canonical statement of *what* to +extract and *how each extracted claim must read*. Reference, not procedure — +no frontmatter, not itself a skill. + +This file does **not** own extraction mechanics — working notes vs incremental +DSL, module layout, the `note` / `question` node kinds, label minting — those +belong to the calling skill. Atomicity (one claim = one question) has its own +file, `formalize-atomicity.md`. + +## What counts as a conclusion + +A conclusion is **new author-asserted knowledge that would not exist if this +paper had not been written**: + +- a newly derived formula, theoretical relation, or analytical result; +- a quantitatively new numerical or experimental value, scaling law, phase + boundary, or benchmark; +- a newly proposed algorithm, computational scheme, or experimental method. + +It is **not**: + +- a restatement of prior work; +- a trivial corollary of the paper's own assumptions; +- a rhetorical claim of importance, motivation, or future work; +- a reformulation that adds no information. + +## Fidelity to the paper + +The paper text is the only source of truth. While extracting: + +- Do not strengthen heuristic claims into established facts. +- Do not supply missing derivations or repair broken arguments. +- Do not import outside knowledge, even to "fix" an undefined symbol — leave + it undefined and surface the gap. +- Preserve the authors' epistemic hedging exactly: regimes, error bars, + speculative qualifiers, modal force ("suggests" stays "suggests"). + +## Write every claim self-contained + +Each claim body must be a complete proposition a reviewer can judge without +reading the paper or any other claim: + +- **Symbols** — every mathematical symbol gets a brief meaning on first use in + that body (`$\alpha$ (ratio of XX to YY)`), not bare (`$\alpha \ll 1$`). + Each claim is independent; re-explain a symbol even if another claim already + did. +- **Acronyms** — expanded on first use in that body, every time. +- **Setup** — the system / model / dataset / regime is described inside the + proposition, not assumed. +- **Concrete subject** — every sentence's subject is the model, the + estimator, the measurement — never "the paper" or "this work". +- **No bare comparatives** — not "significantly larger than X" or "nearly + exact agreement"; give both numbers. +- **Inline values, not pointers** — write the equation, the value, the setup + into the body; never "Eq. (3)" or "Fig. 4" (see "No paper-internal + pointers" below). + +## Content format + +Claim bodies support Markdown — use it for structure: + +- **Tables** — Markdown tables for structured data. +- **Math** — `$...$` inline, `$$...$$` display. LaTeX, not Unicode math + symbols. +- **Lists** — bullets to enumerate conditions or items. +- **Emphasis** — bold / italic for key values or terms. + +## Figures and tables → inline as prose + +The paper Markdown does not carry figure pixels. When the paper's argument +relies on what a figure or table shows, transcribe the quantitative content +into the claim body: the specific values, the curve shape, the trend, the +comparison. + +```python +tc_data = claim( + "Measured superconducting transition temperatures:\n\n" + "| Material | $T_c$ (K) | Pressure (GPa) |\n" + "|----------|-----------|----------------|\n" + "| LaH10 | 250 | 200 |\n" + "| H3S | 203 | 150 |", + title="Tc measurements", +) +``` + +The claim body carries everything needed for judgement. A figure/table +reference in `metadata` is for **traceability only**, never for conveying +information the body omitted. + +## No paper-internal pointers; refs whitelist + +Structural pointers into the paper — `Eq. (5)`, `Fig. 3`, `Table I`, +`Sec. II`, `Appendix A`, `Theorem 2`, `Lemma M`, footnotes — must not appear +inside a claim body. Resolve every such pointer by inlining its content. + +For traceability, note the figures / tables / equations / external citations +that primarily evidence each conclusion. The **only three** pointer kinds that +may be retained (as `refs` metadata) are: + +- **`figure`** — a figure or table (`Fig. 2`, `Table I`). +- **`equation`** — an equation referenced by number (`Eq. (5)`). +- **`citation`** — an external bibliographic reference. Convert the paper's + numeric citations (`[33]`, `Ref. 5`) to a key of first-author surname plus + year (`Smith2020`); the same key goes into `references.json`. + +Section / appendix / paragraph / theorem / lemma / footnote pointers are +**not** legitimate `refs` entries — inline their content instead. + +## Citation form in prose + +External citations in any prose (claim bodies, rationales) use the `[@key]` +form, where `key` matches an entry in `references.json` +(``, e.g. `[@Smith2020]`). Never leave numeric +paper-style citations (`[33]`, `Ref. 5`, `Smith et al., 2020`) in prose; +convert at write time. If a key cannot be derived from the paper's +bibliography, use bare `@unknown_` (**no brackets** — bracketed +`[@unknown_n]` fails the compiler's strict-reference check; bare `@key` is +opportunistic) and surface the gap. The full citation contract lives in +`docs/for-users/language-reference.md`. + +## Extract both sides of every comparison + +When the paper compares a theoretical prediction against an experimental +observation, extract **both** as separate claims (atomicity requires this too +— see `formalize-atomicity.md`), so the verification relation can be wired +later. When several competing theories are compared against one observation, +extract **each** competing prediction as its own claim. + +When the paper argues one general rule is confirmed by repeated independent +observations (multiple samples, labs, conditions), extract **each +observation** as its own claim plus the candidate rule as its own claim. The +wiring — and the independence judgement those observations must satisfy — is +covered in `formalize-reasoning-chains.md` and `formalize-independence.md`. diff --git a/gaia/_skills/_shared/formalize-independence.md b/gaia/_skills/_shared/formalize-independence.md new file mode 100644 index 000000000..2ab6e963b --- /dev/null +++ b/gaia/_skills/_shared/formalize-independence.md @@ -0,0 +1,125 @@ +# Evidence independence — no double counting + +Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. Both +skills must ensure each reasoning relation they emit encodes a genuinely +independent constraint. This file is the canonical statement of the +independence check. Reference, not procedure — no frontmatter, not itself a +skill. + +## The principle + +Gaia runs exact inference (Junction Tree) — given any factor graph it computes +correct posteriors. There is no algorithmic double counting. Every issue here +is about whether the **model** matches reality: each relation must represent a +constraint that brings genuinely new information no other relation already +provides. When the same evidence enters a conclusion twice, the model claims +two independent constraints where only one exists, and beliefs inflate. + +When an implicit dependency exists, make it **explicit** as a node in the +graph so inference can reason about it correctly. + +The independence check applies to whatever relation verbs a skill emits — a +`derive`-only reduced model and a full `derive` / `infer` / `compute` / +`decompose` model are both subject to it. Patterns below that name a specific +verb apply only to skills that emit that verb. + +## Pattern 1 — Redundant relations (same reasoning expressed twice) + +```python +# 1a. Exact duplicate — the same support stated standalone and inside a wider relation +derive(law, given=[obs]) +derive(law, given=[obs_a, obs_b, obs]) # re-uses obs +# FIX: drop the standalone relation, or fold it into the wider one. + +# 1b. Transitive shortcut — an A→B→C chain plus an A→C that is just the chain compressed +derive(B, given=[A]); derive(C, given=[B]); derive(C, given=[A]) +# FIX: drop the shortcut, OR confirm it is a genuinely different argument. + +# 1c. Derived-premise redundancy — A→B, then C given [A, B] where A reaches C only through B +derive(B, given=[A]); derive(C, given=[A, B]) +# FIX: drop A from C's premises → derive(C, given=[B]). +``` + +## Pattern 2 — Hidden evidence in rationale text + +Two relations with identical premises but different `rationale` prose: the +differing prose contains evidence not captured as a premise. Extract it. + +```python +# BEFORE — same premises, different reasoning angles +derive(law, given=[sample, obs_R], rationale="Zero resistance = SC hallmark") +derive(law, given=[sample, obs_R], rationale="Transition width < 0.5 K = bulk SC") + +# AFTER — the hidden "transition width" evidence becomes its own claim +transition_sharpness = claim("Resistivity transition width < 0.5 K") +derive(law, given=[sample, obs_R], rationale="Zero resistance = SC hallmark") +derive(law, given=[sample, transition_sharpness], rationale="Sharp transition = bulk SC") +``` + +## Pattern 3 — Unmodelled shared dependencies + +Two observations share a common cause (same sample, same instrument) but the +cause is not in the graph: the model treats them as unconditionally +independent and loses their correlation. + +```python +# BEFORE — shared sample quality implicit, correlation lost +derive(law, given=[obs_R, obs_chi]) + +# AFTER — extract the shared cause; correlation preserved +sample_quality = claim("Sample A is a high-quality single crystal, confirmed by XRD") +derive(obs_R, given=[sample_quality]) +derive(obs_chi, given=[sample_quality]) +derive(law, given=[obs_R, obs_chi], rationale="Conditionally independent given sample_quality") +``` + +You cannot create new experiments — you formalize what the paper provides: + +| Observation relationship | Modelling approach | +|---|---| +| Truly independent (different samples / labs) | Use the observations directly as parallel premises | +| Partially independent (shared dependency + independent components) | Extract the shared dependency as an explicit claim | +| Completely redundant (same data rephrased) | Merge into a single claim | + +## Pattern 4 — `equal` plus separate relations (structural-verb skills only) + +When `equal(a, b)` couples two claims and both sides also relate to the same +target, check each relation brings information beyond what `equal` already +propagates. + +```python +equal(claim_A, claim_B) +derive(law, given=[claim_A]); derive(law, given=[claim_B]) +# Does B→law add anything A→law + equal does not already give? +# NO → drop B→law. YES → extract the extra information as a new premise. +``` + +## Shared-factor extraction + +If two supports on the same target share an underlying factor — same +approximation, same dataset, same lemma, same external assumption — extract +the shared factor as its own claim and let both supports depend on that one +factor, rather than letting the factor's uncertainty enter the target twice. + +## Repeated observations must be independent + +When a general rule is supported by several observations, each must provide +**independent** evidence. If they share a sample, instrument, or pipeline, +that shared dependency is a Pattern 3 case — extract it as an explicit claim +before treating the observations as parallel support. + +## How to check + +1. List every claim with 2+ incoming relations. +2. For each pair of relations into it: does each bring genuinely independent + new information? +3. For each relation over multiple observations: do the observations share an + unmodelled dependency? +4. For each `equal`: do both sides need their own relation to the same target? +5. For every relation: does the `rationale` prose contain evidence not + captured as a premise? + +After any independence fix, re-run inference and compare beliefs. A +significant belief drop after removing a relation confirms the previous value +was inflated by double counting. For reading the resulting beliefs, see +`bp-interpretation.md`. diff --git a/gaia/_skills/_shared/formalize-reasoning-chains.md b/gaia/_skills/_shared/formalize-reasoning-chains.md new file mode 100644 index 000000000..b78164bdd --- /dev/null +++ b/gaia/_skills/_shared/formalize-reasoning-chains.md @@ -0,0 +1,133 @@ +# Reconstructing reasoning chains + +Shared reference for `gaia-formalize-coarse` and `gaia-formalize-fine`. After +the paper's conclusions are extracted, both skills reconstruct how the paper +argues each one. This file is the canonical statement of that reconstruction. +Reference, not procedure — no frontmatter, not itself a skill. + +This file owns the **logic graph**, the **per-conclusion reasoning trace**, +and the **step-writing rules**. It does not own which DSL verb carries the +relation (a `derive`-only reduced model vs the full `derive` / `infer` / +`observe` / `compute` / `decompose` set) — verb choice is a coarse-vs-fine +divergence owned by each skill. The independence of the resulting premises has +its own file, `formalize-independence.md`. + +## The logic graph + +Before reconstructing any chain, map the dependency edges among the extracted +conclusions. For each ordered pair `(A, B)`, add an edge `A → B` if and only +if: + +- the reasoning that establishes B explicitly or implicitly relies on A's + result as a premise or intermediate step, **and** +- the reliance is traceable to the paper text, not to your own reasoning about + the subject. + +Rules: + +- The graph must be **acyclic**. +- Independent conclusions have no edges; that is expected. +- Edges must be **direct** — if `A → B` and `B → C`, do not also add `A → C` + unless the paper uses A directly in deriving C without going through B. +- Topical similarity is not a derivation dependency. +- Two conclusions appearing in the same downstream application is not a + derivation dependency. + +## Topological ordering + +Reconstruct conclusions in topological order on the logic graph: + +1. If `A → B` is an edge, reconstruct A before B. +2. Tie-break by extraction order / id (smaller first). +3. Every conclusion is reconstructed exactly once, including isolated ones. + +Order matters: when reconstructing B, A's result is already established and +can be referenced by name instead of re-derived, and the reconstruction order +lines up with a linearly readable emitted package. + +## Per-conclusion reconstruction + +For every conclusion, reconstruct the paper's own reasoning trace from +foundational material to the conclusion, as an ordered list of steps. Each +step is one logical move. **Steps are not claims** — they are the prose that +becomes the relation's `rationale`. + +### Root and isolated conclusions + +For a conclusion with no upstream conclusions, reconstruct the full chain from +the paper's foundations: + +- definitions, assumptions, model setups; +- experimental protocol, dataset construction, sample preparation; +- the theoretical framework or governing equations; +- cited results explicitly invoked. + +Capture every logical move. Do not skip mechanical algebra "for brevity" — +redundancy is acceptable, omission is not. + +### Derived conclusions + +For a conclusion B with upstream `A_1, A_2, ...`: + +- the first one or two steps state each upstream conclusion's result (treating + it as established) and which aspect B will use; +- the remaining steps are the **incremental** reasoning bridging the upstream + results to B; +- include additional definitions, assumptions, or cited results only where the + paper itself invokes them. + +Do not re-derive an upstream conclusion. Do not invent a dependency the paper +does not use. + +## Premises vs background + +When wiring a relation, split what the reasoning rests on: + +- **Claims** used in the derivation → **premises** (the support set). +- **Definitions, formal setups, fundamental principles, open questions** used + in the derivation → **background**. + +## Do not miss implicit premises + +Papers often leave premises implicit. While writing the chain, if the +derivation depends on a knowledge node that was already extracted, add it to +the premise or background set and reference it in the rationale. If it depends +on something not yet extracted, go back and extract it — a fact the reasoning +uses must be a node in the graph, never an unstated assumption. + +## Step-writing rules + +1. **Maximize detail.** One logical move per step. Every symbol introduced is + defined inside the same step or an earlier step of the same chain. +2. **Textualize figures and tables.** When the argument relies on what a + figure shows, inline the quantity / shape / trend / comparison. Not + "Fig. 3 shows a direct gap" but "the computed band structure has a direct + gap of 1.2 eV at the $\Gamma$ point, falling to 0.8 eV under 5% biaxial + strain". No step should require *seeing* a figure. +3. **Use formalism where the paper does.** Reproduce equations in `$...$` / + `$$...$$`; do not paraphrase mathematics the paper states as a formula. + Define every quantity at first appearance. +4. **Record logical gaps and heuristic moves explicitly.** If the authors + skip a derivation, appeal to intuition, or assert without proof, record it + as such ("the authors assert without derivation that ...", "the argument + relies on a heuristic that ...") — do not silently repair it. These flagged + steps inform the warrant-strength intent the calling skill writes into the + rationale. +5. **No paper-internal pointers in step prose.** Resolve `Eq. (16)`, + `Sec. II`, `Theorem 2`, `Appendix A`, "as derived above" by inlining the + content. External citations are preserved but rewritten into `[@key]` form + (see `formalize-extract-conclusions.md`). +6. **No external knowledge.** Do not invoke "well-known facts" or textbook + results unless the paper explicitly does. +7. **Authorial voice.** Impersonal scientific voice without changing modal + force: "We assume X" → "X is assumed"; do not strengthen ("show" / "prove") + or weaken ("suggest" / "indicate") beyond the paper's own modality. + +## The chain becomes the rationale + +The ordered step list is the raw material for the relation's `rationale` +field. A rationale is a complete reasoning chain a domain reader can follow — +not a one-sentence stub. Keep the numbered-step structure; it carries through +to the emitted relation. Reference knowledge nodes by `@label` and bibliography +entries by `[@key]`; every `@label` in a rationale must appear in that +relation's premise or background set, and vice versa. diff --git a/gaia/_skills/gaia-formalize-coarse/SKILL.md b/gaia/_skills/gaia-formalize-coarse/SKILL.md index 03903a29b..3d80d9a36 100644 --- a/gaia/_skills/gaia-formalize-coarse/SKILL.md +++ b/gaia/_skills/gaia-formalize-coarse/SKILL.md @@ -203,6 +203,22 @@ paragraph. Do not invent contributions to fill the gap. - [`references/phase-4-emit-package.md`](references/phase-4-emit-package.md) — composing Phase 1–3 working notes into Gaia DSL package files. +### Shared formalization methodology (`../_shared/`) + +Extraction, atomicity, reasoning-chain, and independence methodology shared +with `gaia-formalize-fine`; Phases 1–2 load these from `_shared/`: + +- [`../_shared/formalize-extract-conclusions.md`](../_shared/formalize-extract-conclusions.md) + — what counts as a conclusion, fidelity, self-contained bodies, figures as + prose, `refs` whitelist, citation form. +- [`../_shared/formalize-atomicity.md`](../_shared/formalize-atomicity.md) + — one-question-per-claim, under-splitting traps, the two tests. +- [`../_shared/formalize-reasoning-chains.md`](../_shared/formalize-reasoning-chains.md) + — logic graph, topological order, reasoning-trace reconstruction, step + rules. +- [`../_shared/formalize-independence.md`](../_shared/formalize-independence.md) + — the no-double-counting check on each conclusion's premise set. + ### Gaia knowledge-package contract (this repo's docs) - `docs/for-users/quick-start.md` — end-to-end Gaia knowledge-package diff --git a/gaia/_skills/gaia-formalize-coarse/references/phase-1-extract-conclusions.md b/gaia/_skills/gaia-formalize-coarse/references/phase-1-extract-conclusions.md index eea591ef2..4ed46195e 100644 --- a/gaia/_skills/gaia-formalize-coarse/references/phase-1-extract-conclusions.md +++ b/gaia/_skills/gaia-formalize-coarse/references/phase-1-extract-conclusions.md @@ -34,155 +34,28 @@ the package. ## Extraction Rules -### What is a conclusion - -A conclusion is **new author-asserted knowledge** that would not exist if this -paper had not been written: - -- a newly derived formula, theoretical relation, or analytical result; -- a quantitatively new numerical or experimental value, scaling law, phase - boundary, or benchmark; -- a newly proposed algorithm, computational scheme, or experimental method. - -It is **not**: - -- a restatement of prior work; -- a trivial corollary of the paper's own assumptions; -- a rhetorical claim of importance, motivation, or future work; -- a reformulation that adds no information. - -### Atomicity - -Each conclusion must answer **exactly one** citable epistemic question -about the paper — one new bound, one new relation, one new procedure, one -new measured value, one new comparison outcome, one new causal attribution, -one new generalization result, etc. If a candidate body answers two, -split it into two conclusions. - -This rule is **field-agnostic**: the same one-question-per-conclusion -discipline applies whether the paper is a theorem in pure math, a -clinical-trial endpoint in medicine, a benchmark result in ML, a causal -estimate in social science, or a measurement in experimental physics. - -Do **not** pre-classify a conclusion by "type" (analytical / empirical / -methodological / etc.) here, and do **not** pre-assign it a Phase 3 -`weak_types` pattern. The nine `weak_types` keys describe *threats to a -conclusion's derivation*, not *what kind of conclusion it is*; a single -conclusion typically rests on several patterns simultaneously, and the -pattern assignment happens per weak point in Phase 3, not per conclusion -here. Phase 1's only job for atomicity is to enforce the -one-question-per-conclusion split. - -**Common under-splitting traps to avoid:** - -Each trap is illustrated with examples from different fields to make -clear that the trap is structural, not domain-specific. - -- **Definition + headline result.** A new bound (e.g., "the scheme is - parametrically valid when $\omega_D \ll E_F$, $\omega_c^2 \ll \omega_p^2$, - $T \ll \omega_c$") and the downstream result that uses it are *two* - conclusions, not one — the bound is a citable regime claim on its own. - Outside physics, the same trap appears in a clinical RCT that introduces - a new operational criterion alongside its prevalence: "the protocol's - prespecified no-disease-activity criterion at week 24 (combining OCT - central-subfield thickness, BCVA, hemorrhage status, and investigator - judgment) is met by 65% of treated participants" is two conclusions — - the criterion is a methodological contribution citable by anyone - designing a similar extended-dosing regimen, separate from the - empirical prevalence it yielded in this particular cohort. -- **Procedure + the value it produced.** "Cluster-DiagMC achieves - γ~$10^5$ at $n=6$ and reproduces $P(0,0)=0.0504(3)$" is two - conclusions: the algorithm's measured speedup, and the agreement with - the polarization baseline. Each has different evidence and different - weak points. Outside physics, the same trap appears in a clinical RCT - conclusion that bundles regimen with outcome: "faricimab dosed every - 16 weeks after a four-monthly loading phase produces +11.4 ETDRS - letters at week 52 with a mean of 6.2 injections" is two — the dosing - regimen is a methodological contribution that downstream trials could - reuse for a different outcome, and the measured BCVA change is an - empirical efficacy result that a different regimen could equally have - produced. -- **Theorem + worked example.** A general formal claim and the explicit - worked-example calculation that motivates it (e.g., "the third-order - four-diagram cancellation drops by $\sim 3.48 \times 10^{-3}$") are two - conclusions when the worked example is a separate quantitative finding. - Outside physics, the same trap appears in causal-inference methodology - papers that bundle theory with demonstration: a new identifiability - theorem for an estimand under stated assumptions, and a worked example - applying the resulting estimator to a specific competing-events dataset - to produce a numerical estimate, are two conclusions — the theorem is - a formal contribution citable by anyone working with that estimand - class, and the worked example is an empirical instantiation citable - only by people analyzing that specific data. -- **Mechanism + benchmark.** "The downfolded Migdal–Eliashberg equation - reproduces the toy-model $T_c$ to within $0.2\%$" — the mechanism (the - equation) is one conclusion (analytical); the benchmark agreement is - another (comparative). Outside physics, the same trap appears in - algorithmic system papers that bundle a method with its benchmark: - "DVL pre-integration is linearized in the rotation update, avoiding - full re-integration inside the nonlinear solver, and AQUA-SLAM - achieves lower translation RMSE than five baselines on the WaveTank - dataset" is two — the linearization mechanism is a methodological - contribution that downstream SLAM systems could adopt with a different - baseline set, and the WaveTank RMSE comparison is an empirical - benchmark result that could come from a different underlying - algorithmic choice. - -**Split test.** After writing a candidate body, ask: *if I deleted any one -clause, would I lose an answer to a distinct citable question?* If yes, -split that clause off. If the body merely loses an aside that does not -answer its own citable question, it is one conclusion. - -**Standalone-citation test.** Would each candidate stand on its own as a -sentence the paper could have published as a stand-alone bullet in the -abstract? If yes, it is an atomic conclusion. If two candidates can only -be cited together (because one is an aside of the other), they are one. - -### Self-containment as you write - -Every conclusion's working-note text must already meet the -self-containment criterion that Phase 4 will demand: - -- All symbols and acronyms defined in-text on first use. -- The system / model / dataset / regime described inside the proposition. -- Inline numerical values, equation forms, or experimental setups instead of - pointers like "Eq. (3)" or "Fig. 4". -- Concrete subject in every sentence (the model, the estimator, the - measurement) — not "the paper" or "this work". - -This is the rule the legacy step-4 prompt enforced; here it is enforced at -the moment the conclusion is written, not as a post-hoc rewrite. - -### Fidelity - -- Do not strengthen heuristic claims into established facts. -- Do not supply missing derivations. -- Do not import outside knowledge. -- Preserve the authors' epistemic hedging exactly (regimes, error bars, - speculative qualifiers). - -### Evidence localization - -For each conclusion, note the figures / tables / equations / external -citations that primarily evidence it. These notes become the `refs` -metadata on the `claim(...)` in Phase 4 (the `refs` metadata field is -documented in `docs/for-users/language-reference.md`). - -Allowed pointer kinds — these are the **only three** that may end up in -`refs`: - -- **`figure`** — a figure or table in the paper (e.g. `Fig. 2`, `Table I`). -- **`equation`** — an equation referenced by number (e.g. `Eq. (5)`). -- **`citation`** — an external bibliographic reference. Convert numeric - citations from the paper (e.g. `[33]`, `Ref. 5`) to a key matching the - paper's first-author surname plus year (e.g. `Smith2020`); the same key - goes into `references.json` in Phase 4. - -Section, appendix, paragraph, theorem, lemma, and footnote pointers are -**not** legitimate `refs` entries and must not be retained. If a conclusion -is rooted in "Section IV" of the paper, the relevant content has to be -inlined into the conclusion's body itself; do not preserve the section -pointer. +The methodology for identifying conclusions and writing each one is **shared +with `gaia-formalize-fine`** and lives in `_shared/`. Load both files now and +apply them as you extract: + +- [`../../_shared/formalize-extract-conclusions.md`](../../_shared/formalize-extract-conclusions.md) + — what counts as a new conclusion, fidelity to the paper, self-contained + claim bodies, content format, figures and tables transcribed as prose, the + no-paper-internal-pointer rule, the `refs` whitelist, and citation form. +- [`../../_shared/formalize-atomicity.md`](../../_shared/formalize-atomicity.md) + — the one-question-per-claim rule, the theory/experiment and method/result + corollaries, the under-splitting traps, and the split and + standalone-citation tests. + +Coarse-specific points on top of the shared rules: + +- Phase 1 extracts **conclusions only**. Weak points are extracted later, in + Phase 3, as leaf premises — they are not conclusions and are not subject to + the "what counts as a conclusion" test here. +- Conclusions live in working notes (schema below), not on disk; Phase 4 is + the only phase that emits files. +- The figure / equation / citation pointers collected per the shared file's + `refs` whitelist become the `refs` metadata on each `claim(...)` in Phase 4. ## Motivation Block @@ -208,23 +81,11 @@ conclusions into open questions. ## Logic Graph -For each ordered pair `(A, B)` of conclusions, decide whether the paper's -own argumentation **uses** A in deriving B. Add an edge `A → B` if and only if: - -- The reasoning that establishes B explicitly or implicitly relies on A's - result as a premise or intermediate step, **and** -- The reliance is traceable to the paper text, not to your own reasoning - about the subject matter. - -Rules: - -- The graph must be acyclic. -- Independent conclusions have no edges; that is expected. -- Edges must be **direct**: if A → B and B → C, do not also add A → C unless - the paper uses A directly in deriving C without going through B. -- Topical similarity ≠ derivation dependency. -- Two conclusions appearing in the same downstream application ≠ derivation - dependency. +Build the directed dependency graph among conclusions — an edge `A → B` means +the paper's own reasoning uses A in deriving B — per the "The logic graph" +section of +[`../../_shared/formalize-reasoning-chains.md`](../../_shared/formalize-reasoning-chains.md). +Phase 2 consumes this graph for topological ordering. ## Working Notes Schema @@ -270,8 +131,8 @@ minted in Phase 4 from the paper key plus a semantic suffix. Before moving to Phase 2: - Suitability decision is made; if skipping, stop here and note for Phase 4. -- Every retained conclusion passes atomicity, fidelity, and self-containment - checks. +- Every retained conclusion passes the atomicity, fidelity, and + self-containment checks from the `_shared/` files. - The logic graph is acyclic and minimal. - Motivation and open-question paragraphs are present (or recorded as "no motivation block" / "no open questions" if genuinely absent). diff --git a/gaia/_skills/gaia-formalize-coarse/references/phase-2-build-reasoning-chain.md b/gaia/_skills/gaia-formalize-coarse/references/phase-2-build-reasoning-chain.md index 64f3ca7bf..27d400f9e 100644 --- a/gaia/_skills/gaia-formalize-coarse/references/phase-2-build-reasoning-chain.md +++ b/gaia/_skills/gaia-formalize-coarse/references/phase-2-build-reasoning-chain.md @@ -14,138 +14,35 @@ The trace is held in working notes as an ordered list of step strings per conclusion. Each step is one logical move. Steps are not claims; they are prose that becomes part of `derive(...)`'s `rationale=`. -## Topological Ordering +## Reconstruction Methodology -Process conclusions in topological order on the Phase 1 logic graph: +The reconstruction method is **shared with `gaia-formalize-fine`** — load and +apply: -1. If `A → B` is an edge, A is reconstructed before B. -2. Tie-break by id (smaller first). -3. Every conclusion appears exactly once, including isolated ones. +- [`../../_shared/formalize-reasoning-chains.md`](../../_shared/formalize-reasoning-chains.md) + — topological ordering on the logic graph, per-conclusion reconstruction of + root and derived conclusions, the premise / background split, surfacing + implicit premises, and the seven step-writing rules. -Topological order matters for two reasons: +Coarse-specific points on top of the shared methodology: -- When reconstructing B, A's result is already established and can be - referenced by name in B's chain instead of re-derived. -- The output of Phase 2 will line up with the deduction-emission order in - Phase 4 so that downstream readers can read the package linearly. +- Coarse emits a **reduced DSL**: each derived conclusion becomes exactly one + `derive(...)` whose premises are the union of its upstream conclusions and + (after Phase 3) its weak-point claims. This skill emits no `infer` / + `observe` / `compute` / `decompose`, so the shared file's verb-specific + remarks for those verbs do not apply here. +- The reconstructed step list stays in working notes (schema below); it + becomes the `--rationale` prose in Phase 4, not a file on disk now. -## Per-Conclusion Reconstruction +## Independence Check -### Root and isolated conclusions - -For a conclusion with no upstream conclusions, reconstruct the full chain -from the paper's foundations: - -- Definitions, assumptions, model setups. -- Experimental protocol, dataset construction, sample preparation. -- Theoretical framework or governing equations. -- Cited results explicitly invoked. - -Capture every logical move from those foundations to the conclusion. Do not -skip mechanical algebra "for brevity"; redundancy is acceptable, omission is -not. - -### Derived conclusions - -For a conclusion B with upstream `A_1, A_2, ...`: - -- The first one or two steps state what each upstream conclusion's result is - (treating it as established) and which aspects of it B will use. -- The remaining steps are the **incremental** reasoning that bridges from - those upstream results to B. -- If the derivation also uses additional definitions, assumptions, or cited - results outside the upstream conclusions, include those — but only the - ones the paper itself invokes. - -Do not re-derive an upstream conclusion. Do not invent a dependency that the -paper does not use. - -## Step-Writing Rules - -### 1. Maximize detail and completeness - -- One logical move per step. -- Every symbol introduced gets defined inside the same step or an earlier - step in the same conclusion's chain. -- If the authors rely on a result implicitly, surface that reliance as its - own step. - -### 2. Textualize figures and tables - -The paper Markdown does not carry figure pixels. When the paper's argument -relies on what a figure or table shows, **inline that information as prose**: -the specific quantity, the curve shape, the trend, the comparison value. - -Avoid: "Fig. 3 shows a direct gap." -Write: "The computed band structure has a direct gap of 1.2 eV at the -$\Gamma$ point, decreasing to 0.8 eV under 5% biaxial strain." - -After writing, no step should rely on a reader being able to *see* the -figure to follow the argument. - -### 3. Use formalism where the paper uses formalism - -- Reproduce equations explicitly with LaTeX in `$...$` or `$$...$$`. -- Do not paraphrase mathematics into prose if the paper itself states the - formula. -- Define every quantity at first appearance. - -### 4. Record logical gaps and heuristic moves explicitly - -If the authors skip a derivation, appeal to intuition, or assert without -proof, record the move as such — do not silently repair it: - -- "The authors assert without derivation that ..." -- "At this point the argument relies on a heuristic that ..." - -These flagged steps inform the deduction warrant intent Phase 4 writes -into the `--rationale` prose; persistent gaps surface as explicit "the -authors assert without derivation" / "the argument relies on a heuristic" -sentences in the rationale (the engine `derive(...)` signature has no -`metadata=` / `warrant_prior` kwarg, so the calibration cannot live as -a number on the deduction itself). - -### 5. No paper-internal pointers in step prose - -Do not write "Eq. (16)", "Sec. II", "Theorem 2", "Appendix A", or "as derived -above in the paper" inside step text. Resolve every such pointer inline: - -- "Using Eq. (16)" → reproduce the equation, with symbols defined. -- "The Hamiltonian defined in Sec. II" → write the explicit Hamiltonian. -- "By the argument in Appendix A" → summarize the relevant argument inline. - -Paper-internal structural pointers are not preserved at all. **External -citations** are preserved (the cited work is still credited) but they are -rewritten into the `[@key]` form prescribed in rule 6a — never left in the -paper's original numeric form (`[33]`, `Ref. 5`). - -### 6. No external knowledge - -Do not invoke "well-known facts", standard theorems, or textbook results -unless the paper explicitly does. If the paper cites such results without -proof, record the citation as the paper presents it — but in the citation -form prescribed in rule 8 below. - -### 6a. Citation form in step prose - -External citations appearing in step prose use the `[@key]` form, where -`key` matches an entry in `references.json` (``, -e.g. `[@Smith2020]`). Do **not** leave numeric paper-style citations like -`[33]`, `Ref. 5`, or `Smith et al., 2020` in step prose; convert at write -time. If a key cannot be derived from the paper's bibliography, use -`@unknown_` (bare `@key`, **no brackets** — `gaia build compile` rejects -bracketed `[@unknown_n]` as an unresolvable strict reference; bare `@key` -is opportunistic) and note the gap in the hand-off report. The full -citation contract (allowed prose forms, `refs` whitelist, CSL-JSON / -`references.json` conventions) is documented in -`docs/for-users/language-reference.md`. - -### 7. Authorial voice - -Use impersonal scientific voice without changing modal force. -"We assume X" → "X is assumed". "The authors observe Y" → "Y is observed". -Do not strengthen ("show" / "prove") or weaken ("suggest" / "indicate") -beyond the paper's own modality. +Before closing Phase 2, verify each derived conclusion's premise set encodes +genuinely independent support — apply +[`../../_shared/formalize-independence.md`](../../_shared/formalize-independence.md). +In coarse's reduced DSL the load-bearing case is **Pattern 1c** +(derived-premise redundancy): if an upstream conclusion reaches the current +conclusion *only* through another upstream conclusion, drop it from the +premise set so the same support does not enter the conclusion twice. ## Working Notes Schema @@ -182,5 +79,6 @@ Before moving to Phase 3: whose content has not been inlined. - Every flagged logical gap or heuristic move is recorded as such, not silently repaired. +- Each derived conclusion's premise set has passed the independence check. - The next todo is marked in progress before loading `phase-3-review-weak-points.md`. diff --git a/gaia/_skills/gaia-formalize-fine/SKILL.md b/gaia/_skills/gaia-formalize-fine/SKILL.md index 9ae2c00d8..88c90c493 100644 --- a/gaia/_skills/gaia-formalize-fine/SKILL.md +++ b/gaia/_skills/gaia-formalize-fine/SKILL.md @@ -64,7 +64,8 @@ Formalize the **complete** source — not just the main result. A partial formal The methodology below leans on this fixed set of CLI calls. Drill into `gaia --help` when you need exact flags. -- `gaia build init -gaia` — fresh package skeleton (`src//__init__.py`, `pyproject.toml`). Does not create `artifacts/` or `references.json` — make those manually. +- `gaia pkg scaffold --target -gaia --name -gaia --namespace [--with-uuid] [--description "..."]` — fresh package skeleton (`pyproject.toml`, `src//__init__.py`, `.gaia/.gitkeep`). The import name is derived from `--name` (strip the trailing `-gaia`, hyphens → underscores); the CLI emits a JSON envelope. Does not create `artifacts/` or `references.json` — make those manually. +- `gaia pkg add-module --name --target -gaia [--imports ]` — scaffold a sibling module under `src//` (e.g. `motivation`, `s2_xxx`, `priors`). `--imports` pre-seeds DSL-verb imports (e.g. `--imports register_prior`). - `gaia build compile ` — lower DSL → IR (`.gaia/ir.json`). Run after every pass. - `gaia build check ` — structural validation + role classification (independent / derived / structural / background / scaffolded / orphaned). Use between passes: - `gaia build check --brief` — per-module overview with strategy summaries. @@ -111,7 +112,10 @@ my-package-gaia/ └── pyproject.toml ``` -`gaia build init` does not create `artifacts/` or `references.json` — make them manually. +`gaia pkg scaffold` creates `pyproject.toml`, `src//__init__.py`, and +`.gaia/.gitkeep`; per-section modules (`motivation.py`, `s2_xxx.py`, ...) are added +with `gaia pkg add-module`. Neither command creates `artifacts/` or +`references.json` — make those manually. ### `references.json` @@ -132,638 +136,31 @@ Keys must follow Pandoc citation-key grammar (letters, digits, `_`, `-`, `.`, `: Both PDF and markdown formats are supported for artifacts. Throughout formalization, refer back to the originals in `artifacts/` to keep numbers, formulas, and reasoning steps consistent with the source. -## Pass 1 — Extract knowledge nodes - -Read the source **section by section**. For each section, identify: - -| Type | Criterion | Examples | Author verb | -|------|-----------|---------|---| -| **note** | Background facts that cannot be questioned | Mathematical definitions, formal setups, fundamental principles | `gaia author note` | -| **claim** | Propositions that can be questioned or falsified | Computation results, theoretical derivations, predictions, experimental observations | `gaia author claim` | -| **question** | Open research questions | Driving questions for the source | `gaia author question` | - -### Organize by module - -Each source section corresponds to one Gaia module (Python file): - -- Introduction → `motivation.py` -- Section II → `s2_xxx.py` -- ... - -The module's docstring serves as the section heading. Each knowledge node should have a `title` parameter. - -### Place knowledge in the earliest module - -Each knowledge node belongs in the module corresponding to the section where it **first appears** in the source. Content from the Introduction goes into `motivation.py`. Claims in `motivation.py` can be freely referenced as premises or background by later modules — they are not restricted by module membership. Notes and questions are typically referenced via `background=`. - -### `note` vs `claim` classification guide - -**Principle: when in doubt between `note` and `claim`, mark it as `claim`.** - -| Category | Type | Examples | -|----------|------|---------| -| Mathematical definitions / formal setups | **note** | Coordinate system choice, variable decomposition definitions, mathematical form of potentials | -| Established fundamental principles | **note** | Conservation laws, exclusion principle, laws of thermodynamics | -| Standard approximation / method definitions (without applicability assertions) | **note** | Mathematical expression of an approximation (definition only, not asserting applicability) | -| Whether applicability conditions hold | **claim** | Whether an approximation applies to a specific system | -| Theoretical frameworks dependent on conditions | **claim** | "Theorem B holds when A is satisfied" | -| Theoretical derivation results | **claim** | Renormalization relations, scaling laws, asymptotic behaviour | -| Numerical computation results | **claim** | Values from computational methods | -| Experimental observations | **claim** | Measured quantities | - -**Key criterion:** can this proposition be questioned? If yes → `claim`. Only mathematical definitions and formal setups qualify as notes. - -**Distinguish definitions from assertions.** The mathematical definition of an approximation is a note; "this approximation is unreliable under certain conditions" is a claim. "Decompose the variable into high- and low-frequency parts" is a note (mathematical operation), but "the contribution of the high-frequency part is negligible" is a claim (physical assertion). - -**Dependency chains.** If A is a note and B depends on A being true while containing a physical assertion — B is typically a claim. - -Content that the source itself derives — even when the derivation is rigorous — should be a claim, because the derivation process itself may contain errors. - -### Content format - -Claim content supports markdown. Use it for structure: -- Tables: markdown tables for structured data. -- Math: `$...$` for inline, `$$...$$` for display equations. -- Lists: bullet points to enumerate conditions or items. -- Bold / italic: emphasise key values or terms. - -### Atomicity principle - -Each claim must be an **atomic proposition** — one claim expresses one thing. - -**Core rule: theoretical predictions must be separated from experimental results.** - -```python -# BAD: mixing theory and experiment -result = claim("The model predicts X, the experimental value is Y, deviation Z%.") - -# GOOD: separated into independent claims -prediction = claim("Based on method XX, the model predicts a certain quantity as X.", title="Model prediction") -experiment = claim("The experimental measurement of a certain quantity is Y.", title="Experimental value") -``` - -Similarly, separate **method descriptions** from **method application results**: - -```python -# BAD: method and result mixed -result = claim("Using method XX to compute YY yields ZZ.") - -# GOOD: separated -method = claim("Method XX employs ... strategy ...", title="Method description") -result = claim("The numerical result for YY is ZZ +/- delta.", title="Numerical result") -``` - -### Theory-experiment comparison: extract both sides for `infer` - -When a theoretical prediction is compared with experimental data, Pass 2 will connect them with an `infer(evidence=..., hypothesis=...)` step. To make that possible, Pass 1 must extract the prediction and the observation as **two separate claims**: - -```python -pred = claim("Theory T predicts Tc = 1.9 K under condition C.", title="Theory prediction") -obs = claim("Measured Tc = 1.2 K under condition C.", title="Measured Tc") -``` - -When the source argues that one of several competing theories best explains the observation, extract each competing prediction as its own claim. Pass 2 will model the comparison either by chaining `infer` against each candidate (each gets its own `--p-e-given-h`) or — when the alternatives are mutually exclusive in the paper's framing — by adding an `exclusive(a, b)` relation (for the two-alternative case) or a `decompose --formula-template or` over the candidate claims (for three or more). `exclusive` is strictly binary. The concept that the release/0.4 SKILL labelled "abduction" is preserved as a pattern: see [Pass 4](#pass-4--refine-strategy-types) for the explicit recipe and `../gaia-review/SKILL.md` for the prior-side π(Alt) discussion. - -### Repeated-observation pattern: extract every observation - -When the source argues that one general rule is confirmed by repeated independent observations (multiple samples, multiple labs, multiple conditions), extract **each observation as its own claim** plus the candidate law as its own claim: - -```python -law = claim("MgB2 universally superconducts below 39 K.", title="Universal Tc law") -obs_a = claim("Sample A: Tc = 39 K.") -obs_b = claim("Sample B: Tc = 39 K.") -obs_c = claim("Sample C: Tc = 39 K.") -``` - -Pass 2 will chain `derive(law, given=[obs_a, obs_b, obs_c], rationale=...)` (or one `derive` per observation against a shared `compose`'d generalisation step — see Pass 4). What release/0.4 called "induction" is now expressed as `derive` over a `compose`'d pattern; the underlying judgement (each observation must be **independent**) survives intact. - -### Figures and tables - -When the source contains figures or tables with important data: - -**Tables.** Use markdown table format in the claim content. The claim must be self-contained — a reviewer should not need to open the original. - -```python -tc_data = claim( - "Measured superconducting transition temperatures:\n\n" - "| Material | $T_c$ (K) | Pressure (GPa) |\n" - "|----------|-----------|----------------|\n" - "| LaH10 | 250 | 200 |\n" - "| H3S | 203 | 150 |\n" - "| YH6 | 224 | 166 |", - title="Tc measurements", - metadata={"source_table": "artifacts/paper.pdf, Table 2"}, -) -``` - -**Figures.** Describe the key quantitative information (values, trends, comparisons) in the claim content. Reference the original figure in metadata for traceability. - -```python -phase_diagram = claim( - "The Tc vs pressure curve shows a dome shape with maximum Tc = 250 K at 200 GPa, " - "decreasing to 200 K at 250 GPa and 180 K at 150 GPa.", - title="Tc-pressure phase diagram", - metadata={ - "figure": "artifacts/images/fig3.png", - "caption": "Fig. 3 | Tc-pressure phase diagram showing dome-shaped dependence.", - }, -) -``` - -**Key principle:** the claim content carries all information needed for judgement. The metadata figure/table reference is for traceability, not for conveying information. - -### Content must be self-contained - -Each node's content must be a complete, independently understandable proposition. A reviewer reading it should not need additional context to make a judgement. - -```python -# BAD: requires context to understand -result = claim("The computed result significantly exceeds conventional estimates.") - -# GOOD: self-contained proposition -result = claim( - "Using method XX to compute YY under condition ZZ yields A +/- delta, " - "compared to the estimate B from conventional method WW, a deviation of approximately C-fold.", - title="Result description", -) -``` - -### Pass 1 reflection - -After extracting all modules, ask yourself: - -- **Theory vs experiment separated?** For every result where the source compares theory to experiment, do I have separate claims for the theoretical prediction and the experimental measurement? If mixed in one claim, Pass 2 cannot wire them with `infer`. -- **Figures and tables transcribed?** Are all key numerical values from figures and tables written into claim content (not just referenced)? -- **Each claim independently judgeable?** Can a reviewer assess each claim without reading any other claim? -- **Contradictory claims identified?** When the source argues "A succeeds where B fails," or compares competing methods / hypotheses, have I extracted both sides as separate claims? These pairs become `contradict(...)` operators in Pass 2, providing strong BP constraints. - -### Marking exported conclusions - -The source's **core contributions** (new theoretical results, new numerical computation results, new experimental findings, key arguments) should be marked as exported conclusions in `__all__`. These are this knowledge package's external interface — other packages can reference them. - -Criterion: if this result were removed from the source, the source would lose its core value. - -When you use `gaia author claim` / `gaia author derive` / etc., the verbs default to `--export` on every Knowledge-producing call; explicitly pass `--no-export` for an internal-only binding. - -### Pass 1 deliverable - -One claim / note / question list per module. - -Pass 1 only extracts atomic, self-contained knowledge nodes. **Do not prejudge which are "derived conclusions"** — whether a claim is an independent premise or a derived one depends on how reasoning connections are established in Pass 2, not on the claim itself. - -## Pass 2 — Connect: write reasoning relations - -Pass 2 wires the knowledge graph. The default starting verb is `infer` (`gaia author infer`) — it is the **most general** way to say "this evidence updates the belief in that hypothesis." Specific strategy types are refined in Pass 4. - -For each claim "supported by other claims," choose one of these author verbs: - -- `gaia author derive --conclusion C --given P1,P2,...` — rigid implication: premises jointly support the conclusion. Use when the source presents a step-by-step derivation that, given the premises, is the intended way to reach the conclusion. To express warrant uncertainty (numerical methods, approximations, omitted conditions), label the `derive` with `--dsl-binding-name`/`--label` and then `gaia author register-prior --claim --value ... --justification ...`. -- `gaia author infer --evidence E --hypothesis H --p-e-given-h ...` — Bayesian update: explicit P(E|H) and (optional) P(E|~H). Use when the source argues "observing E updates belief in H," especially when comparing competing hypotheses against the same observation. -- `gaia author observe --conclusion C [--value ... --error ...]` — raw measurement: ties a Claim, Variable, or Distribution to an observed value. Use for experimental measurements that anchor the graph in data. -- `gaia author compute --conclusion-type T --fn f --given P1,P2,...` — deterministic mapping: a named callable produces the result from the premises. Use when the source presents a closed-form computation whose function is captured by code. -- `gaia author decompose --whole W --parts A,B,... --formula-template and|or|atom` — structural split: composite claim → atomic parts. Use when an aggregate claim is best read as a conjunction (or disjunction) of independently judgeable atoms. -- `gaia author compose --from-file pattern.py` — register a reusable multi-step pattern as a `@compose`-decorated function. Use Pass 4 to refine flat `derive`/`infer` calls into compositions when meaningful intermediate propositions appear. - -Plus the structural-relation verbs (no `--given`; these state a logical constraint between claims): - -- `gaia author equal --a A --b B` — A = B (logically equivalent). -- `gaia author contradict --a A --b B` — NOT (A AND B): both cannot be true, but both can be false. -- `gaia author exclusive --a A --b B` — A XOR B: exactly one must be true (exhaustive + mutually exclusive). - -When in doubt at this pass, reach for `infer` first; Pass 4 will tighten it. - -### Write a detailed `--rationale` - -Summarise the derivation process from the source — not a one-sentence stub, but a complete reasoning chain. The rationale should let a domain reader follow "why these premises lead to this conclusion." - -### Identify premises and background - -- **Claims** used in the derivation → `--given` (the premise list). -- **Notes / questions** used in the derivation → `--background`. - -### Use `@label` and `[@citation]` references in rationales - -In the rationale text, use `@label` to reference knowledge nodes and `[@key]` to cite bibliography entries from `references.json`: - -```python -rationale=( - "Based on the XX framework (@framework_claim), under condition YY (@condition_claim), " - "conclusion ZZ can be derived. The derivation uses the property of WW (@property_note). " - "This follows the approach in [@Dias2020]." -) -``` - -**Knowledge refs** (`@label`): must appear in the verb's `--given` or `--background` list. Verified in Pass 3. - -**Citations** (`[@key]`): must match a key in `references.json`. The strict `[@...]` form raises a compile error if the key is not found. Supports Pandoc group syntax: `[@Bell1964; @CHSH1969]`, `[see @Bell1964, pp. 33-35]`. - -**Rule.** A single `[...]` group must be homogeneous — all knowledge refs or all citations, never mixed. `[@lemma_a; @Bell1964]` is a compile error. - -Citations can also appear in **claim content** to provide traceability: - -```python -tc_measurement = claim( - "The measured superconducting transition temperature is 287.7 K at 267 GPa [@Dias2020].", - title="CSH Tc measurement", -) -``` - -### Do not miss implicit premises - -Sources often have implicit premises. While writing the rationale, if you discover the derivation depends on a knowledge node already extracted in Pass 1, add it to `--given` or `--background` and reference it with `@label` in the rationale. - -### Model contradictions and exclusives - -After wiring derivation / inference relations, model logical constraints between claims using structural verbs. These claim pairs were identified in Pass 1 reflection; now formalize them. - -**Key distinction — get this right, it matters for BP:** - -- `contradict(a, b)` = NOT (A AND B): both cannot be true, but both **can** be false. -- `exclusive(a, b)` = A XOR B: exactly one must be true (exhaustive + mutually exclusive). - -**When to use `contradict`:** the source argues two claims are incompatible — they cannot both hold. Example: two competing hypotheses about a mechanism, where accepting one rules out the other, but a third option might exist. - -```python -not_both = contradict( - claim("The pairing mechanism is phonon-mediated"), - claim("The pairing mechanism is magnon-mediated"), - rationale="Phonon and magnon mechanisms produce incompatible signatures; the data matches only one.", -) -``` - -**When to use `exclusive`:** exactly two exhaustive, mutually exclusive options. One **must** be true. - -```python -one_of = exclusive( - claim("RFdiffusion outperforms Hallucination on this benchmark"), - claim("Hallucination outperforms or matches RFdiffusion on this benchmark"), - rationale="On the same benchmark with the same metric, one must be better or equal.", -) -``` - -**When to use `equal`:** two formulations express the same proposition. - -```python -same = equal( - claim("Energy is conserved in the closed system."), - claim("dE/dt = 0 in the closed system."), - rationale="Word form and differential form of the same statement.", -) -``` - -**When NOT to use either contradict or exclusive:** two claims that are "in tension" but can both be true. Example: "comprehensive improvement across all areas" and "enzyme scaffolding lacks experimental validation" — both can be true (comprehensive improvement does not require every area to have wet-lab validation). Do not model these as `contradict`. Flag them in the critical analysis as unmodelled tensions instead. - -Contradictions and exclusives are especially valuable in BP because they create strong coupling between nodes — when one side's belief goes up, the other must go down. But a **wrong** contradiction silently distorts all downstream beliefs, so always verify semantics in Pass 5. - -### Pass 2 reflection - -Before moving to Pass 3, verify: - -- **Theory-experiment pairs use `infer`?** Every place the source compares a theoretical prediction against an experimental observation should be connected via `infer(evidence=obs, hypothesis=pred, --p-e-given-h ..., --p-e-given-not-h ...)`. The relationship is explanatory ("does the observation support the prediction?"), not a rigid step-by-step derivation. -- **Multiple observations confirming one law?** If several independent observations all support the same general rule, the conclusion claim (the law) should be a `derive(...)` over those observations — and in Pass 4 you will likely refactor that to a `compose`'d pattern that names the generalisation step explicitly. -- **No missing alternatives?** When the source compares competing hypotheses against one observation, every alternative should be extracted as a claim and either chained as additional `infer` evidence or wired with `exclusive` if the source treats the alternatives as exhaustive. -- **Contradictions modelled?** Every contradictory claim pair identified in Pass 1 should now have a `contradict(...)` (or `exclusive(...)`) operator. Also check: did any new contradictions emerge while writing relations? - -## Pass 3 — Check completeness - -**Prerequisite:** code from Pass 1-2 has been written and passes `gaia build compile` and `gaia build check`. Pass 3 combines `gaia build check` feedback with manual review. - -### 3a. Check `@label` and `[@citation]` reference consistency - -Review each relation's rationale one by one: - -1. **Re-read the rationale.** Carefully read every sentence. -2. **Check `@label` coverage.** Every `@label` in the rationale must appear in `--given` or `--background`. -3. **Reverse check.** Every node in `--given` / `--background` should be referenced by `@label` in the rationale (otherwise, why is it a premise?). -4. **Check if additional knowledge is needed.** If the rationale mentions an important fact without a corresponding `@label`, go back to Pass 1 to add it. -5. **Check `[@citation]` coverage.** Key claims and reasoning steps from the source should cite the original via `[@key]`. Ensure `references.json` contains all referenced keys. - -### 3b. Check for claims missing reasoning - -Use `gaia build check` output to see if any claim should have reasoning support but lacks a relation: - -- `gaia build check` reports claims that are not the conclusion of any relation (leaf nodes). -- Review each leaf node: is it truly an independent premise? Or should it have an `infer` / `derive` / `compute` / `observe` relation? -- Criterion: if the source provides an argument for this claim (not just a statement), it should have one. - -### 3c. Check for isolated nodes - -- Are there claims that are neither premise / background of any relation nor conclusion of any relation? -- Isolated nodes indicate they do not participate in the reasoning graph — either they should not exist, or a relation referencing them was missed. - -The most common mistake at this step is **assuming certain knowledge does not need explicit references.** In Gaia, if the reasoning process depends on a fact, that fact must be a node in the knowledge graph. - -## Pass 4 — Refine strategy types - -Passes 2-3 produce a graph dominated by `infer` (the general fall-back). Pass 4 tightens each relation into the most specific verb that still fits the source. - -### Author-verb reference - -| Verb | Semantics | When to use | Author-side cost | -|----------|-----------|-------------|--------------| -| `derive` | Directed implication: premises jointly support conclusion | Step-by-step derivations, theoretical results read off a formal framework, computation-application chains | `register_prior` against the derive's labelled output (or its warrant helper) for residual uncertainty | -| `infer` | Bayesian update: explicit P(E\|H), optional P(E\|~H) | Theory-vs-experiment fit, single-evidence updates to a hypothesis | `--p-e-given-h` (required), `--p-e-given-not-h` (defaults 0.5) | -| `compute` | Deterministic mapping: callable `fn` produces conclusion from premises | Closed-form computations where the function is in code | `--fn` identifier of a callable; conclusion is the function's output Claim | -| `observe` | Measurement event tying Claim / Variable / Distribution to data | Experimental observations that anchor the graph | `--value` / `--error` for quantity form, or discrete observation against a premise list | -| `compose` | Reusable multi-step pattern: `@compose`-decorated function | Recurring derivation patterns that need a named, registered shape | Author the `pattern.py` and register via `gaia author compose --from-file` | -| `decompose` | Structural split: composite → atomic parts via `and`/`or`/`atom` | Aggregate claim is best read as the conjunction of independently judgeable parts | `--formula-template` or `--formula-expr` | - -Also available as **structural verbs** (modelled in Pass 2 alongside the rest, not in Pass 4): - -| Verb | Semantics | When to use | -|----------|-----------|-------------| -| `contradict(a, b)` | NOT (A AND B) — cannot both be true | Incompatible hypotheses | -| `exclusive(a, b)` | A XOR B — exactly one true | Exhaustive binary choice | -| `equal(a, b)` | A = B — logically equivalent | Two formulations of the same proposition | - -### Decision tree - -``` -For each `infer` relation drafted in Pass 2: - - Is the conclusion a measured datum (or a Variable/Distribution observed at a value)? - YES → observe - NO ↓ - Is the conclusion produced by a closed-form computation in code (named callable f over premises)? - YES → compute - NO ↓ - Does the source present this as a deterministic step-by-step derivation that, given the premises, - is the intended way to reach the conclusion (with at most residual numerical or approximation uncertainty)? - YES → derive (optionally register_prior against the derive's labelled output for warrant uncertainty) - NO ↓ - Is this a Bayesian update where the evidence's likelihood under hypothesis and under its negation - is what carries the inferential weight (e.g. theory predicts X, experiment measured X')? - YES → infer (with explicit --p-e-given-h, and --p-e-given-not-h when known) - NO ↓ - Is the conclusion best read as the conjunction or disjunction of independently judgeable atomic parts? - YES → decompose (--formula-template and|or|atom) - NO ↓ - Does the same multi-step pattern recur across multiple conclusions, and is naming intermediate - propositions worthwhile? - YES → compose (extract into a @compose pattern; per-call the wrapper authors a derive over - the composition's intermediate Claims) - NO → keep infer (with the most informative likelihood you can justify) -``` - -### Recasting legacy reasoning patterns - -The release/0.4 SKILL talked about several named reasoning patterns. Several have clean v0.5 idioms; some do not. Be honest about the gap. - -**Strict mathematical deduction** ("if all premises true, conclusion necessarily true"): use `derive` and omit the warrant prior (or set it very close to 1). `derive` carries the same skeleton (conjunction + directed implication); leaving the warrant near 1 expresses determinism. There is no separate "deduction" verb in v0.5. - -**Soft / probabilistic support** ("premises usually imply the conclusion, with uncertainty"): use `derive` for the relation, then reach for `gaia author register-prior --claim --value ... --justification ...` against the `derive`'s labelled output Claim (or its auto-generated warrant helper) to express the residual uncertainty (numerical methods, approximations, omitted conditions). The engine's `derive(...)` signature does not accept an inline `prior=` — warrant priors are attached via `register_prior`. - -**Theory-experiment comparison ("abduction")**: extract the theoretical prediction and the experimental observation as separate claims (Pass 1), then use `infer(evidence=obs, hypothesis=pred, --p-e-given-h ...)`. When several alternative theories compete, chain `infer` against each candidate hypothesis with its own likelihoods. When the alternatives are mutually exclusive in the paper's framing, add `exclusive(a, b)` for the two-alternative case or `decompose --formula-template or` for three or more (`exclusive` is strictly binary). The abduction *concept* — the prior on the alternative reflects explanatory power for the specific observation, not the alternative's truth in general — survives intact; that deep guide lives in `../gaia-review/SKILL.md`. - -**Repeated-observation generalisation ("induction")**: there is no single v0.5 verb. The recommended idiom is `derive` over a `compose`'d generalisation step. Specifically: author each observation as its own claim, then either (a) for the simple flat case, `derive(law, given=[obs_a, obs_b, obs_c], rationale=...)`, or (b) when the generalisation involves a named pattern, define a `@compose` function that takes the observations and the law and returns the law's `derive` step, and register it via `gaia author compose --from-file`. The underlying judgement — each observation must be **independent**; if dependent, extract the shared dependency as an explicit claim in Pass 5 — still applies. - -**Process of elimination, proof by cases, mathematical induction, cross-system analogy, extrapolation beyond measured range:** these patterns **have no single-verb v0.5 form**. The recommended idiom for each: - -- *Process of elimination:* `decompose --formula-template or` over the exhaustive option set + `derive(survivor, given=[evidence_eliminating_alt_1, evidence_eliminating_alt_2, ...])`. The disjunctive decomposition guarantees the survivor must be the one true option; the `derive` carries the per-alternative refutation reasoning. (`exclusive(a, b)` is strictly binary — exactly two options — so it only fits the n=2 case; for n≥3 alternatives use `decompose --formula-template or`.) -- *Proof by cases:* one `derive(conclusion, given=[case_k_premise, conclusion_holds_in_case_k])` per case, plus a `decompose --formula-template or` over the case predicates (or `exclusive(a, b)` when there are exactly two cases — `exclusive` is binary only). -- *Mathematical induction:* one `derive` for the base case, one `derive` for the inductive step (`P(n) ⇒ P(n+1)`), and a `derive(for_all_law, given=[base_case, inductive_step])` whose rationale references the inductive schema. **The engine does not enforce the inductive schema** — it treats this as a generic two-premise `derive`. The author must carry the "this is induction over N" framing in the `rationale` text, and the Pass 5 reviewer must verify the base case + step actually warrant the universal. Do not assume the engine guarantees the quantifier reasoning. -- *Analogy* and *extrapolation:* author the structural-similarity / continuity premise as a `claim`, then `derive(target, given=[source, similarity_premise])` or `derive(extrapolated, given=[measured_range_result, continuity_premise])`. The justification quality lives in the premise prior plus the `derive` warrant prior — see `../gaia-review/SKILL.md`. - -If your source has a derivation that does not map cleanly onto any of these idioms, that is signal: capture the gap in `ANALYSIS.md` under "unmodelled reasoning" so a reviewer can examine it. - -### Strategy variable naming - -Every relation that produces a Claim or warrant **must** be assigned to a named public variable (no `_` prefix). This is required so that the relation appears in `gaia build check --brief` output and can be referenced by `priors.py` and downstream verbs. - -When using `gaia author `, set `--dsl-binding-name` (Python LHS) and `--label` (engine `label=` kwarg) together for any relation that needs to be cited downstream. Use descriptive names like `derive_tc_al`, `compose_workflow`, `infer_theory_vs_exp`. - -### Claim variable naming - -Every Claim **must** be assigned to a named variable (no `_` prefix for claims that need to be visible). Anonymous `claim()` calls or `_`-prefixed claims will not get labels and become invisible in CLI output. The only exception: `__` double-underscore prefix is reserved for compiler-generated helper Claims. - -### When to reach for `compose` - -`compose` is the v0.5 way to capture **complex reasoning with meaningful intermediate steps**. Two triggers: - -1. **3+ premises and no `decompose` fit.** A flat `derive` over 4+ premises suffers the BP multiplicative effect — small uncertainties on each premise compound on the conclusion. If you can name meaningful intermediate propositions (not stubs introduced purely to split the call), refactor into a `@compose` pattern whose intermediate Claims are independently judgeable. -2. **Recurring pattern.** The same shape of derivation appears across multiple conclusions. Register it once via `gaia author compose --from-file` and reuse. - -If decomposition would be forced — no meaningful intermediate proposition exists — 3 premises is acceptable to keep as `derive` or `infer`; 4+ premises must decompose, otherwise BP multiplicative effect will severely suppress belief. - -### Pass 4 reflection - -After refining all relations, verify: - -- **Every theory-vs-experiment `infer` has a meaningful alternative?** When the source compares competing hypotheses, did you extract each alternative and either chain `infer` against it or wire `exclusive` across the candidates? Remember: the prior on the alternative reflects its **explanatory power** for the specific observation, not its truth in general — see `../gaia-review/SKILL.md` for the deep guide. -- **Each repeated-observation `derive` over independent observations?** For `derive(law, given=[obs_a, obs_b, ...])`, each observation should provide independent evidence. If observations are dependent (shared sample, shared instrument), extract the shared dependency as an explicit claim in Pass 5. -- **`infer` likelihoods anchored?** Every `infer` call has `--p-e-given-h` from the source. If `--p-e-given-not-h` is left at 0.5, it is a fall-back — when the source's framing supplies a competing-explanation likelihood, set it explicitly. - -### Post-refinement check - -After refining all relations, check the **verb distribution**: - -- If `derive` accounts for more than 70% of relations, review whether some should be `infer` (theory-vs-experiment fit) or `compose`'d (multi-step generalisation). -- Papers with extensive experimental validation typically have many `infer` calls. -- Discussion / conclusion sections that synthesise multiple results often have a `compose`'d generalisation step. - -Also check **reasoning chain depth** (hops from leaf to exported conclusion): - -- Maximum recommended depth: **3 hops**. -- If a derived conclusion has belief < 0.4, the chain is likely too deep. -- Fix by flattening: make intermediate claims into leaf premises, or restructure into wider (more premises per relation) rather than deeper (more relations in series). - -## Pass 5 — Verify structural integrity - -**Prerequisite:** Pass 4 is complete — all relation types are finalised. This pass checks that the factor graph correctly represents the source's reasoning. It must happen after Pass 4 because verb refinement (especially `compose`'d patterns) changes the graph topology. - -**Background.** Gaia uses Junction Tree (exact inference). There is no algorithmic double-counting — given any factor graph, JT computes correct posteriors. All issues in this pass are about whether the **model** correctly represents reality: each factor (relation / structural verb) should represent a genuinely independent constraint, and each structural verb's logical semantics should match the actual relationship. - -### 5a. Verify structural-verb semantics - -Check structural verbs first — if the graph's hard constraints are wrong, everything downstream is wrong too. - -Review every `contradict(...)`, `exclusive(...)`, and `equal(...)` call: - -**`contradict(a, b)` = NOT (A AND B)**: both cannot be true, but both **can** be false. - -```python -# WRONG: these can both be true — no contradiction! -contradict( - claim("RFdiffusion succeeds at designing large proteins"), - claim("Hallucination fails at designing large proteins"), -) - -# CORRECT: these cannot both be true -contradict( - claim("RFdiffusion is inferior to Hallucination on this task"), - claim("RFdiffusion outperforms Hallucination on this task"), -) -``` - -**`exclusive(a, b)` = A XOR B**: exactly one must be true. Stronger than `contradict`. - -**Three-question checklist for each structural verb call:** -1. Can both claims be true simultaneously? If yes → not a `contradict`, remove it. -2. Can both claims be false simultaneously? If no → should be `exclusive` (XOR), not `contradict` (NAND). -3. Is this just "in tension" rather than logically exclusive? Informal tension should NOT be modelled as `contradict` — flag in critical analysis instead. - -### 5b. Eliminate double counting - -Each factor in the factor graph represents an **independent constraint**. If the same argument appears as two factors, the model claims two independent constraints exist when there is only one. This inflates beliefs — not because JT miscalculates, but because the model is wrong. - -**The unified principle:** every factor must bring genuinely new information that no other factor already provides. When implicit dependencies exist, make them explicit as variables in the graph so JT can correctly reason about them. - -**Pattern 1 — Redundant relations (same reasoning expressed twice):** - -```python -# 1a. Exact duplicate: standalone derive + a derive inside a compose'd generalisation -derive(law, given=[obs], rationale="law predicts obs") -derive_law_from_obs = derive(law, given=[obs_a, obs_b, obs], rationale="...") # internally re-uses obs -# FIX: remove the standalone derive, or fold it into the compose pattern. - -# 1b. Transitive shortcut: A→B→C chain + A→C that is just the chain compressed -derive(B, given=[A], rationale="A implies B") -derive(C, given=[B], rationale="B implies C") -derive(C, given=[A], rationale="A implies B implies C") # redundant with the chain -# FIX: remove the shortcut, OR confirm it represents a genuinely different argument. - -# 1c. Derived premise redundancy: A→B, then derive(C, given=[A, B]) where A supports C only through B -derive(B, given=[A], rationale="A implies B") -derive(C, given=[A, B], rationale="A leads to B which leads to C") -# FIX: remove A from C's premises → derive(C, given=[B], ...). -``` - -**Pattern 2 — Hidden evidence in rationale text:** - -Two relations with identical premises but different `rationale` text. The different reasoning contains evidence not captured as premises — extract it. - -```python -# BEFORE: same premises, different reasoning angles -derive(law, given=[sample, obs_R], rationale="Zero resistance = hallmark of SC") -derive(law, given=[sample, obs_R], rationale="Transition width < 0.5 K = bulk SC") -# The "transition width < 0.5 K" is evidence hidden in the rationale text. - -# AFTER: extract hidden evidence as a claim -transition_sharpness = claim("Resistivity transition width < 0.5 K") -derive(law, given=[sample, obs_R], rationale="Zero resistance = hallmark of SC") -derive(law, given=[sample, transition_sharpness], rationale="Sharp transition = bulk SC") -``` - -**Pattern 3 — Unmodelled shared dependencies:** - -Two observations share a common cause (same sample, same instrument) but the cause is not in the graph. The model treats them as unconditionally independent, losing their correlation. - -```python -# BEFORE: shared sample quality is implicit — correlation lost -obs_R = claim("Sample A: Tc = 39 K by resistivity") -obs_chi = claim("Sample A: Tc = 39 K by susceptibility") -derive(law, given=[obs_R, obs_chi], rationale="...") - -# AFTER: extract shared dependency — correlation preserved -sample_quality = claim("Sample A is high-quality single crystal, confirmed by XRD") -derive(obs_R, given=[sample_quality], rationale="Resistivity depends on @sample_quality") -derive(obs_chi, given=[sample_quality], rationale="Susceptibility depends on @sample_quality") -derive(law, given=[obs_R, obs_chi], - rationale="Conditionally independent given sample_quality") -``` - -You cannot create new experiments — you formalize what the paper provides. The table below guides the modelling choice: - -| Observation relationship | Modelling approach | -|--------------------------|-------------------| -| Truly independent (different samples, different labs) | `derive(law, given=[obs_a, obs_b, ...])` directly | -| Partially independent (shared dependency + independent components) | Extract shared dependency as an explicit claim | -| Completely redundant (same data rephrased) | Merge into a single claim | - -**Pattern 4 — `equal` + separate relations:** - -`equal(a, b)` couples two claims. If both sides have relations to the same target, check whether each relation brings information beyond what `equal` already propagates. - -```python -equal(claim_A, claim_B) -derive(law, given=[claim_A], rationale="argument from A's perspective") -derive(law, given=[claim_B], rationale="argument from B's perspective") - -# Ask: does the B→law relation add information that A→law + equal doesn't already provide? -# If NO: remove B→law. -# If YES: extract the additional information as a new premise. -``` - -**How to check (procedure):** - -1. List every claim with 2+ incoming relations. -2. For each pair of relations: "does each bring genuinely independent new information?" -3. For each `derive` over multiple observations: "do the observations share unmodelled dependencies?" -4. For each `equal`: "do both sides need their own relations to the same target?" -5. For all relations: "does the rationale text contain evidence not captured as premises?" -6. For all `infer` calls: "is `--p-e-given-h` set from a source-supported value, and is `--p-e-given-not-h` the right alternative-likelihood (not a stand-in 0.5 when the source actually argued an alternative)?" - -### 5c. Re-compile and verify - -After any structural changes in Pass 5, run `gaia build compile` + `gaia build check` + `gaia run infer` and compare beliefs to before. A significant belief drop after removing a relation suggests the previous value was inflated by double counting. - -## Pass 6 — Polish for standalone readability - -**Prerequisite:** the knowledge graph is structurally correct (Pass 5 complete). Pass 6 ensures that every claim, rationale, and metadata entry is independently understandable without access to the original source. - -### 6a. Claim self-containedness - -Review every claim for standalone readability: - -**Symbols must be self-explanatory.** -- Every mathematical symbol must have a brief explanation on its first appearance in that claim. -- Example: do not write "$\alpha \ll 1$"; write "the parameter $\alpha$ (ratio of XX to YY) is much less than 1". -- The physical meaning of subscripts / superscripts must be explicit. - -**Abbreviations must be expanded.** -- Every abbreviation must be expanded on its first appearance in that claim. -- Example: do not write "XXX computes $\lambda$"; write "the such-and-such method (XXX) computes the coupling constant $\lambda$". -- Even if an abbreviation has been expanded in another claim, each claim is independent and must expand it again. - -**No comparative assertions without reference.** -- Do not write "significantly larger than X" — the reader does not know what is being compared. -- Do not write "nearly exact agreement" — the reader does not know what it agrees with. -- Numerical comparisons must provide both values. - -**Sufficient detail.** -- Can a reader understand what this claim says by reading only this one claim? -- Are conditions and applicable ranges clear? -- Do numerical values include units and error bars? - -### 6b. Data formatting - -- Tabular data should use markdown tables in claim content. -- Key numerical values from figures must be transcribed into the claim text (not just referenced). -- Trends described in prose should include specific data points. - -### 6c. Rationale standalone readability - -Review every relation's `rationale` text: - -- The rationale should be a complete reasoning chain, not "see Section 3 of the paper." -- Specific numbers, method names, and conditions should be stated, not implied. -- Every `@label` reference should have enough surrounding context that a reader unfamiliar with the label can follow the argument. - -### 6d. Figure and table references - -Add `metadata={"figure": "...", "caption": "..."}` to every claim whose content comes from a specific figure or table: - -1. **Coverage.** Check each module against the source for missing references. -2. **Path validity.** Verify each file path exists in `artifacts/`. -3. **Caption accuracy.** Copy the figure caption from the source (abbreviated OK, but figure number and key content must be correct). -4. **Relation metadata.** Relations whose `rationale` references figure data should also carry `metadata`. - -### 6e. Complete citation metadata - -During Passes 1-4, `references.json` entries were kept minimal (key + type + title). Now fill in complete metadata for all cited references: - -- **author** — full author list (`[{"family": "...", "given": "..."}]`). -- **issued** — publication date (`{"date-parts": [[2020]]}`). -- **container-title** — journal / conference name. -- **volume**, **page**, **DOI** — where applicable. - -Verify: every `[@key]` used in claims and rationales has a corresponding entry in `references.json`. Run `gaia build compile .` to catch any missing keys (strict `[@key]` form raises a compile error if the key is not found). - -### 6f. Format consistency - -- Metadata format should be consistent across all claims (same key names, same path conventions). -- Titles should follow a consistent naming style. -- Cross-module import patterns should be uniform. +## Progressive Workflow + +After Pass 0, create a session todo list with the seven items below. Mark only +Pass 1 in progress. Do not load a later pass's reference file until the current +pass is complete **and** its compile + check inner loop passes — each pass +builds on the working state the earlier passes produced. + +1. **Pass 1 — Extract knowledge nodes** — load + [`references/pass-1-extract.md`](references/pass-1-extract.md). +2. **Pass 2 — Connect: write reasoning relations** — load + [`references/pass-2-connect.md`](references/pass-2-connect.md). +3. **Pass 3 — Check completeness** — load + [`references/pass-3-completeness.md`](references/pass-3-completeness.md). +4. **Pass 4 — Refine strategy types** — load + [`references/pass-4-strategy-types.md`](references/pass-4-strategy-types.md). +5. **Pass 5 — Verify structural integrity** — load + [`references/pass-5-structural-integrity.md`](references/pass-5-structural-integrity.md). +6. **Pass 6 — Polish for standalone readability** — load + [`references/pass-6-polish.md`](references/pass-6-polish.md). +7. **Prior assignment, inference, ANALYSIS.md, render** — load + [`references/priors-analysis-render.md`](references/priors-analysis-render.md). + +Run the compile + check inner loop (below) after every pass. The six-pass +split is cumulative scaffolding — the emitted package must reflect all passes +as one coherent body of work, not six independent passes. ## Inner loop: compile + check after every pass @@ -791,121 +188,6 @@ gaia build check --show label # detail view of a specific claim's warra - Claims should show their role (independent / derived / structural / background / scaffolded / orphaned) and prior if set. - Use `--show ` to inspect full claim content and warrant trees for review readiness. -## Prior-assignment tail - -After Pass 6, you have a structurally complete graph and a passing `gaia build check`. Now assign priors and run inference. - -### Write `priors.py` - -`priors.py` assigns priors to leaf claims. Warrant priors on `derive` (and `infer` / `compute` where relevant) are set by `gaia author register-prior --claim --value ... --justification ...` against the verb's labelled output Claim (or its auto-generated warrant helper). The engine's verb signatures do not accept an inline `prior=` kwarg — `register_prior` is the only path. - -**Before writing `priors.py`, run `gaia build check --hole .`** to see exactly which independent claims need priors, along with their content and current status. Use this as your checklist — address each hole, then re-run `gaia build check --hole .` to confirm "All independent claims have priors assigned." - -The CLI shortcut is: - -```bash -gaia author register-prior \ - --claim my_leaf_claim \ - --value 0.85 \ - --justification "Well-established by [@Smith2020] in the same regime." \ - --file priors.py -``` - -That command appends a `register_prior(...)` statement to `priors.py` and auto-injects the import if the target file is a sibling of `__init__.py`. - -**Do NOT set priors for derived claims.** The inference engine automatically assigns uninformative priors (0.5) to derived claims. Their beliefs are determined entirely by BP propagation from leaf premises. Setting an explicit prior on a derived claim double-counts evidence: the reviewer's judgement and the reasoning chain both reflect the same underlying data. Only set priors for independent (leaf) claims that are not the conclusion of any relation. - -**The π(Alt) discipline (`infer` alternatives) deserves special attention.** In the abductive pattern (theory-vs-experiment `infer`), the prior on the alternative reflects its **explanatory power for the specific observation**, not whether the alternative's computation is correct in general. The most common and consequential mistake in prior assignment is setting π(Alt) based on "the alternative's calculation is right," rather than "the alternative explains the observation." The deep guide — worked examples, rule-of-thumb checks, the explanatory-power-vs-correctness distinction — lives in `../gaia-review/SKILL.md`. Read it before writing the prior on any abductive alternative. - -The full prior-assignment guide (evidence-level → prior-range tables, warrant-prior ranges, iteration loop) also lives in `../gaia-review/SKILL.md`. This skill points at it; do not duplicate the tables here. - -### Run inference - -```bash -gaia run infer # writes .gaia/beliefs.json -gaia run infer --depth 1 # joint cross-package inference (direct deps) -gaia run infer --depth -1 # joint cross-package inference (all transitive deps) -``` - -### Interpret BP results - -Read the table in `../_shared/bp-interpretation.md`. Do not duplicate the interpretation table here — that reference is the single canonical copy. The shape of the loop: - -``` -gaia run infer → .gaia/beliefs.json → interpret per ../_shared/bp-interpretation.md - ↓ - structural issues → back to Pass 1-5 (revise graph) - prior issues → revise priors.py (revisit ../gaia-review/SKILL.md guide) - otherwise → proceed to ANALYSIS.md -``` - -If results are clearly wrong (a well-supported conclusion has belief < 0.3, or a contradict relation does not pick a side), go back and check: - -1. **Structural issue?** (→ revisit Pass 1-5.) Missing premises, wrong relation verb, missing alternative for an `infer`, evidence double-counting. -2. **Parameter issue?** (→ revisit `priors.py`.) Priors too low / high, `--p-e-given-h` miscalibrated, π(Alt) reflecting computational correctness instead of explanatory power. - -## Generate the GitHub presentation - -After the prior-assignment tail produces beliefs you trust, hand off to `../gaia-publish/SKILL.md`: - -```bash -gaia run render --target github # .github-output/ README + narrative outline -gaia run render --target docs # per-module Mermaid graphs in docs/detailed-reasoning.md -gaia run render --target obsidian # gaia-wiki/ skeleton (hands off to ../gaia-obsidian-wiki/SKILL.md) -``` - -`../gaia-publish/SKILL.md` carries the README narrative discipline (per-conclusion evidence assessment, Weak Points framed around internal nodes, Evidence Gaps by theme). `../gaia-obsidian-wiki/SKILL.md` carries the rich-vault discipline (claim pages with full derivations, section pages as narrative chapters). - -## `ANALYSIS.md` — critical analysis deliverable - -After BP results stabilise, produce a **critical analysis** of the source. This is the analytical payoff of formalization — by building the knowledge graph, you now understand the argument's structure well enough to identify its strengths and weaknesses. - -`ANALYSIS.md` lives in the package root and is a **required deliverable** — do not skip it. The required sections: - -### 1. Package statistics - -Knowledge graph counts (claims by role, relations by verb, structural-verb counts), verb-type distribution, claim role classification, figure reference coverage, BP result summary. - -### 2. Summary - -One paragraph on the argument's overall structure and strength. - -### 3. Weak points (table) - -Internal nodes with low belief. **Internal nodes, not exported conclusions** — exported conclusions go in the README's Reasoning Structure section (`../gaia-publish/SKILL.md`); `ANALYSIS.md` Weak Points is for the load-bearing intermediate nodes whose fragility threatens the whole chain. - -Columns: claim, belief, issue. Include all derived claims with belief < 0.8 and any `infer`-alternative claims with belief > 0.25. - -Vulnerability signals to capture in the "issue" column: - -| Signal | What it means | -|--------|---------------| -| Derived conclusion with low belief (< 0.5) | Weak premise support or fragile reasoning chain | -| Long reasoning chain (4+ hops from leaf to conclusion) | Multiplicative effect — small uncertainties compound | -| `infer` alternative π(Alt) ≈ π(H) | Alternative is equally plausible — evidence does not distinguish | -| Leaf claim with low prior and many downstream dependents | Single weak foundation supporting many conclusions | -| `derive` warrant with very low prior (< 0.3) | Reviewer flagged this step as unreliable | -| Claim marked as `note` that could be questioned | Hidden assumption not subject to BP updating | - -### 4. Evidence gaps (tables, grouped by theme) - -Group by theme: **experimental**, **computational**, **theoretical**. Within each, identify where additional evidence would most strengthen the argument. For each gap: which conclusions improve if filled. Prioritise by impact. - -- **Unsupported leaf claims:** claims with no reasoning support that the source takes as given — what evidence could back them up? -- **Weak `infer` alternatives:** where the alternative nearly matches the hypothesis in explanatory power — what new observation could break the tie? -- **Missing comparisons:** theoretical predictions without experimental validation — what experiment could test them? -- **Single-observation generalisations:** laws supported by only one observation — what additional observations would strengthen the `derive`? - -### 5. Contradictions - -(a) Explicit `contradict(...)` relations modelled and how BP resolved them (which side won). (b) Internal tensions in the source that were not modelled as formal contradictions but are worth flagging. - -### 6. Confidence assessment - -Tier the exported claims into confidence levels (very high / high / moderate / tentative) with belief ranges. - -The critical analysis transforms a qualitative reading of the source into a quantitative structural assessment. Every knowledge package should ship with one. - ## Common mistakes | Mistake | Consequence | Fix | @@ -932,9 +214,31 @@ The critical analysis transforms a qualitative reading of the source into a quan | Setting prior on derived claim | Double-counts evidence | Do not set priors for derived claims; inference engine defaults to 0.5 | | Observation claim missing prior (classified as derived because it has incoming supports) | Observation's empirical grounding lost; belief depends entirely on theory relations instead of being anchored by data | Add observation to `priors.py` with high prior (0.9+), or use `observe` to tie it directly to a measurement value | -## See also +## Reference Files + +### Passes (this skill) + +- [`references/pass-1-extract.md`](references/pass-1-extract.md) — extract `claim` / `note` / `question` knowledge nodes. +- [`references/pass-2-connect.md`](references/pass-2-connect.md) — wire reasoning relations and structural verbs. +- [`references/pass-3-completeness.md`](references/pass-3-completeness.md) — `@label` / citation consistency, missing reasoning, isolated nodes. +- [`references/pass-4-strategy-types.md`](references/pass-4-strategy-types.md) — tighten `infer` into the most specific verb. +- [`references/pass-5-structural-integrity.md`](references/pass-5-structural-integrity.md) — structural-verb semantics and double-counting. +- [`references/pass-6-polish.md`](references/pass-6-polish.md) — self-containedness, figures, citation metadata. +- [`references/priors-analysis-render.md`](references/priors-analysis-render.md) — `priors.py`, inference, `ANALYSIS.md`, render handoff. + +### Shared formalization methodology (`../_shared/`) + +Shared with `gaia-formalize-coarse`; loaded by the passes that need them: + +- [`../_shared/formalize-extract-conclusions.md`](../_shared/formalize-extract-conclusions.md) — what counts as a conclusion, fidelity, self-contained bodies, figures as prose, `refs` whitelist, citation form (Pass 1). +- [`../_shared/formalize-atomicity.md`](../_shared/formalize-atomicity.md) — one claim = one citable question, under-splitting traps, the two tests (Pass 1). +- [`../_shared/formalize-reasoning-chains.md`](../_shared/formalize-reasoning-chains.md) — logic graph, topological order, reasoning-trace reconstruction, step rules (Pass 2). +- [`../_shared/formalize-independence.md`](../_shared/formalize-independence.md) — no-double-counting check, the four patterns, shared-factor extraction (Pass 5). +- [`../_shared/bp-interpretation.md`](../_shared/bp-interpretation.md) — interpreting `.gaia/beliefs.json` (prior-assignment tail). + +### Sibling skills -- `../_shared/bp-interpretation.md` — single canonical reference for interpreting `.gaia/beliefs.json` (normal vs abnormal patterns for premises, derived conclusions, `contradict` / `exclusive` sides; common problems and fixes). -- `../gaia-review/SKILL.md` — prior-assignment guide (evidence-level → prior-range tables, warrant priors, π(Alt) explanatory-power semantics, iteration loop). -- `../gaia-publish/SKILL.md` — README narrative discipline after `gaia run render --target github`. -- `../gaia-obsidian-wiki/SKILL.md` — rich Obsidian-vault discipline after `gaia run render --target obsidian`. +- [`../gaia-formalize-coarse/SKILL.md`](../gaia-formalize-coarse/SKILL.md) — the quick four-phase single-pass sibling, for a fast first cut of one paper. +- [`../gaia-review/SKILL.md`](../gaia-review/SKILL.md) — prior-assignment guide (evidence-level → prior-range tables, warrant priors, π(Alt) explanatory-power semantics, iteration loop). +- [`../gaia-publish/SKILL.md`](../gaia-publish/SKILL.md) — README narrative discipline after `gaia run render --target github`. +- [`../gaia-obsidian-wiki/SKILL.md`](../gaia-obsidian-wiki/SKILL.md) — rich Obsidian-vault discipline after `gaia run render --target obsidian`. diff --git a/gaia/_skills/gaia-formalize-fine/references/pass-1-extract.md b/gaia/_skills/gaia-formalize-fine/references/pass-1-extract.md new file mode 100644 index 000000000..17b76311c --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/pass-1-extract.md @@ -0,0 +1,103 @@ +# Pass 1 — Extract knowledge nodes + +Load this file when starting Pass 1. When the pass is complete, run the +compile + check inner loop (see `../SKILL.md` → "Inner loop") and then load +`pass-2-connect.md`. + +Read the source **section by section**. For each section, identify: + +| Type | Criterion | Examples | Author verb | +|------|-----------|---------|---| +| **note** | Background facts that cannot be questioned | Mathematical definitions, formal setups, fundamental principles | `gaia author note` | +| **claim** | Propositions that can be questioned or falsified | Computation results, theoretical derivations, predictions, experimental observations | `gaia author claim` | +| **question** | Open research questions | Driving questions for the source | `gaia author question` | + +### Organize by module + +Each source section corresponds to one Gaia module (Python file): + +- Introduction → `motivation.py` +- Section II → `s2_xxx.py` +- ... + +The module's docstring serves as the section heading. Each knowledge node should have a `title` parameter. Add modules with `gaia pkg add-module` (see `../SKILL.md` → "CLI invocations"). + +### Place knowledge in the earliest module + +Each knowledge node belongs in the module corresponding to the section where it **first appears** in the source. Content from the Introduction goes into `motivation.py`. Claims in `motivation.py` can be freely referenced as premises or background by later modules — they are not restricted by module membership. Notes and questions are typically referenced via `background=`. + +### `note` vs `claim` classification guide + +**Principle: when in doubt between `note` and `claim`, mark it as `claim`.** + +| Category | Type | Examples | +|----------|------|---------| +| Mathematical definitions / formal setups | **note** | Coordinate system choice, variable decomposition definitions, mathematical form of potentials | +| Established fundamental principles | **note** | Conservation laws, exclusion principle, laws of thermodynamics | +| Standard approximation / method definitions (without applicability assertions) | **note** | Mathematical expression of an approximation (definition only, not asserting applicability) | +| Whether applicability conditions hold | **claim** | Whether an approximation applies to a specific system | +| Theoretical frameworks dependent on conditions | **claim** | "Theorem B holds when A is satisfied" | +| Theoretical derivation results | **claim** | Renormalization relations, scaling laws, asymptotic behaviour | +| Numerical computation results | **claim** | Values from computational methods | +| Experimental observations | **claim** | Measured quantities | + +**Key criterion:** can this proposition be questioned? If yes → `claim`. Only mathematical definitions and formal setups qualify as notes. + +**Distinguish definitions from assertions.** The mathematical definition of an approximation is a note; "this approximation is unreliable under certain conditions" is a claim. "Decompose the variable into high- and low-frequency parts" is a note (mathematical operation), but "the contribution of the high-frequency part is negligible" is a claim (physical assertion). + +**Dependency chains.** If A is a note and B depends on A being true while containing a physical assertion — B is typically a claim. + +Content that the source itself derives — even when the derivation is rigorous — should be a claim, because the derivation process itself may contain errors. + +### Shared extraction methodology + +The rules for writing claim content — content format, **atomicity**, figures +and tables transcribed as prose, self-contained bodies — are shared with +`gaia-formalize-coarse` and live in `_shared/`. Load and apply both: + +- [`../../_shared/formalize-extract-conclusions.md`](../../_shared/formalize-extract-conclusions.md) + — fidelity to the source, self-contained claim bodies, content format + (Markdown tables, `$...$` math, lists), figures and tables transcribed as + prose, the no-paper-internal-pointer rule, the `refs` whitelist, and + citation form. It also states the rule to **extract both sides of a + theory-vs-experiment comparison** and **every observation in a + repeated-observation set** as separate claims, so Pass 2 can wire them + (`infer` for theory-vs-experiment; `derive` over the observations for a + generalisation — see Pass 2 and Pass 4). +- [`../../_shared/formalize-atomicity.md`](../../_shared/formalize-atomicity.md) + — one claim = one citable question, the theory/experiment and + method/result separation corollaries, the under-splitting traps, the split + and standalone-citation tests. + +Fine-specific points beyond the shared rules: + +- The `note` vs `claim` classification above is unique to this skill; + `gaia-formalize-coarse` emits no `note`. +- Artifact file paths for rendering + (`metadata={"figure": "...", "caption": "..."}`) are added in Pass 6, not + here — see [`pass-6-polish.md`](pass-6-polish.md). They complement the + shared `refs` whitelist: `refs` records provenance pointers, + `metadata.figure` records the artifact path the renderer needs. + +### Pass 1 reflection + +After extracting all modules, ask yourself: + +- **Theory vs experiment separated?** For every result where the source compares theory to experiment, do I have separate claims for the theoretical prediction and the experimental measurement? If mixed in one claim, Pass 2 cannot wire them with `infer`. +- **Figures and tables transcribed?** Are all key numerical values from figures and tables written into claim content (not just referenced)? +- **Each claim independently judgeable?** Can a reviewer assess each claim without reading any other claim? +- **Contradictory claims identified?** When the source argues "A succeeds where B fails," or compares competing methods / hypotheses, have I extracted both sides as separate claims? These pairs become `contradict(...)` operators in Pass 2, providing strong BP constraints. + +### Marking exported conclusions + +The source's **core contributions** (new theoretical results, new numerical computation results, new experimental findings, key arguments) should be marked as exported conclusions in `__all__`. These are this knowledge package's external interface — other packages can reference them. + +Criterion: if this result were removed from the source, the source would lose its core value. + +When you use `gaia author claim` / `gaia author derive` / etc., the verbs default to `--export` on every Knowledge-producing call; explicitly pass `--no-export` for an internal-only binding. + +### Pass 1 deliverable + +One claim / note / question list per module. + +Pass 1 only extracts atomic, self-contained knowledge nodes. **Do not prejudge which are "derived conclusions"** — whether a claim is an independent premise or a derived one depends on how reasoning connections are established in Pass 2, not on the claim itself. diff --git a/gaia/_skills/gaia-formalize-fine/references/pass-2-connect.md b/gaia/_skills/gaia-formalize-fine/references/pass-2-connect.md new file mode 100644 index 000000000..0b10100af --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/pass-2-connect.md @@ -0,0 +1,124 @@ +# Pass 2 — Connect: write reasoning relations + +Load this file after Pass 1 is complete and its compile + check loop passes. +When this pass is done, run the inner loop again and load +`pass-3-completeness.md`. + +Pass 2 wires the knowledge graph. The default starting verb is `infer` (`gaia author infer`) — it is the **most general** way to say "this evidence updates the belief in that hypothesis." Specific strategy types are refined in Pass 4. + +For each claim "supported by other claims," choose one of these author verbs: + +- `gaia author derive --conclusion C --given P1,P2,...` — rigid implication: premises jointly support the conclusion. Use when the source presents a step-by-step derivation that, given the premises, is the intended way to reach the conclusion. To express warrant uncertainty (numerical methods, approximations, omitted conditions), label the `derive` with `--dsl-binding-name`/`--label` and then `gaia author register-prior --claim --value ... --justification ...`. +- `gaia author infer --evidence E --hypothesis H --p-e-given-h ...` — Bayesian update: explicit P(E|H) and (optional) P(E|~H). Use when the source argues "observing E updates belief in H," especially when comparing competing hypotheses against the same observation. +- `gaia author observe --conclusion C [--value ... --error ...]` — raw measurement: ties a Claim, Variable, or Distribution to an observed value. Use for experimental measurements that anchor the graph in data. +- `gaia author compute --conclusion-type T --fn f --given P1,P2,...` — deterministic mapping: a named callable produces the result from the premises. Use when the source presents a closed-form computation whose function is captured by code. +- `gaia author decompose --whole W --parts A,B,... --formula-template and|or|atom` — structural split: composite claim → atomic parts. Use when an aggregate claim is best read as a conjunction (or disjunction) of independently judgeable atoms. +- `gaia author compose --from-file pattern.py` — register a reusable multi-step pattern as a `@compose`-decorated function. Use Pass 4 to refine flat `derive`/`infer` calls into compositions when meaningful intermediate propositions appear. + +Plus the structural-relation verbs (no `--given`; these state a logical constraint between claims): + +- `gaia author equal --a A --b B` — A = B (logically equivalent). +- `gaia author contradict --a A --b B` — NOT (A AND B): both cannot be true, but both can be false. +- `gaia author exclusive --a A --b B` — A XOR B: exactly one must be true (exhaustive + mutually exclusive). + +When in doubt at this pass, reach for `infer` first; Pass 4 will tighten it. + +### Reasoning-chain reconstruction + +How to reconstruct each conclusion's reasoning trace — the detailed +`--rationale`, the premise (`--given`) vs background (`--background`) split, +surfacing implicit premises, and the seven step-writing rules — is **shared +with `gaia-formalize-coarse`**: + +- [`../../_shared/formalize-reasoning-chains.md`](../../_shared/formalize-reasoning-chains.md) + +In this skill's terms: claims used in the derivation go to `--given`; notes +and questions go to `--background`. The `--rationale` is a complete reasoning +chain a domain reader can follow, not a one-sentence stub. + +### Use `@label` and `[@citation]` references in rationales + +In the rationale text, use `@label` to reference knowledge nodes and `[@key]` to cite bibliography entries from `references.json`: + +```python +rationale=( + "Based on the XX framework (@framework_claim), under condition YY (@condition_claim), " + "conclusion ZZ can be derived. The derivation uses the property of WW (@property_note). " + "This follows the approach in [@Dias2020]." +) +``` + +**Knowledge refs** (`@label`): must appear in the verb's `--given` or `--background` list. Verified in Pass 3. + +**Citations** (`[@key]`): must match a key in `references.json`. The strict `[@...]` form raises a compile error if the key is not found. Supports Pandoc group syntax: `[@Bell1964; @CHSH1969]`, `[see @Bell1964, pp. 33-35]`. + +**Rule.** A single `[...]` group must be homogeneous — all knowledge refs or all citations, never mixed. `[@lemma_a; @Bell1964]` is a compile error. + +Citations can also appear in **claim content** to provide traceability: + +```python +tc_measurement = claim( + "The measured superconducting transition temperature is 287.7 K at 267 GPa [@Dias2020].", + title="CSH Tc measurement", +) +``` + +### Do not miss implicit premises + +Surface every implicit premise per the step-writing rules in +[`../../_shared/formalize-reasoning-chains.md`](../../_shared/formalize-reasoning-chains.md): +a fact the derivation uses must be a node in the graph (a `--given` premise or +`--background`), never an unstated assumption. Reference it with `@label` in +the rationale. + +### Model contradictions and exclusives + +After wiring derivation / inference relations, model logical constraints between claims using structural verbs. These claim pairs were identified in Pass 1 reflection; now formalize them. + +**Key distinction — get this right, it matters for BP:** + +- `contradict(a, b)` = NOT (A AND B): both cannot be true, but both **can** be false. +- `exclusive(a, b)` = A XOR B: exactly one must be true (exhaustive + mutually exclusive). + +**When to use `contradict`:** the source argues two claims are incompatible — they cannot both hold. Example: two competing hypotheses about a mechanism, where accepting one rules out the other, but a third option might exist. + +```python +not_both = contradict( + claim("The pairing mechanism is phonon-mediated"), + claim("The pairing mechanism is magnon-mediated"), + rationale="Phonon and magnon mechanisms produce incompatible signatures; the data matches only one.", +) +``` + +**When to use `exclusive`:** exactly two exhaustive, mutually exclusive options. One **must** be true. + +```python +one_of = exclusive( + claim("RFdiffusion outperforms Hallucination on this benchmark"), + claim("Hallucination outperforms or matches RFdiffusion on this benchmark"), + rationale="On the same benchmark with the same metric, one must be better or equal.", +) +``` + +**When to use `equal`:** two formulations express the same proposition. + +```python +same = equal( + claim("Energy is conserved in the closed system."), + claim("dE/dt = 0 in the closed system."), + rationale="Word form and differential form of the same statement.", +) +``` + +**When NOT to use either contradict or exclusive:** two claims that are "in tension" but can both be true. Example: "comprehensive improvement across all areas" and "enzyme scaffolding lacks experimental validation" — both can be true (comprehensive improvement does not require every area to have wet-lab validation). Do not model these as `contradict`. Flag them in the critical analysis as unmodelled tensions instead. + +Contradictions and exclusives are especially valuable in BP because they create strong coupling between nodes — when one side's belief goes up, the other must go down. But a **wrong** contradiction silently distorts all downstream beliefs, so always verify semantics in Pass 5. + +### Pass 2 reflection + +Before moving to Pass 3, verify: + +- **Theory-experiment pairs use `infer`?** Every place the source compares a theoretical prediction against an experimental observation should be connected via `infer(evidence=obs, hypothesis=pred, --p-e-given-h ..., --p-e-given-not-h ...)`. The relationship is explanatory ("does the observation support the prediction?"), not a rigid step-by-step derivation. +- **Multiple observations confirming one law?** If several independent observations all support the same general rule, the conclusion claim (the law) should be a `derive(...)` over those observations — and in Pass 4 you will likely refactor that to a `compose`'d pattern that names the generalisation step explicitly. +- **No missing alternatives?** When the source compares competing hypotheses against one observation, every alternative should be extracted as a claim and either chained as additional `infer` evidence or wired with `exclusive` if the source treats the alternatives as exhaustive. +- **Contradictions modelled?** Every contradictory claim pair identified in Pass 1 should now have a `contradict(...)` (or `exclusive(...)`) operator. Also check: did any new contradictions emerge while writing relations? diff --git a/gaia/_skills/gaia-formalize-fine/references/pass-3-completeness.md b/gaia/_skills/gaia-formalize-fine/references/pass-3-completeness.md new file mode 100644 index 000000000..c1f643389 --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/pass-3-completeness.md @@ -0,0 +1,32 @@ +# Pass 3 — Check completeness + +Load this file after Pass 2 is complete and its compile + check loop passes. +When this pass is done, run the inner loop again and load +`pass-4-strategy-types.md`. + +**Prerequisite:** code from Pass 1-2 has been written and passes `gaia build compile` and `gaia build check`. Pass 3 combines `gaia build check` feedback with manual review. + +### 3a. Check `@label` and `[@citation]` reference consistency + +Review each relation's rationale one by one: + +1. **Re-read the rationale.** Carefully read every sentence. +2. **Check `@label` coverage.** Every `@label` in the rationale must appear in `--given` or `--background`. +3. **Reverse check.** Every node in `--given` / `--background` should be referenced by `@label` in the rationale (otherwise, why is it a premise?). +4. **Check if additional knowledge is needed.** If the rationale mentions an important fact without a corresponding `@label`, go back to Pass 1 to add it. +5. **Check `[@citation]` coverage.** Key claims and reasoning steps from the source should cite the original via `[@key]`. Ensure `references.json` contains all referenced keys. + +### 3b. Check for claims missing reasoning + +Use `gaia build check` output to see if any claim should have reasoning support but lacks a relation: + +- `gaia build check` reports claims that are not the conclusion of any relation (leaf nodes). +- Review each leaf node: is it truly an independent premise? Or should it have an `infer` / `derive` / `compute` / `observe` relation? +- Criterion: if the source provides an argument for this claim (not just a statement), it should have one. + +### 3c. Check for isolated nodes + +- Are there claims that are neither premise / background of any relation nor conclusion of any relation? +- Isolated nodes indicate they do not participate in the reasoning graph — either they should not exist, or a relation referencing them was missed. + +The most common mistake at this step is **assuming certain knowledge does not need explicit references.** In Gaia, if the reasoning process depends on a fact, that fact must be a node in the knowledge graph. diff --git a/gaia/_skills/gaia-formalize-fine/references/pass-4-strategy-types.md b/gaia/_skills/gaia-formalize-fine/references/pass-4-strategy-types.md new file mode 100644 index 000000000..502b88af9 --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/pass-4-strategy-types.md @@ -0,0 +1,117 @@ +# Pass 4 — Refine strategy types + +Load this file after Pass 3 is complete and its compile + check loop passes. +When this pass is done, run the inner loop again and load +`pass-5-structural-integrity.md`. + +Passes 2-3 produce a graph dominated by `infer` (the general fall-back). Pass 4 tightens each relation into the most specific verb that still fits the source. + +### Author-verb reference + +| Verb | Semantics | When to use | Author-side cost | +|----------|-----------|-------------|--------------| +| `derive` | Directed implication: premises jointly support conclusion | Step-by-step derivations, theoretical results read off a formal framework, computation-application chains | `register_prior` against the derive's labelled output (or its warrant helper) for residual uncertainty | +| `infer` | Bayesian update: explicit P(E\|H), optional P(E\|~H) | Theory-vs-experiment fit, single-evidence updates to a hypothesis | `--p-e-given-h` (required), `--p-e-given-not-h` (defaults 0.5) | +| `compute` | Deterministic mapping: callable `fn` produces conclusion from premises | Closed-form computations where the function is in code | `--fn` identifier of a callable; conclusion is the function's output Claim | +| `observe` | Measurement event tying Claim / Variable / Distribution to data | Experimental observations that anchor the graph | `--value` / `--error` for quantity form, or discrete observation against a premise list | +| `compose` | Reusable multi-step pattern: `@compose`-decorated function | Recurring derivation patterns that need a named, registered shape | Author the `pattern.py` and register via `gaia author compose --from-file` | +| `decompose` | Structural split: composite → atomic parts via `and`/`or`/`atom` | Aggregate claim is best read as the conjunction of independently judgeable parts | `--formula-template` or `--formula-expr` | + +Also available as **structural verbs** (modelled in Pass 2 alongside the rest, not in Pass 4): + +| Verb | Semantics | When to use | +|----------|-----------|-------------| +| `contradict(a, b)` | NOT (A AND B) — cannot both be true | Incompatible hypotheses | +| `exclusive(a, b)` | A XOR B — exactly one true | Exhaustive binary choice | +| `equal(a, b)` | A = B — logically equivalent | Two formulations of the same proposition | + +### Decision tree + +``` +For each `infer` relation drafted in Pass 2: + + Is the conclusion a measured datum (or a Variable/Distribution observed at a value)? + YES → observe + NO ↓ + Is the conclusion produced by a closed-form computation in code (named callable f over premises)? + YES → compute + NO ↓ + Does the source present this as a deterministic step-by-step derivation that, given the premises, + is the intended way to reach the conclusion (with at most residual numerical or approximation uncertainty)? + YES → derive (optionally register_prior against the derive's labelled output for warrant uncertainty) + NO ↓ + Is this a Bayesian update where the evidence's likelihood under hypothesis and under its negation + is what carries the inferential weight (e.g. theory predicts X, experiment measured X')? + YES → infer (with explicit --p-e-given-h, and --p-e-given-not-h when known) + NO ↓ + Is the conclusion best read as the conjunction or disjunction of independently judgeable atomic parts? + YES → decompose (--formula-template and|or|atom) + NO ↓ + Does the same multi-step pattern recur across multiple conclusions, and is naming intermediate + propositions worthwhile? + YES → compose (extract into a @compose pattern; per-call the wrapper authors a derive over + the composition's intermediate Claims) + NO → keep infer (with the most informative likelihood you can justify) +``` + +### Recasting legacy reasoning patterns + +The release/0.4 SKILL talked about several named reasoning patterns. Several have clean v0.5 idioms; some do not. Be honest about the gap. + +**Strict mathematical deduction** ("if all premises true, conclusion necessarily true"): use `derive` and omit the warrant prior (or set it very close to 1). `derive` carries the same skeleton (conjunction + directed implication); leaving the warrant near 1 expresses determinism. There is no separate "deduction" verb in v0.5. + +**Soft / probabilistic support** ("premises usually imply the conclusion, with uncertainty"): use `derive` for the relation, then reach for `gaia author register-prior --claim --value ... --justification ...` against the `derive`'s labelled output Claim (or its auto-generated warrant helper) to express the residual uncertainty (numerical methods, approximations, omitted conditions). The engine's `derive(...)` signature does not accept an inline `prior=` — warrant priors are attached via `register_prior`. + +**Theory-experiment comparison ("abduction")**: extract the theoretical prediction and the experimental observation as separate claims (Pass 1), then use `infer(evidence=obs, hypothesis=pred, --p-e-given-h ...)`. When several alternative theories compete, chain `infer` against each candidate hypothesis with its own likelihoods. When the alternatives are mutually exclusive in the paper's framing, add `exclusive(a, b)` for the two-alternative case or `decompose --formula-template or` for three or more (`exclusive` is strictly binary). The abduction *concept* — the prior on the alternative reflects explanatory power for the specific observation, not the alternative's truth in general — survives intact; that deep guide lives in `../../gaia-review/SKILL.md`. + +**Repeated-observation generalisation ("induction")**: there is no single v0.5 verb. The recommended idiom is `derive` over a `compose`'d generalisation step. Specifically: author each observation as its own claim, then either (a) for the simple flat case, `derive(law, given=[obs_a, obs_b, obs_c], rationale=...)`, or (b) when the generalisation involves a named pattern, define a `@compose` function that takes the observations and the law and returns the law's `derive` step, and register it via `gaia author compose --from-file`. The underlying judgement — each observation must be **independent**; if dependent, extract the shared dependency as an explicit claim in Pass 5 — still applies. + +**Process of elimination, proof by cases, mathematical induction, cross-system analogy, extrapolation beyond measured range:** these patterns **have no single-verb v0.5 form**. The recommended idiom for each: + +- *Process of elimination:* `decompose --formula-template or` over the exhaustive option set + `derive(survivor, given=[evidence_eliminating_alt_1, evidence_eliminating_alt_2, ...])`. The disjunctive decomposition guarantees the survivor must be the one true option; the `derive` carries the per-alternative refutation reasoning. (`exclusive(a, b)` is strictly binary — exactly two options — so it only fits the n=2 case; for n≥3 alternatives use `decompose --formula-template or`.) +- *Proof by cases:* one `derive(conclusion, given=[case_k_premise, conclusion_holds_in_case_k])` per case, plus a `decompose --formula-template or` over the case predicates (or `exclusive(a, b)` when there are exactly two cases — `exclusive` is binary only). +- *Mathematical induction:* one `derive` for the base case, one `derive` for the inductive step (`P(n) ⇒ P(n+1)`), and a `derive(for_all_law, given=[base_case, inductive_step])` whose rationale references the inductive schema. **The engine does not enforce the inductive schema** — it treats this as a generic two-premise `derive`. The author must carry the "this is induction over N" framing in the `rationale` text, and the Pass 5 reviewer must verify the base case + step actually warrant the universal. Do not assume the engine guarantees the quantifier reasoning. +- *Analogy* and *extrapolation:* author the structural-similarity / continuity premise as a `claim`, then `derive(target, given=[source, similarity_premise])` or `derive(extrapolated, given=[measured_range_result, continuity_premise])`. The justification quality lives in the premise prior plus the `derive` warrant prior — see `../../gaia-review/SKILL.md`. + +If your source has a derivation that does not map cleanly onto any of these idioms, that is signal: capture the gap in `ANALYSIS.md` under "unmodelled reasoning" so a reviewer can examine it. + +### Strategy variable naming + +Every relation that produces a Claim or warrant **must** be assigned to a named public variable (no `_` prefix). This is required so that the relation appears in `gaia build check --brief` output and can be referenced by `priors.py` and downstream verbs. + +When using `gaia author `, set `--dsl-binding-name` (Python LHS) and `--label` (engine `label=` kwarg) together for any relation that needs to be cited downstream. Use descriptive names like `derive_tc_al`, `compose_workflow`, `infer_theory_vs_exp`. + +### Claim variable naming + +Every Claim **must** be assigned to a named variable (no `_` prefix for claims that need to be visible). Anonymous `claim()` calls or `_`-prefixed claims will not get labels and become invisible in CLI output. The only exception: `__` double-underscore prefix is reserved for compiler-generated helper Claims. + +### When to reach for `compose` + +`compose` is the v0.5 way to capture **complex reasoning with meaningful intermediate steps**. Two triggers: + +1. **3+ premises and no `decompose` fit.** A flat `derive` over 4+ premises suffers the BP multiplicative effect — small uncertainties on each premise compound on the conclusion. If you can name meaningful intermediate propositions (not stubs introduced purely to split the call), refactor into a `@compose` pattern whose intermediate Claims are independently judgeable. +2. **Recurring pattern.** The same shape of derivation appears across multiple conclusions. Register it once via `gaia author compose --from-file` and reuse. + +If decomposition would be forced — no meaningful intermediate proposition exists — 3 premises is acceptable to keep as `derive` or `infer`; 4+ premises must decompose, otherwise BP multiplicative effect will severely suppress belief. + +### Pass 4 reflection + +After refining all relations, verify: + +- **Every theory-vs-experiment `infer` has a meaningful alternative?** When the source compares competing hypotheses, did you extract each alternative and either chain `infer` against it or wire `exclusive` across the candidates? Remember: the prior on the alternative reflects its **explanatory power** for the specific observation, not its truth in general — see `../../gaia-review/SKILL.md` for the deep guide. +- **Each repeated-observation `derive` over independent observations?** For `derive(law, given=[obs_a, obs_b, ...])`, each observation should provide independent evidence. If observations are dependent (shared sample, shared instrument), extract the shared dependency as an explicit claim in Pass 5. +- **`infer` likelihoods anchored?** Every `infer` call has `--p-e-given-h` from the source. If `--p-e-given-not-h` is left at 0.5, it is a fall-back — when the source's framing supplies a competing-explanation likelihood, set it explicitly. + +### Post-refinement check + +After refining all relations, check the **verb distribution**: + +- If `derive` accounts for more than 70% of relations, review whether some should be `infer` (theory-vs-experiment fit) or `compose`'d (multi-step generalisation). +- Papers with extensive experimental validation typically have many `infer` calls. +- Discussion / conclusion sections that synthesise multiple results often have a `compose`'d generalisation step. + +Also check **reasoning chain depth** (hops from leaf to exported conclusion): + +- Maximum recommended depth: **3 hops**. +- If a derived conclusion has belief < 0.4, the chain is likely too deep. +- Fix by flattening: make intermediate claims into leaf premises, or restructure into wider (more premises per relation) rather than deeper (more relations in series). diff --git a/gaia/_skills/gaia-formalize-fine/references/pass-5-structural-integrity.md b/gaia/_skills/gaia-formalize-fine/references/pass-5-structural-integrity.md new file mode 100644 index 000000000..7d885076c --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/pass-5-structural-integrity.md @@ -0,0 +1,60 @@ +# Pass 5 — Verify structural integrity + +Load this file after Pass 4 is complete and its compile + check loop passes. +When this pass is done, run the inner loop again and load `pass-6-polish.md`. + +**Prerequisite:** Pass 4 is complete — all relation types are finalised. This pass checks that the factor graph correctly represents the source's reasoning. It must happen after Pass 4 because verb refinement (especially `compose`'d patterns) changes the graph topology. + +**Background.** Gaia uses Junction Tree (exact inference). There is no algorithmic double-counting — given any factor graph, JT computes correct posteriors. All issues in this pass are about whether the **model** correctly represents reality: each factor (relation / structural verb) should represent a genuinely independent constraint, and each structural verb's logical semantics should match the actual relationship. + +### 5a. Verify structural-verb semantics + +Check structural verbs first — if the graph's hard constraints are wrong, everything downstream is wrong too. + +Review every `contradict(...)`, `exclusive(...)`, and `equal(...)` call: + +**`contradict(a, b)` = NOT (A AND B)**: both cannot be true, but both **can** be false. + +```python +# WRONG: these can both be true — no contradiction! +contradict( + claim("RFdiffusion succeeds at designing large proteins"), + claim("Hallucination fails at designing large proteins"), +) + +# CORRECT: these cannot both be true +contradict( + claim("RFdiffusion is inferior to Hallucination on this task"), + claim("RFdiffusion outperforms Hallucination on this task"), +) +``` + +**`exclusive(a, b)` = A XOR B**: exactly one must be true. Stronger than `contradict`. + +**Three-question checklist for each structural verb call:** +1. Can both claims be true simultaneously? If yes → not a `contradict`, remove it. +2. Can both claims be false simultaneously? If no → should be `exclusive` (XOR), not `contradict` (NAND). +3. Is this just "in tension" rather than logically exclusive? Informal tension should NOT be modelled as `contradict` — flag in critical analysis instead. + +### 5b. Eliminate double counting + +Every factor in the factor graph must encode a **genuinely independent +constraint**; the same evidence entering a conclusion twice inflates belief — +not because Junction Tree miscalculates, but because the model is wrong. The +double-counting patterns (redundant relations, hidden evidence in rationale +text, unmodelled shared dependencies, `equal` plus separate relations), the +shared-factor extraction rule, the modelling-choice table, and the check +procedure are **shared with `gaia-formalize-coarse`**: + +- [`../../_shared/formalize-independence.md`](../../_shared/formalize-independence.md) + +All four patterns apply to this skill — it emits the full relation-verb set, +including `equal`. One Pass-5-specific addition to the shared check: for every +`infer` call, confirm `--p-e-given-h` is a source-supported value and +`--p-e-given-not-h` is the right alternative-likelihood (not a stand-in 0.5 +when the source actually argued an alternative). Run the shared file's check +procedure over every claim with 2+ incoming relations before 5c. + +### 5c. Re-compile and verify + +After any structural changes in Pass 5, run `gaia build compile` + `gaia build check` + `gaia run infer` and compare beliefs to before. A significant belief drop after removing a relation suggests the previous value was inflated by double counting. diff --git a/gaia/_skills/gaia-formalize-fine/references/pass-6-polish.md b/gaia/_skills/gaia-formalize-fine/references/pass-6-polish.md new file mode 100644 index 000000000..7e9d8889e --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/pass-6-polish.md @@ -0,0 +1,71 @@ +# Pass 6 — Polish for standalone readability + +Load this file after Pass 5 is complete and its compile + check loop passes. +When this pass is done, run the inner loop a final time and load +`priors-analysis-render.md`. + +**Prerequisite:** the knowledge graph is structurally correct (Pass 5 complete). Pass 6 ensures that every claim, rationale, and metadata entry is independently understandable without access to the original source. + +### 6a. Claim self-containedness + +Review every claim for standalone readability: + +**Symbols must be self-explanatory.** +- Every mathematical symbol must have a brief explanation on its first appearance in that claim. +- Example: do not write "$\alpha \ll 1$"; write "the parameter $\alpha$ (ratio of XX to YY) is much less than 1". +- The physical meaning of subscripts / superscripts must be explicit. + +**Abbreviations must be expanded.** +- Every abbreviation must be expanded on its first appearance in that claim. +- Example: do not write "XXX computes $\lambda$"; write "the such-and-such method (XXX) computes the coupling constant $\lambda$". +- Even if an abbreviation has been expanded in another claim, each claim is independent and must expand it again. + +**No comparative assertions without reference.** +- Do not write "significantly larger than X" — the reader does not know what is being compared. +- Do not write "nearly exact agreement" — the reader does not know what it agrees with. +- Numerical comparisons must provide both values. + +**Sufficient detail.** +- Can a reader understand what this claim says by reading only this one claim? +- Are conditions and applicable ranges clear? +- Do numerical values include units and error bars? + +### 6b. Data formatting + +- Tabular data should use markdown tables in claim content. +- Key numerical values from figures must be transcribed into the claim text (not just referenced). +- Trends described in prose should include specific data points. + +### 6c. Rationale standalone readability + +Review every relation's `rationale` text: + +- The rationale should be a complete reasoning chain, not "see Section 3 of the paper." +- Specific numbers, method names, and conditions should be stated, not implied. +- Every `@label` reference should have enough surrounding context that a reader unfamiliar with the label can follow the argument. + +### 6d. Figure and table references + +Add `metadata={"figure": "...", "caption": "..."}` to every claim whose content comes from a specific figure or table: + +1. **Coverage.** Check each module against the source for missing references. +2. **Path validity.** Verify each file path exists in `artifacts/`. +3. **Caption accuracy.** Copy the figure caption from the source (abbreviated OK, but figure number and key content must be correct). +4. **Relation metadata.** Relations whose `rationale` references figure data should also carry `metadata`. + +### 6e. Complete citation metadata + +During Passes 1-4, `references.json` entries were kept minimal (key + type + title). Now fill in complete metadata for all cited references: + +- **author** — full author list (`[{"family": "...", "given": "..."}]`). +- **issued** — publication date (`{"date-parts": [[2020]]}`). +- **container-title** — journal / conference name. +- **volume**, **page**, **DOI** — where applicable. + +Verify: every `[@key]` used in claims and rationales has a corresponding entry in `references.json`. Run `gaia build compile .` to catch any missing keys (strict `[@key]` form raises a compile error if the key is not found). + +### 6f. Format consistency + +- Metadata format should be consistent across all claims (same key names, same path conventions). +- Titles should follow a consistent naming style. +- Cross-module import patterns should be uniform. diff --git a/gaia/_skills/gaia-formalize-fine/references/priors-analysis-render.md b/gaia/_skills/gaia-formalize-fine/references/priors-analysis-render.md new file mode 100644 index 000000000..3911257fc --- /dev/null +++ b/gaia/_skills/gaia-formalize-fine/references/priors-analysis-render.md @@ -0,0 +1,120 @@ +# Prior assignment, inference, analysis, and rendering + +Load this file after Pass 6 is complete. This is the tail of the workflow: +assign leaf priors, run inference, interpret the results, produce the +`ANALYSIS.md` deliverable, and hand off to rendering. + +## Prior-assignment tail + +After Pass 6, you have a structurally complete graph and a passing `gaia build check`. Now assign priors and run inference. + +### Write `priors.py` + +`priors.py` assigns priors to leaf claims. Warrant priors on `derive` (and `infer` / `compute` where relevant) are set by `gaia author register-prior --claim --value ... --justification ...` against the verb's labelled output Claim (or its auto-generated warrant helper). The engine's verb signatures do not accept an inline `prior=` kwarg — `register_prior` is the only path. + +**Before writing `priors.py`, run `gaia build check --hole .`** to see exactly which independent claims need priors, along with their content and current status. Use this as your checklist — address each hole, then re-run `gaia build check --hole .` to confirm "All independent claims have priors assigned." + +The CLI shortcut is: + +```bash +gaia author register-prior \ + --claim my_leaf_claim \ + --value 0.85 \ + --justification "Well-established by [@Smith2020] in the same regime." \ + --file priors.py +``` + +That command appends a `register_prior(...)` statement to `priors.py` and auto-injects the import if the target file is a sibling of `__init__.py`. + +**Do NOT set priors for derived claims.** The inference engine automatically assigns uninformative priors (0.5) to derived claims. Their beliefs are determined entirely by BP propagation from leaf premises. Setting an explicit prior on a derived claim double-counts evidence: the reviewer's judgement and the reasoning chain both reflect the same underlying data. Only set priors for independent (leaf) claims that are not the conclusion of any relation. + +**The π(Alt) discipline (`infer` alternatives) deserves special attention.** In the abductive pattern (theory-vs-experiment `infer`), the prior on the alternative reflects its **explanatory power for the specific observation**, not whether the alternative's computation is correct in general. The most common and consequential mistake in prior assignment is setting π(Alt) based on "the alternative's calculation is right," rather than "the alternative explains the observation." The deep guide — worked examples, rule-of-thumb checks, the explanatory-power-vs-correctness distinction — lives in `../../gaia-review/SKILL.md`. Read it before writing the prior on any abductive alternative. + +The full prior-assignment guide (evidence-level → prior-range tables, warrant-prior ranges, iteration loop) also lives in `../../gaia-review/SKILL.md`. This skill points at it; do not duplicate the tables here. + +### Run inference + +```bash +gaia run infer # writes .gaia/beliefs.json +gaia run infer --depth 1 # joint cross-package inference (direct deps) +gaia run infer --depth -1 # joint cross-package inference (all transitive deps) +``` + +### Interpret BP results + +Read the table in `../../_shared/bp-interpretation.md`. Do not duplicate the interpretation table here — that reference is the single canonical copy. The shape of the loop: + +``` +gaia run infer → .gaia/beliefs.json → interpret per ../../_shared/bp-interpretation.md + ↓ + structural issues → back to Pass 1-5 (revise graph) + prior issues → revise priors.py (revisit ../../gaia-review/SKILL.md guide) + otherwise → proceed to ANALYSIS.md +``` + +If results are clearly wrong (a well-supported conclusion has belief < 0.3, or a contradict relation does not pick a side), go back and check: + +1. **Structural issue?** (→ revisit Pass 1-5.) Missing premises, wrong relation verb, missing alternative for an `infer`, evidence double-counting. +2. **Parameter issue?** (→ revisit `priors.py`.) Priors too low / high, `--p-e-given-h` miscalibrated, π(Alt) reflecting computational correctness instead of explanatory power. + +## Generate the GitHub presentation + +After the prior-assignment tail produces beliefs you trust, hand off to `../../gaia-publish/SKILL.md`: + +```bash +gaia run render --target github # .github-output/ README + narrative outline +gaia run render --target docs # per-module Mermaid graphs in docs/detailed-reasoning.md +gaia run render --target obsidian # gaia-wiki/ skeleton (hands off to ../../gaia-obsidian-wiki/SKILL.md) +``` + +`../../gaia-publish/SKILL.md` carries the README narrative discipline (per-conclusion evidence assessment, Weak Points framed around internal nodes, Evidence Gaps by theme). `../../gaia-obsidian-wiki/SKILL.md` carries the rich-vault discipline (claim pages with full derivations, section pages as narrative chapters). + +## `ANALYSIS.md` — critical analysis deliverable + +After BP results stabilise, produce a **critical analysis** of the source. This is the analytical payoff of formalization — by building the knowledge graph, you now understand the argument's structure well enough to identify its strengths and weaknesses. + +`ANALYSIS.md` lives in the package root and is a **required deliverable** — do not skip it. The required sections: + +### 1. Package statistics + +Knowledge graph counts (claims by role, relations by verb, structural-verb counts), verb-type distribution, claim role classification, figure reference coverage, BP result summary. + +### 2. Summary + +One paragraph on the argument's overall structure and strength. + +### 3. Weak points (table) + +Internal nodes with low belief. **Internal nodes, not exported conclusions** — exported conclusions go in the README's Reasoning Structure section (`../../gaia-publish/SKILL.md`); `ANALYSIS.md` Weak Points is for the load-bearing intermediate nodes whose fragility threatens the whole chain. + +Columns: claim, belief, issue. Include all derived claims with belief < 0.8 and any `infer`-alternative claims with belief > 0.25. + +Vulnerability signals to capture in the "issue" column: + +| Signal | What it means | +|--------|---------------| +| Derived conclusion with low belief (< 0.5) | Weak premise support or fragile reasoning chain | +| Long reasoning chain (4+ hops from leaf to conclusion) | Multiplicative effect — small uncertainties compound | +| `infer` alternative π(Alt) ≈ π(H) | Alternative is equally plausible — evidence does not distinguish | +| Leaf claim with low prior and many downstream dependents | Single weak foundation supporting many conclusions | +| `derive` warrant with very low prior (< 0.3) | Reviewer flagged this step as unreliable | +| Claim marked as `note` that could be questioned | Hidden assumption not subject to BP updating | + +### 4. Evidence gaps (tables, grouped by theme) + +Group by theme: **experimental**, **computational**, **theoretical**. Within each, identify where additional evidence would most strengthen the argument. For each gap: which conclusions improve if filled. Prioritise by impact. + +- **Unsupported leaf claims:** claims with no reasoning support that the source takes as given — what evidence could back them up? +- **Weak `infer` alternatives:** where the alternative nearly matches the hypothesis in explanatory power — what new observation could break the tie? +- **Missing comparisons:** theoretical predictions without experimental validation — what experiment could test them? +- **Single-observation generalisations:** laws supported by only one observation — what additional observations would strengthen the `derive`? + +### 5. Contradictions + +(a) Explicit `contradict(...)` relations modelled and how BP resolved them (which side won). (b) Internal tensions in the source that were not modelled as formal contradictions but are worth flagging. + +### 6. Confidence assessment + +Tier the exported claims into confidence levels (very high / high / moderate / tentative) with belief ranges. + +The critical analysis transforms a qualitative reading of the source into a quantitative structural assessment. Every knowledge package should ship with one.