[codex] Normalize deduction priors under MaxEnt#654
Draft
kunyuan wants to merge 273 commits into
Draft
Conversation
[codex] Unify context knowledge as notes
* Add propositional operators to Gaia Lang * Add propositional logic analysis backend * Fix propositional helper priors and formal logic expansion --------- Co-authored-by: kunchen <chenkun0228@gmail.com>
Resolves the scope ambiguity between the two idea-stage foundation drafts (scientific formal language vs Jaynesian backend) by picking a concrete north star and drawing the kernel boundary explicitly. Key decisions captured: - Three-layer probability semantics (belief / noise / likelihood), with naming discipline to keep the layers from conflating - Kernel owns Claim / Action / Review / Context / Evidence schema / MeasurementRecord / CallableRef / PriorSpec; unit algebra and distribution computation delegate to Pint / scipy adapters - Independence becomes a review-layer concern (IndependenceDeclaration as a relation-level ReviewTarget); EvidenceMetadata.independence_group retired - EvidenceMetadata class dissolved into InferStrategy via pydantic discriminated union; bayes_factor / likelihood_ratio persist only the ratio, not a fabricated CPT - Strategy.background (list of Claim IDs) replaces free-text assumptions; Derive / Compute / Infer all carry it - Setting (v5 Knowledge type) and v5 strategies deprecated from v0.5 - No first-class Z3 / PPL / Model / Experiment / Dataset in v0.x kernel; explicit extension points named for v1.x+ Supersedes both drafts under docs/ideas/foundation-specs/. Partially supersedes the release specs under docs/ideas/gaia-upgrade-specs/ that need rewriting against the new foundation. Does not propose a release plan — that belongs in a separate document and must be rewritten against this foundation. Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
Clarify what "Gaia has a unit system" means:
- Kernel owns Quantity as a structural type (value + unit)
- Unit semantics (registry, conversion, dimensional analysis)
belongs exclusively to the Pint adapter
- Claim identity and context_id hash the literal {value, unit}
bytes; no unit canonicalisation at hash time
Rationale: canonicalisation at hash time would leak floating-
point rounding, offset-unit affine transforms, ratio-unit
ambiguity, and Pint-version-dependent aliasing into Claim
identity, breaking context reproducibility across library
versions and architectures.
Unit-equivalence detection becomes an audit-level concern via
the UnitAdapter (soft warnings in gaia audit, dual rendering
in gaia explain), never an identity-level one.
§16 gains a ninth IR change item recording the literal-hash
invariant.
Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
… a unit system
Previous §4.5 wording ("Gaia has a Quantity type") could be
misread as Gaia shipping its own unit system. Strengthen the
framing:
- Open with the plain statement: Gaia does NOT implement a
unit system
- Name Pint explicitly as the authoritative unit library
- Reframe the kernel Quantity schema as a 2-field pydantic
carrier whose sole job is IR serialisation and context_id
hash — no methods, no arithmetic, no conversion
- Add explanatory block on why Pint's native Quantity is not
used directly (hash stability, core-dep discipline, testing
hygiene)
- Analogy: kernel Quantity is to Pint what a pydantic model
is to JSON — a contract surface, not a reimplementation
Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
…arrier
Units are foundational to scientific claims. Treating Pint as an
optional adapter was friction without benefit: nearly every real
Gaia package needs units, and a shared Pint UnitRegistry across
packages gives consistency that individual Pint() calls cannot.
Architecture update:
- Introduce gaia.unit as a core module of gaia-lang
- Thin Pint facade (~30 lines of real code)
- Owns a shared UnitRegistry singleton with Gaia-configured
conventions (domain units, default preferred system, contexts)
- Re-exports pint.Quantity as the user-facing runtime type
- Provides q() helper and to_literal/from_literal bridges
- Rename kernel IR carrier: Quantity -> QuantityLiteral
- 2-field {value: float, unit: str} pydantic schema, unchanged
- Name change eliminates collision with gaia.unit.Quantity
(Pint's Quantity); kernel reads QuantityLiteral only, user
code reads gaia.unit.Quantity only
- Pint moves from optional extras to core dependency of gaia-lang
- Kernel code itself still does not import Pint; dependency is
scoped to gaia.unit
- Pint transitive closure is small (~500 KB, no numpy)
Spec edits touch §3.2 (adapter table notes Pint exception),
§3.3 (rationale updated), §4.5 (full rewrite showing the
three-piece design: gaia.unit runtime / QuantityLiteral kernel /
adapter boundary), §5 (inventory adds QuantityLiteral, notes
gaia.unit.Quantity lives outside kernel), §14 (ecosystem rule
records the Pint exception), §16 (IR change list adds items 9
and 10 covering QuantityLiteral and gaia.unit).
Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
…onSpec
Extend the gaia.unit pattern to statistics. Same facade idea,
with an intentional asymmetry in dep policy because scipy is
100x heavier than Pint and user interaction pattern differs.
Additions:
- gaia.stats as a core module of gaia-lang
- Named constructors: Normal, Lognormal, StudentT, Cauchy,
Binomial, Poisson, Exponential, Beta (8 built-ins)
- Shared distribution registry (param schemas, dispatch tags)
- from_callable(...) helper producing DistributionSpec with a
CallableRef — the user-extensibility path
- Does NOT import scipy at load time
- gaia-lang[stats] optional extras pulling scipy
- gaia/adapters/stats/scipy_adapter.py dispatches
DistributionSpec by kind to scipy.stats, or resolves
CallableRef for kind="custom"
- Lazy-imported inside evidence adapters
Renames:
- Kernel schema ErrorModelSpec → DistributionSpec
- Generalises to any distribution use (noise, future prior
shapes, future predictive, etc.), not only measurement error
- Adds kind-vs-callable-ref validator: built-in kind disallows
callable_ref; kind="custom" requires it
User-extensibility (normative): authors add custom distributions
via gaia.stats.from_callable(...), producing DistributionSpec
with kind="custom" + CallableRef. No kernel extension required;
existing CallableRef machinery handles naming/versioning/source
hashing/cross-package import review.
Why scipy stays optional (unlike Pint for gaia.unit):
- Weight: scipy + numpy ≈ 70 MB vs Pint ≈ 500 KB
- Usage: users construct specs, adapters evaluate. User code
rarely needs logpdf/sampling directly.
- Testing: kernel and gaia.stats spec tests run without scipy
Spec edits: §1.x (kernel object list), §3.2 (adapter table
splits spec vs compute), §4.4 (example uses gaia.stats.Normal),
§4.6 (new section mirroring §4.5), §5 (inventory adds
DistributionSpec, notes gaia.stats constructors live outside
kernel), §16 (IR items 5/9 reference DistributionSpec, new
items 11-13 cover rename + gaia.stats + scipy adapter extras).
Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
Physical constants recur across scientific claims (c, h, k_B, G, N_A, particle masses, etc.). Introduce gaia.constants as a thin curated re-export of Pint's built-in constant registry. Design: - Core module, lives in gaia/constants.py - No new schema: constants are named gaia.unit.Quantity instances - No new dependency: Pint is already core (§4.5) - Double naming — short (c) and long (speed_of_light) — both resolve to the same value; author picks per context - CODATA version tracks Pint's registry; Pint upgrades propagate values automatically - User-extensibility: authors add their own constants at package level using gaia.unit.q(...); no Gaia mechanism required. gaia.constants is a Gaia-blessed default set, not an enumeration ceiling. Spec edits: - §3.2 adapter table: new row for Physical constants - §4.5 "split" table: row for Physical constants now references gaia.constants, not scipy.constants - New §4.7 section with schema-free design summary - §16 IR changes: new item 14 records the module addition Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
Rewrite §3.1 "In the kernel" and §5 "Kernel object inventory" to reflect the U1 decision: Strategy and Operator are subtypes of Knowledge, not parallel hierarchies. Unification applies at both Gaia Lang (runtime) and Gaia IR (serialisation) layers. Structural changes: - §3.1 lists Knowledge as the single base type with Claim / Note / Question / Strategy / Operator as subtypes. Belief lives only on Claim; review_status is optional on any Knowledge. - §3.1 acknowledges StrategyParamRecord as sidecar for parameter updates (per priors.py pattern) — not inlined into Strategy. - §5 reorganises the kernel inventory into (a) Knowledge hierarchy, (b) sidecar records (PriorRecord, StrategyParamRecord), (c) Review / Context / Measurement / Callable / Prior schemas. - §5 adds a new §5.x "Lang ↔ IR mapping" table clarifying the two-layer differences (object refs vs QID strings, etc.). - §8 drops references to bayes_factor() / likelihood_ratio() DSL helpers (which §11 will remove entirely in Segment 3). - §15.2.1 (new) records U1 runtime refactor as an independent, dedicated PR — v0.5 HEAD's gaia/lang/runtime/action.py explicitly has Action *parallel to* Knowledge; U1 reverses that and the refactor touches enough surface that it must not be bundled with a functional PR. Scope bounded: this segment does not yet address R4 review model, CallableRef=provenance invariant, publish-time contract, §11 Infer simplification, or §16 audit against v0.5 code. Those land in Segments 2-4. Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
…ract
Second of four planned segments. Expands §7 with the cross-package
review authority model and §14 with the publish-time contract.
§7 Independence — aligned with U1 and extended to R4:
- 7.2 schema: ReviewTarget keyed by knowledge_id (QID) under U1;
IndependenceDeclaration.factors now holds knowledge_ids (was
action_labels). Single target-identity scheme covers claims,
strategies, operators uniformly.
- 7.5 (new) Cross-package review authority — R4:
* Normative effective-status rule: foreign K is "active" iff
upstream accepted AND (downstream accepted OR TrustDelegation
applies). Silence is not consent.
* Upstream "rejected" cannot be bypassed downstream (hard
scientific-integrity constraint).
* TrustDelegation as a reviewable bulk-trust target, version-
pinned (no ranges, no author-wide), with scope narrowing
(all_knowledge / exclude_compute / claims_only).
* Rationale records why this beats pure upstream-authority (R1)
and pure independent-review (R2).
§14 Ecosystem integration — split into three subsections:
- 14.1 What the official registry already enforces: accurate
accounting of current gaia-registry CI (ir_hash recompile
verification, tag/SHA pinning, dependency closure, namespace
check, UUID uniqueness) and the artefacts it ships (Package.toml,
Versions.toml, Deps.toml, beliefs.json per release). Avoids the
"we will build X" framing for mechanisms that already exist.
- 14.2 Publish-time contract (foundation-level): four normative
invariants — upstream ships results (α-hard), registry CI
verifies IR-result consistency (extension work item, §16),
downstream consumes without re-executing CallableRefs regardless
of --depth, stale upstream is refused with no escape hatch.
- 14.3 The replication path — gaia recompute: explicit opt-in,
point-by-point, R4-gated. Keeps actual cross-package code
execution out of any default flow. Details (§4.8 invariant,
full CLI spec) come in Segment 3.
Scope bounded: this segment does not yet touch §4.8 CallableRef
invariant, §11 Infer simplification, §16 IR change list audit.
Those land in Segments 3-4.
Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
…inline-only reality Segments 1 and 2 treated StrategyParamRecord and PriorRecord as live foundation-level sidecar carriers. That was wrong. Verified against origin/v0.5: - gaia/cli/_reviews.py header: DEPRECATED since 0.4.2 - Replacement priors.py (gaia/cli/_packages.py:apply_package_priors) is a DSL-layer convenience that writes priors into Knowledge.metadata["prior"] at compile time — inline, not a sidecar record at IR level. - Infer CPT is inlined at compile time onto IrStrategy.conditional_probabilities from action.p_e_given_h / action.p_e_given_not_h. - gaia/ir/validator.py:validate_parameterization, which enforced StrategyParamRecord presence for parameterized strategies, is never called in the active code path (grep finds no callers). It is dead code from the sidecar era. Corrections in this commit: - §3.1: remove StrategyParamRecord bullet; add a note explaining the v0.5 inline-only parameter model (priors via metadata injection, CPTs inline on IrStrategy). Explicitly flag the sidecar types as deprecated. - §5: replace the "Sidecar records" subsection with "Inline parameters (no sidecar records)", showing the actual IR shape (Knowledge.metadata["prior"], IrStrategy.conditional_probabilities) and listing the deprecated types only to note their deprecation. - §14.2 Invariant 3: fix the joint-graph example to reference inline IrStrategy.conditional_probabilities and foreign Knowledge.metadata["prior"], not StrategyParamRecord. - §15.2: drop "StrategyParamRecord formalisation" from the additive-changes list; add "inline-only parameter model" to the clarifying-changes list. No policy change — only documentation correction. The foundation spec now accurately describes how v0.5 stores parameters. Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
…Infer rewrite Third of four planned segments. Introduces the CallableRef-as- provenance normative invariant and rewrites §11 to match the CPT-pair-only decision. §4.8 (new) — `CallableRef` is provenance, not an execution pointer: - Normative invariant stated plainly: every CallableRef is a provenance record, not a routine-execution pointer. The expected execution happens in the declaring package at the author's time; the result is baked into IR / beliefs.json. Downstream never invokes upstream CallableRefs at any depth. - Walks the three sites CallableRef appears (ComputeStrategy, DistributionSpec custom kind, adapter hooks) and shows each bakes its result at author's time. - States that gaia recompute is the sole operation that resolves any CallableRef; everything else reads baked values. - Consequences: no cross-package code safety concern in default flows; --depth N is not re-execution; purity declarations are not load-bearing; upstream library version drift cannot change downstream beliefs. §11 rewritten for CPT-pair-only evidence: - 11.1 Schema: DSL requires both p_e_given_h and p_e_given_not_h as keyword args (no defaults, Cromwell-clamped). IR side keeps the existing v0.5 IrStrategy shape — conditional_probabilities stores [P(E|¬H), P(E|H)] inline. Adds well-known metadata keys (evidence.source_id / data_id / data_hash / rationale + evidence_computation). - 11.2 Why forced CPT: scientific-rigour argument (committing to absolute values forces modelling work) + BP-correctness argument (when E isn't pinned, BP propagation depends on absolute values, not just ratio). Arbitrary LR→CPT normalisations produce unrecognised results. - 11.3 Literature BF citations: example showing the author does their own anchoring and records the derivation in rationale. No kernel helper does this conversion. - 11.4 Adapter-computed evidence: gaussian_measurement_evidence example showing the adapter computes both values at author's time and writes them to conditional_probabilities. Per §4.8 and §4.6, scipy runs only in author's context. - 11.5 EvidenceComputationRecord: adapter_ref + inputs, for recompute replay. Provenance-only per §4.8. - 11.6 Provenance field set: source_id / data_id / data_hash / rationale are kernel-consumed; instrument_id / cohort_id / model_id etc. go to free metadata; assumptions removed entirely (they're Claims referenced via background). - 11.7 Retired helpers: likelihood_ratio() and bayes_factor() are explicitly not in the kernel. Tools that accept LR/BF must compile down to the CPT pair via author anchoring. §4 three-layer table and concrete example updated to reflect the CPT-pair-only reality (no more InferStrategy.likelihood_ratio references). Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
…points refresh
Final segment of the four-part update. Walks §16 item by item
and tags each against what actually exists in v0.5 HEAD.
§16 rewrite:
- Introduce a four-value status tag per item:
[implemented] — already in v0.5; spec just names it
[to-refactor] — partial v0.5 support; needs work
[new] — nothing in v0.5; fresh schema/module
[retracted] — earlier drafts listed it but v0.5 never had
the precondition; foundation drops the ask
- Regroup into §16.1–§16.6 (kernel schema / U1 / review-R4 /
gaia.unit-stats-constants / CLI-registry / deprecations).
Key audit findings baked into §16:
- background: list[str] on IrStrategy is [implemented] (live in
v0.5 gaia/ir/strategy.py).
- Knowledge.type == "setting" is [to-refactor] (still live in
v0.5 setting() DSL).
- EvidenceMetadata dissolution, independence_group removal, and
assumptions removal are all [retracted] — those structures
never existed in v0.5 HEAD; they were proposed by GPT Pro's
v0.6 idea draft. Foundation's final §11 is CPT-pair inline,
which matches v0.5 IrStrategy.conditional_probabilities.
- ReviewManifest already keys by target_id with target_kind
spanning strategy/operator/knowledge (v0.5 gaia/ir/review.py);
under U1 that collapses to knowledge-only, but the underlying
schema is [to-refactor], not [new].
- Registry ir_hash recompile verification and beliefs.json
shipping are [implemented] in the existing gaia-registry CI
and gaia register CLI. belief_state.json schema extension
(context_id / diagnostics / generated_at / belief_state_hash)
and the registry CI extension to re-run infer are [new].
- IndependenceDeclaration, TrustDelegation, R4 effective-status
resolver, gaia recompute CLI — all [new].
- U1 runtime refactor is [to-refactor] with an explicit
requirement (§15.2.1) that it ship as a dedicated PR.
- Legacy sidecar modules (_reviews.py, validate_parameterization)
are already [implemented]-deprecated in v0.5; foundation
simply confirms they are not part of the kernel and does not
require removal.
§17 expanded:
- Add "multi-source parameterisation" as a parked design point —
explicit note that this is not a continuation of the
deprecated PriorRecord/StrategyParamRecord sidecar.
- Add TrustDelegation revocation (parked until registry
attestation story lands).
- Add unit registry versioning in context_id and physical-
constants versioning — both parked extensions that would
mirror the CallableRef name+version+hash pattern.
Co-Authored-By: Claude Opus 4 (1M context) <noreply@anthropic.com>
Follow-up to PR #628's compiler extension hook. Addresses three concerns (M1 / M2 / M3 from the review thread) plus one structural improvement and one round of post-merge-review feedback. M1 — Auto-discover first-party extensions before compile. `compile_package_artifact` calls `discover_and_register_extensions()` at the top, which invokes each first-party extension's `register_<name>_lowerer` helper via a small `(module_path, callable_name)` table in `extensions.py`. Callers no longer need to ensure `gaia.engine.bayes` is imported before compile; the previous failure mode (`ValueError: Unsupported action type: PredictiveModel` from `_compile_action`) now only surfaces when discovery is explicitly disabled. The discovery table lives in `extensions.py`, not `compile.py`, so the host -/-> extension contract stays intact. M2 — Duplicate-guard on `register_action_lowerer`. Re-registering the same name raises `ValueError` unless `override=True` is passed. Bayes self-registration is identity-aware idempotent: returns early only when the existing "bayes" entry uses the official `_is_bayes_action` / `_lower_bayes_actions` pair via `is` comparison; any other callable pair under that name raises so accidental shadowing surfaces loudly (addresses the [P2] review thread on PR #633 — a name-only check would silently mask exactly the scenario M2 exists to catch, including the worst case where a foreign "bayes" registration with `handles=lambda _: True` + no-op `lower` produces silently-incomplete Bayes IR). M3 — Lock in the contract with tests. Nine tests covering: discovery happy-path, auto-discovery after registry clear, loud failure when registry empty and discovery disabled, duplicate rejection, override-replace, Bayes idempotency, conflicting-registration rejection, end-to-end Bayes compile through the registry. Bonus: AST-walk host/extension contract test. The previous `test_lang_compiler_has_no_direct_bayes_import_or_hook` guarded the spec PR #617 §6 host ⊥ extension dependency direction by searching `compile.py`'s source for the literal string `"gaia.engine.bayes"`. Replaced with an `ast.walk` over `ast.Import` / `ast.ImportFrom` nodes filtered by an `extension_namespaces` tuple. Docstrings and comments mentioning bayes no longer false-positive; the namespace list is the single place to extend when the second extension lands. A docstring note flags the migration to `import-linter` at that point so the contract (including extension ⊥ extension) can be expressed declaratively. Files: - `gaia/engine/lang/compiler/extensions.py` — new `discover_and_register_extensions`, `_FIRST_PARTY_EXTENSIONS` table, `override=` param + duplicate guard on `register_action_lowerer` - `gaia/engine/lang/compiler/compile.py` — call discovery at the top of `compile_package_artifact` - `gaia/engine/bayes/compiler/__init__.py` — identity-aware idempotent `register_bayes_lowerer` - `tests/gaia/lang/compiler/test_extension_lowering.py` — six new tests, AST-walk contract test, helper `_build_minimal_bayes_package` No production behaviour change: `gaia build / run` on Bayes packages continues to compile to the same IR. The new behavioural guarantee is "compile no longer cares whether the user imported bayes first" and "name collisions on registered lowerers surface loudly."
* docs: design formula graph ir foundation * docs: address formula graph design review * docs: add formula graph implementation plan * feat(ir): add formula graph models * fix(ir): validate formula node kind consistency * feat(lang): emit formula graphs during lowering * fix(lang): preserve scoped formula variables * feat(ir): validate formula graph structure * fix(lang): canonicalize formula helper identities * fix(ir): harden formula graph validation * docs: mark formula graph implementation plan progress * fix(ir): satisfy formula graph type checks * fix(ir): validate malformed formula graph nodes * fix(test): refresh formula graph baselines --------- Co-authored-by: kunchen <chenkun0228@gmail.com>
8 P0 corrections across user-facing and foundation docs: - for-users/cli-commands.md: invert "Old flat verbs" wording (was claiming current grouped verbs were tombstoned) - foundations/review/review-pipeline.md: replace 6+ tombstoned source paths (gaia/inquiry/*, gaia/trace/*, gaia/cli/commands/_review_manifest.py) with their canonical engine homes - foundations/cli/workflow.md: complete the gaia build check option table (--warrants / --blind / --inquiry / --gate) - foundations/bp/belief-state.md: rename diagnostics fields to iterations_run / max_change_at_stop to match dataclasses - foundations/gaia-lang/knowledge-and-reasoning.md: fix legacy support([P], C) -> infer mapping (positional polarity was reversed) - foundations/bp/formal-strategy-lowering.md: rewrite leftover editing TODO into positive cross-reference - for-users/language-reference.md: add missing import to compile_package_artifact snippet - foundations/theory/03-propositional-operators.md: fix archive link Includes a codex review pass that further corrected: - cli/inference.md: JT exact diagnostics records iterations_run = 2 (collect + distribute), not 0 - review-pipeline.md: narrow _review_manifest.py tombstone description - propositional analysis snippet: clarify pkg is already-collected - archive link: rewrite as inline path to eliminate mkdocs INFO PR #634
User-facing framing fixes; no behavior changes. - for-visitors/what-is-gaia.md: rewrite "What Gaia Does" / "How It Works" so the v0.5 reality is visible. Gaia v0.5 does not auto-extract knowledge from papers; authors / agents write Python DSL packages and Gaia compiles + lowers + runs BP. Global corpus-wide recomputation belongs to the registry / LKM layer, not to a hidden automatic step in the local CLI. - for-users/quick-start.md: note gaia build init requires uv, document pip + uv tool install paths, add gaia --version, match the directory layout to what init.py actually emits, mention gaia inspect starmap. - for-users/hole-bridge-tutorial.md: add a callout at compat.deduction noting it is the legacy v5 surface (canonical v0.5 replacement is derive(C, given=[P])); bump example dependency gaia-lang>=0.1.0 to gaia-lang>=0.5. Includes a codex review pass that further corrected: - gaia build init step 6 wraps uv add in try/except; doc says "Attempts" with manual fallback now. - uv.lock marked as "present after uv dependency resolution succeeds". - gaia pkg register is dry-run by default; doc says "checks the release artifacts and prepares or writes git-backed registry metadata". PR #641 (replaces #635 which was auto-closed when its stacked base branch was deleted on #634 merge).
User-facing reference cleanup; no behavior changes. cli-commands.md: - Add a top-level "gaia --version" section documenting the version, channel, commit, and ir_schema lines. - Document gaia inquiry focus --push / --pop / --stack flags. - Add gaia inquiry hypothesis remove to the inquiry sub-command list. language-reference.md (Q19/Q20 split — keep design narrative, push API enumeration to docstrings + auto-generated reference): - Add forall, exists, iff to the imports cheat sheet. - Add a "First-order quantifiers" subsection with a worked example. - Slim the "Legacy / Experimental Strategy APIs" appendix from ~150 lines of per-function micro-tutorials to a focused migration table. - Add a banner near the imports cheat sheet pointing at the auto- generated lang.md reference. Includes a codex review pass that further corrected: - ir_schema example value: ir-v1+<12hex> (the actual format from gaia/_meta.py) instead of integer 7. - compile_metadata.json claim: removed the false claim that ir_schema is in compile_metadata.json (actual payload is gaia_lang_version / compiled_at / ir_hash). - First-order quantifiers example rewritten with actual v0.5 API: Domain / PredicateSymbol / UserPredicate / ClaimKind.QUANTIFIED. - compat reference pointer clarified. PR #636
Bring all 8 docs/foundations/gaia-ir/*.md files back into agreement with the actual v0.5 code (gaia/engine/ir/*, validator.py, _meta.py). Doc-side contract correction; no code changes. 01-overview.md: - Knowledge taxonomy: list all 6 KnowledgeType members. - Strategy table: replace deferred induction with the actual v0.5 CompositeStrategy-over-shared-conclusion-support shape. - Add Compose entity overview; flag is_qid as internal helper. 02-gaia-ir.md: - Knowledge schema: add v0.5 fields, document content_hash exclusions. - New §1.1.2 specifies content_hash payload as type|format|content|sorted((name,type)). - Knowledge type table expands to all 6 members. - New §1.4 Compose: schema, invariants (lcm_ prefix, DAG, no self-ref), lowering note, contrast with CompositeStrategy. - Operator §2.1: top-level vs FormalExpr-embedded ID rule. 03-identity-and-hashing.md: - §2.1 QID label charset corrected to [A-Za-z_][A-Za-z0-9_]*. - §3 content_hash formula code-aligned. - §4 add lcm_ Compose ID; clarify lco_ is required only for top-level. - §5 add ir_hash vs IR_SCHEMA distinction. 04-helper-claims.md: - §2 helper_kind table adds negation_result and a reviewable column. 05-canonicalization.md: - §1 + §2.2: quote new content_hash formula. - §7: align with unified induction story. - New §8 documents Compose role in canonicalization. 06-parameterization.md: - New "与 IR schema 版本的关系" section ties Parameterization to gaia._meta.IR_SCHEMA and the schema-bump pre-push hook. 07-lowering.md: - §4.1 leaf list now matches StrategyType. - §4.3 add support vs deduction lowering divergence. - New §4.4 covers Compose lowering. 08-validation.md: - §2 list all 6 KnowledgeType members. - §3 correct ID rule to top-level-only lco_/scope. - New §5 Compose validation. Includes a codex review pass that further corrected: - 03 hash length wording: "完整 SHA-256 hex digest (64 个十六进制字符)". - 03 canonical(formal_expr) impl pointer corrected to gaia.engine.ir.strategy._canonical_formal_expr (was wrongly pointing at gaia.engine.ir.graphs._canonicalize_strategy_dump). - 07 Compose Knowledge handling refined. - 08 composition validator overclaim reframed (graph-level validator doesn't actually enforce sub_knowledge graph closure today; field- shape only). PR #637
Apply slim-and-link strategy to gaia-lang foundations; correct a bp/inference routing pitfall; tighten contract status banners. Non-protected foundation layer. gaia-lang/knowledge-and-reasoning.md: - §4.2 helper claim visibility now points at gaia-ir/04-helper-claims for the public/private boundary. - New §4.4 documents the compiler extension registry from gaia/engine/lang/compiler/extensions.py. gaia-lang/predicate-logic.md: - Normalise quantifier examples to exists(x, ...) / forall(x, ...). gaia-lang/bayes.md: - Add a status callout at the top distinguishing the two surfaces. - Slim the "Verbs at a Glance" pseudo-signature block to a one-line conceptual summary plus a deep link to the auto-generated reference. gaia-lang/package.md: - Replace "reasoning strategies (reasoning.py)" with v0.5 action-verb framing; cross-link bayes.md from dependencies table. bp/inference.md (high-impact): - Add explicit "two paths" warning callout: gaia.engine.bp.infer() vs CLI's InferenceEngine route large graphs differently. bp/potentials.md: - Document formula_lowering="connective" exception on IMPLICATION. contracts/rebuttal-report.md: - Promote the status banner: no v0.5 code emits or consumes RebuttalReport / .gaia/review/rebuttal.json. Includes a codex review pass that further corrected: - knowledge-and-reasoning §4.4 register_action_lowerer signature was wrong: actual is (name, *, handles, lower) per gaia/engine/lang/compiler/extensions.py:57-66, not the original (action_type, lowerer, *, replace=False). Also reframed as engine- extension hook (used by peer modules like gaia.engine.bayes), not a package-author DSL surface. - bayes.md Quantity-With-Predicate framing corrected: it ships in v0.5 partial form (predicate priors via CDF, observation events recorded; posterior CDF update is follow-up). Original framing as v0.6+ target was wrong. - bp/potentials formula_lowering mechanism: it's metadata (op.metadata["formula_lowering"]), not a runtime parameter; source pointers corrected. - package.md gaia-lang dependency example bumped 2.0.0 → 0.5.0 to match pyproject.toml. PR #638
Wording-clarification / cross-link / status-banner level edits to docs/foundations/theory/ (frozen) and docs/foundations/ecosystem/ (protected). No theory or ecosystem semantics rewritten. theory/04-reasoning-strategies.md: - §1 Knowledge type table drops Template as a 4th type; lists 3 base types plus a callout that Template is teaching vocabulary, not an IR-level KnowledgeType. - §1.4 reframes Template as "Claim with parameters"; cross-link bridge to v0.5 Formula AST in gaia.engine.lang.formula and ir.logic. theory/07-belief-propagation.md: - Replace stale libs/inference/* source pointers with gaia/engine/bp/*. - Add an "Algorithm-family note" pointing at InferenceEngine and runtime routing policy (junction tree / TRW-BP / mean field VI). theory/08-causality-and-jaynes.md: - Promote v0.6+ status banner to "Target Design (v0.6+) — NOT current v0.5 contract". - Add a v0.5-mapping table: Claim→Claim, Action→Strategy variants, Mechanism / CausalFactor / mutilate / do() → not in v0.5. ecosystem/01-product-scope.md: - Add v0.5 grouped-CLI mapping under the abstract pipeline framing. ecosystem/06-belief-flow-and-quality.md: - Add a callout: federated registries / multi-LKM are multiplicity within tier-2 inference, not a third inference tier. ecosystem/04-registry-operations.md: - Reframe CI verification table with [Current] / [Target] markers. ecosystem/07-related-systems.md: - Replace stale "Status: Current draft" banner with "Current canonical — design positioning". Includes a codex review pass that further corrected: - ecosystem/04 [Current] / [Target] rows mis-scoped: gaia pkg register doesn't clone the package repo or check that all deps are in registry. Codex split into [Current CLI precheck] vs [Target registry CI]. - theory/04 Formula AST symbol names: "Predicate / Term" → actual exports are PredicateSymbol / UserPredicate / Term. - theory/07 InferenceEngine routing list: removed loopy_bp from the auto-routing list (it's only in the legacy gaia.engine.bp.infer() fallback). Added "并支持 forced exact". PR #639
Add an explicit early-reminder admonition right after the first introduction of `(p1, p2)` in §4.1 of `03-propositional-operators.md`, covering three points the reader otherwise has to wait for §4.5–§4.6 to encounter: - `(p1, p2)` are local interface parameters / potential weights, not global conditional probabilities. `P_eff(B|A)` only matches global `P(B|A)` numerically when the soft-implication is isolated. - The degenerate case `p2 = 0.5` is a flat factor row, NOT a global claim that `P(B|A=0) = 0.5`. It means the factor is silent at `A=0` and `B`'s belief is determined by `pi(B)` and other factors. - Setting `p2 = pi(B)` to "pass the prior through" would double-count the prior; flat (`p2 = 0.5`) is the correct MaxEnt encoding. Closes #239. The change is a single inserted blockquote (10 lines) that down-links to `06-factor-graphs.md` §3.7 and `07-belief-propagation.md` §2.2 so the reader sees where `(p1, p2)` actually become potential weights at BP time. Co-authored-by: Cursor <cursoragent@cursor.com>
In `docs/documentation-policy.md`, the 关联文档 row had `[docs/README.md](README.md)` — the link text reads as a concrete file path, but under mkdocs (directory-URL mode) `docs/README.md` is registered as the site root (`Home`), so the rendered href is `..` (the site root). On the GitHub source view it works fine, but on the published mkdocs site readers see the link land on the documentation index instead of any file literally named `docs/README.md`. Change the visible label to `文档导航首页` so the text describes where the link actually lands on both surfaces (mkdocs Home / GitHub source `docs/README.md`). The href is unchanged (`README.md`, mkdocs auto-resolves to the site root). Closes #614. Co-authored-by: Cursor <cursoragent@cursor.com>
Adds `docs/foundations/bp/choosing-algorithm.md`, a decision-oriented how-to page that complements the reference-oriented `inference.md`. Closes #616. The page covers the three concrete gaps huangy22 identified in the issue: 1. A one-minute decision tree (n / treewidth thresholds + fallback warnings) so authors don't have to reverse-engineer the routing logic from `engine.py`. 2. Three ways to obtain the treewidth of a real graph: read the `InferenceEngine.run` log line, call `jt_treewidth(fg)` directly, or use a "common IR shapes -> typical treewidth" cheat sheet keyed off the patterns Gaia authors actually write. 3. A concrete accuracy-cost table grounded in repo measurements: - JT vs exact: < 1e-3 (Cromwell floor) on tw <= 20 graphs - TRW-BP vs JT: < 1e-3 on block-DAG 50/100/250 (test_bp_large_scale) - MF VI vs TRW-BP: 30%-79% systematic error on hard-constraint graphs - explicitly NOT production-grade Plus practical material that does not belong in the algorithmic contract page: - Section 4: when to override `auto` and how (`"trw_bp"` escape hatch for large graphs, JT for reproducing someone else's exact result, exact_inference for ground-truth tests, MF VI only for "I accept large error" debugging). - Section 5: explicit "infer() vs InferenceEngine.run" guidance, pointing out the historical Loopy BP / MF VI divergence on n > 2000 and recommending `InferenceEngine` for new code. - Section 6: symptom -> cause -> action triage table for the most common BP runtime issues (MF warning, JT timeout, TRW-BP non-convergence, two-API mismatch). Strict mkdocs build passes (`make docs-build`). The new page is registered in `mkdocs.yml` under `Foundational Docs / Belief Propagation` between Inference and Local Vs Global, matching the natural reading order (Inference reference -> Choosing how-to -> rest of BP topics). Co-authored-by: Cursor <cursoragent@cursor.com>
… marker + nightly restore (#631) * fix(ci): release composite runs full validation gates + strict version assert Addresses chenkun's post-merge review on PR #620 (#620 (comment)). B1: Release composite previously delegated only to wheel-smoke after uv build. It did not run make test-all, mkdocs build --strict, or scripts/run_package_corpus.py, and did not verify nightly green for ${{ github.sha }}. A maintainer could dispatch alpha/stable and publish a wheel even when the package corpus would fail. Add the three release-time validation gates between wheel-smoke and publish. These gates run in both dry-run and non-dry-run modes — dry-run skips publish/tag/release, but the validation gates are themselves the pipeline being verified, so they always run. Note: with galileo's current --gate failures, the corpus runner step will fail every release dispatch until the galileo fixture is reviewed; this is the designed correct behavior (spec §4 release CI = nightly CI + publishing checks). B3: Strict version assertion. sed pattern was \`s/^version = "0.5.0"\$/...\` with only a print after (no assert). If pyproject.toml's pinned version drifts past 0.5.0, sed silently no-ops and the workflow can build/publish the wrong version. Add a grep -q assertion after sed that fails loudly on no-op. Also extend the existing \`gaia --version\` channel assert to also assert the version line, defending against any other version- injection bug. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(spec): update release-channel-strategy spec to match landed implementation Addresses chenkun's post-merge review's spec-drift framing (#620 (comment)): "the spec/decision record should be updated in the same PR so future maintainers do not read the spec as a stronger contract than the workflows actually enforce." Surgical updates to docs/specs/2026-05-16-gaia-release-channel-strategy.md to reflect what was actually implemented in PR #620 (merged) + the follow-on fixes in this PR: - Status header: Proposal -> Implemented; add "Last updated" note. - §2 / §8: PR CI command is the narrowed baseline+CLI form (no Codecov upload, no --cov-report=xml); Codecov retired entirely. - §3: PR/dev trigger matches actual workflow on:; nightly trigger is workflow_dispatch only (cron deliberately not added); release rows reference the four manual caller workflows by name. - §4: PR CI section reflects narrowed test selection and retired Codecov; nightly CI section reflects make test-all (no test-slow, test-all already covers it); release CI section enumerates the six invariants as a table mapping each to its enforcement mechanism (PEP 440 via grep -q + gaia --version asserts; changelog via --generate-notes; docs/corpus as in-composite gates). - §6: ir_schema field example is now concrete (ir-v1+<12-hex>) since §9 Q5 is resolved; brief note about the snapshot-hash-bump mechanism. - §8: re-titled "Implementation (landed)"; reads as record of what was built, not proposal of what to build. - §9: each open question marked resolved or deferred with the implementation-time decision; Q-codecov and Q-schedule added as resolved decisions captured during PR #620 review. Preserves voice and structure; does not rewrite the proposal. The spec moves from "proposal awaiting implementation" to "spec describing what was built", consistent with chenkun's framing. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * chore(agents): reshape AGENTS.md — drop overlap, consolidate into Design Discipline, add test-placement section Reshape AGENTS.md from 287 -> 160 lines. Removes overlap and adds the test placement guidance the marker-based PR-CI gate (next commit) needs. Removed sections: - Project Map (overlapped with README.md product overview) - Doc Fidelity (replaced by Design Discipline section with weaker but still-actionable wording; flag-don't-silent-fix posture preserved) - Protected Layers (replaced by Design Discipline section; relies on PR review + spec-first discipline rather than file-level lock) - Foundations Layers (off-loaded to docs/foundations/README.md; contributors going there for architecture context anyway) - Scripts and Pipelines (logging template; gaia's current scripts/ are simple enough not to need a template inline in canon) Added sections: - Design Discipline (consolidates Doc Fidelity + Protected Layers + Engineering Rules' "follow specs / scope edits" essence into 4 bullets) - Quality Gates > Test placement and PR-CI marker (the gap chenkun surfaced post-merge on PR #620; tells contributors where new tests go and when to mark them pr_gate) Adjusted: - Git and Worktrees: added one sentence on the 'git config --worktree core.bare false' requirement after 'git worktree add' (codified in parallel-dev_rsw.md, not previously surfaced in repo canon) Preserved (voice and substance unchanged): - Local Setup, Push Pre-flight, CLAUDE.md <-> AGENTS.md sync, Commits, Code Style, Community. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * feat(ci): switch PR-CI gate from directory-based to pr_gate marker Migrate PR-CI test gate selection from directory-based ('tests/baseline tests/cli') to marker-based ('-m "pr_gate and not slow"'). Future tests can be flagged for PR-CI inclusion via @pytest.mark.pr_gate without modifying ci.yml or the pre-push hook. Addresses the question chenkun raised in PR #620 post-merge review (see issuecomment-4467251197): a contributor adding new code didn't have a clean way to opt their tests into PR-CI without expanding the directory scope of ci.yml. Changes: - pyproject.toml: register 'pr_gate' marker - ci.yml: Run tests step uses '-m "pr_gate and not slow"' - .pre-commit-config.yaml: pytest hook uses same marker form - tests/baseline/**/test_*.py and tests/cli/**/test_*.py: add module-level 'pytestmark = pytest.mark.pr_gate' to preserve the current PR-CI scope (mass-tagged via temporary script). AGENTS.md was updated in the previous commit to document this. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * feat(ci): restore nightly schedule cron at 20:00 UTC + add nightly status badge After the AGENTS.md reshape + pr_gate marker migration land via the merge of chore/agents-reshape-pr-gate-marker_rsw, reconsider the "manual only" nightly cadence introduced late in PR #620: - Restore the schedule cron, set to 20:00 UTC daily (= 04:00 Asia/Shanghai next day), a quieter window than the original 06:00 UTC. - workflow_dispatch trigger remains for on-demand runs. - Add nightly status badge to README.md so failures are visible from the repo landing page. - Adjust spec doc and AGENTS.md text that claimed nightly was manual only — both now reflect the restored schedule + workflow_dispatch duality. Operator note: galileo fixture's --gate failures will cause every scheduled nightly to fail at the corpus runner step (blocking artifact upload by design). This noise is accepted as a daily reminder until the galileo fixture review lands. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * chore(agents): second trim — drop override clause, restore-symlink tip, mccabe rationale, Design Discipline; point Code Style to pyproject for machine-enforced bits Five further trims on top of the AGENTS.md reshape merged earlier in this PR via commit e9d3d15: 1. Push Pre-flight: drop the "only human contributor can override the hook in genuinely exceptional circumstances" clause — no documented escape hatch from the no-bypass rule. 2. CLAUDE.md ↔ AGENTS.md sync: drop the `rm CLAUDE.md && ln -sf` restore command. The pre-commit + pre-push hooks verify the symlink; if it breaks, the gate surfaces it. 3. Quality Gates: drop the standalone paragraph rationalizing the ruff mccabe complexity limit of 12. The rationale lives where the config lives (pyproject.toml) if anywhere; not canon-worthy. 4. Code Style: drop the Python-target and ruff-line-length bullets (both expressed in pyproject.toml). Add a one-liner pointing at pyproject for machine-enforced bits. Keep the 4 convention bullets (PEP 604, Google docstrings, Pydantic v2 APIs, Typer docstring brevity) — these are not lint-enforced. 5. Drop entire Design Discipline section. The 4 bullets it carried (specs-first design, flag-don't-silent-fix, scope discipline, prefer-existing-patterns) are removed as canon rules; future contributors and reviewers carry these as norms without an explicit canon entry. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
docs(theory): clarify (p1, p2) are local potentials at first intro
docs: align policy page link text with mkdocs render target
docs(bp): add how-to choose between JT, TRW-BP, and Mean Field VI
Adds reviewer-facing formula logic diagnostics with claim-local and cross-claim reports.
The alpha-0 release (#607) shipped explicit "error -> remove" stubs for relocated import paths and flat CLI verbs as a migration aid. Per the spec these were always intended to disappear in a follow-up release once external callers migrated. This is that follow-up. Removed: - 8 namespace tombstones under gaia/{bp,inquiry,ir,lang,logic,trace}/ plus gaia/engine/{lang/types,logic}/ - 3 per-symbol tombstone files in gaia/cli/ (_packages.py, commands/_review_manifest.py, commands/check_core.py) - 9 hidden flat-verb stubs (gaia/cli/commands/_flat_tombstones.py) and the register_flat_tombstones wiring in cli/main.py - gaia/_legacy_imports.py (the TOMBSTONED_NAMESPACES/SYMBOLS maps and the meta-path finder that drove all of the above) - tests/baseline/test_l2_tombstones.py and test_flat_verb_death.py (the contract tests for the stubs) along with their snapshot dir After this change: - import gaia.bp / gaia.lang / etc. raise plain ModuleNotFoundError - gaia compile / gaia infer / etc. fail with typer's standard "No such command" usage error (still exit 2) docs/migration.md (and the cli/engine reference + README + cli-commands docs) updated to describe the current behavior. The old-to-new mapping tables stay as the authoritative reference for anyone migrating off pre-alpha-0 code. docs/specs/2026-05-16-engine-module-reorg-design.md keeps its historical body and gains a "Post-launch update" section flagging the removal. Verified: tests/baseline -m pr_gate (99 passed, 91 snapshots), full sweep (2029 passed, 3 skipped), ruff + mypy --strict clean.
kunyuan
force-pushed
the
codex/v05-jaynes-maxent-cleanup
branch
from
31e0816 to
ab73859
Compare
kunyuan
force-pushed
the
codex/v05-jaynes-maxent-cleanup
branch
from
ab73859 to
0f3a551
Compare
kunyuan
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
6 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Normalize Gaia v0.5 deduction so open scientific consequences no longer reverse-penalize their antecedents.
IMPLICATIONas the pure Jaynes hard-constraint factor for global feasible-world countingDEDUCTIVE_IMPLICATIONfordeduction:A=trueforbidsB=false, whileA=falseleavesBat the MaxEnt 0.5 rowWhy
For pure hard constraints, Jaynes MaxEnt is still feasible-world counting over all states not ruled out by constraints.
For Gaia scientific
deduction, however, an unobserved consequence should remain open rather than count against the premise. In the toy shapeA -> B1andA -> B2, missing priors onB1/B2should leaveP(A)=0.5; an explicitP(A)=0.7should remain0.7; and a supported/observedBcan still increaseA.Validation
uv run --project /private/tmp/gaia_v05_maxent_audit ruff check .uv run --project /private/tmp/gaia_v05_maxent_audit ruff format --check .uv run --project /private/tmp/gaia_v05_maxent_audit mypyuv run --project /private/tmp/gaia_v05_maxent_audit --extra dev python -m pytest -q(2033 passed, 3 skipped)build,commit-lint, andtestpass