Repository navigation
feat: v3.8 hierarchical proof search — full milestone (foundation + integration) - #10
Merged
Merged
Conversation
First commit toward the v3.8 hierarchical proof search milestone. Lands
the data structures the search/explorer/microkernel layers will build
on, plus the design spec they all reference. No behavior change to the
existing GVR loop — proof_graph.py is not yet wired in anywhere.
Spec: docs/superpowers/specs/2026-04-11-v3.8-tree-search-design.md.
Roadmap context: user chose Model F (PUCT tree search) on 2026-04-02
after the E-vs-F experiment came back indecisive.
Modules added
-------------
- src/alethic/proof_graph.py — AtomStatus enum, AtomNode (mutable, with
from_annotation classmethod that lifts frozen AtomAnnotation into a
search-state-carrying node), ProofGraph (gaps/anchors/neighbors/
subdivide/downstream/is_complete/assemble_solution), plus an internal
Kahn's-algorithm topo sort used for deterministic assembly.
Design decisions baked in
-------------------------
- Composition, not inheritance: AtomAnnotation stays frozen (v3.5+
parsing code is unaffected); AtomNode is a parallel mutable structure
populated via from_annotation(). Two value types, one canonical
parser.
- Synthetic atoms with id<0 (preamble id=-1, residual id=-2) auto-
anchor in from_annotation — they are problem text or trailing prose,
never gaps. The monolithic fallback (id=0) is the one synthetic that
IS the proof, so it does enter normal verification.
- Subdivision rewrites dependents' deps to point at the chain tail.
Without this rewrite, topological assembly puts dependents in the
wrong position relative to the new chain (parent is skipped during
assembly but still occupies its old slot in the dep DAG). Tested
explicitly via test_dependents_rewired_to_chain_tail and
test_subdivided_parent_skipped_children_appear.
- Children are chained, not parallel: child_0 inherits parent's deps;
child_i (i>0) depends on child_{i-1}. Matches how a sub-proof actually
works — intermediate result A → intermediate result B → conclusion.
- neighbors() uses topological order, not ID order. Subdivision IDs
start at 1,000,000 (above the typical atom-ID space); ID-order would
put all sub-atoms after every original atom, which is wrong
positionally. Topo order respects the chain semantics.
- next_id floor of 1,000,000 is defensive — parse_atoms enforces
MAX_ATOMS=12 today so collisions are impossible, but the cap could
rise. Floor leaves room for deep subdivision under any future cap.
Tests
-----
tests/test_proof_graph.py — 52 tests across 8 test classes covering
AtomNode lifting + q_value math, ProofGraph construction with preamble/
residual/monolithic edge cases, gaps/anchors topo ordering, neighbor
selection across pending+failed atoms, full subdivision semantics
(chaining, level/parent wiring, dep rewriting on dependents, error
paths), downstream BFS for re-verify propagation, is_complete with
nested subdivision, and assemble_solution including the
subdivided-parent-skipped scenario.
1422 → 1474 tests pass. ruff clean, mypy clean.
Out of scope (next PRs)
-----------------------
- search.py (PUCT gap selection, re-bridge management)
- explorer.py (Alien-style technique enumeration)
- microkernel.py (atom-scoped generate/verify/revise)
- AgentConfig wiring for max_bridges/max_depth/technique_budget/etc.
- Skill-side equivalents (deferred until library implementation stabilizes)
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Second commit on the v3.8 milestone branch — adds the GVR microkernel
that the search layer (next PR) will dispatch per-gap. The microkernel
takes a single MicrokernelTask (one gap, two anchors, one chosen
technique) and runs an atom-scoped generate → verify → revise loop,
returning a MicrokernelResult with one of three statuses: filled,
too_large, or failed. No behavior change to the existing GVR loop —
microkernel.py is not yet wired in anywhere.
Spec: docs/superpowers/specs/2026-04-11-v3.8-tree-search-design.md
§Layer 3 — GVR Microkernel (lines 30-43, 105-122, 161-202).
Modules added
-------------
- src/alethic/microkernel.py — MicrokernelTask / MicrokernelResult
frozen dataclasses; gvr_microkernel() entry point; atom-scoped prompt
templates for math + physics (generator system, verifier system,
reviser system) plus a shared user-template trio that brackets the
gap with left/right anchors and the chosen technique; helpers
_detect_too_large, _extract_atom_content, _render_atom_template,
_select_system_prompts.
Design decisions baked in
-------------------------
- Reuse existing subagents.py via system_prompt= / user_template=
override hooks. No changes to generate() / verify() / revise() APIs.
The atom-specific placeholders (left_anchor, right_anchor, technique)
are pre-rendered via _safe_format before the call; the {problem}
placeholder stays open for the subagent's own _safe_format pass to
fill. This works because _safe_format leaves unknown placeholders
untouched (re.sub with kwargs.get(name, original_match)).
- Atom output header is the literal "ATOM[GAP]", not "ATOM[N]" with a
numeric ID. The gap's true ID is owned by the search layer's
ProofGraph, not the LLM — fixing the header removes a class of
"model invents wrong ID" bugs and makes _extract_atom_content's
regex bulletproof.
- Two too-large channels: explicit ("GAP TOO LARGE" literal in
generator/reviser output) and implicit (keyword scan over verifier
critique for phrases like "several steps", "non-trivial intermediate",
"should be subdivided"). Both lead to status="too_large" for the
search layer to subdivide via ProofGraph.subdivide(). Tested across
11 keyword variants plus negative cases.
- balanced=False on the atom generator — the existing
BALANCED_GENERATOR_ADDENDUM is counterexample-first anti-confirmation
guidance. Between two established anchors there is nothing to
counterexample. Tested by test_balanced_false_for_atom_generator.
- Microkernel emits no events. Event logging belongs to the search
layer, which has iteration/gap-id context the microkernel doesn't.
Microkernel returns a value; search layer logs it.
- Unknown domain falls through to math system prompts (math is the
canonical pattern; physics is the explicit override). The reviser
system prompt is domain-agnostic.
Tests
-----
tests/test_microkernel.py — 55 tests across 7 test classes:
- TestDataTypes (5): construction + frozen semantics for Task/Result
- TestDetectTooLarge (12): explicit signal, case insensitivity, all 11
keyword hints parameterized, negative cases, partial-word non-trigger
- TestExtractAtomContent (7): header at start, with leading whitespace,
after preamble, no-header passthrough, empty, only-header,
multi-line body preservation
- TestRenderAtomTemplate (3): atom placeholders substituted, downstream
placeholders left untouched (the key invariant for the two-pass
rendering)
- TestSelectSystemPrompts (3): math / physics / unknown-defaults-math
- TestPromptTemplates (6): all required placeholders present in each
template, GAP TOO LARGE mentioned in all three user templates
- TestGvrMicrokernel (13): happy path filled, explicit too_large from
generator, verifier-hints-too_large skips revision, successful
revision after one failure, budget exhausted (max_revisions=2),
reviser emits too_large, zero max_revisions, confidence below
threshold falls into revision, physics/math system-prompt dispatch,
atom-placeholder pre-rendering invariant, balanced=False invariant,
ledger threading, critical-issue blocks acceptance
1420 → 1475 tests pass (+55). ruff clean, mypy clean.
Out of scope (next PRs)
-----------------------
- search.py (PUCT gap selection + technique enumeration + re-bridge
management). This is where the 5 open Qs from the spec bind (PUCT
formula details, subdivision triggers, variant-B integration).
- explorer.py (Alien-style technique enumeration with coherence ×
novelty scoring).
- AgentConfig wiring for max_bridges / max_depth / technique_budget /
c_puct / atom_revisions / search_mode.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Layer 2 of the v3.8 hierarchical proof search. For each gap, the
exploration layer asks the model to enumerate 3-5 bridging techniques
between the established left anchor and the target right anchor, with
a coherence prior in [0, 1] per technique. Output: list[Technique]
filtered against tried_techniques (case-insensitive). The search
layer combines coherence with novelty for PUCT-based selection.
- src/alethic/explorer.py (~250 LOC):
- Technique frozen dataclass (name, coherence)
- EXPLORER_SYSTEM_MATH / EXPLORER_SYSTEM_PHYSICS / EXPLORER_USER prompts
- _parse_techniques: ordinal-indexed pair parser (TECHNIQUE N / COHERENCE N
joined on N — robust to interleaved prose, reordered lines, missing
coherence entries default to 0.5 neutral prior)
- _filter_novel: case- and whitespace-insensitive dedup vs tried list,
also dedups intra-call duplicates, preserves input order
- _format_tried, _select_system_prompt helpers
- enumerate_techniques: one _call_model call at config.temperature_generator
- tests/test_explorer.py: 47 tests across 7 classes (TestTechnique,
TestFormatTried, TestParseTechniques, TestFilterNovel,
TestSelectSystemPrompt, TestPromptTemplates, TestEnumerateTechniques).
Design note: calls subagents._call_model directly rather than going
through generate() — the explorer output is structured data
(technique list), not a Solution, so wrapping in Solution.solution_text
and re-parsing would add a round trip with no benefit. Uses
_safe_format (not str.format) to tolerate literal {/} in anchor text
from LaTeX (e.g. \frac{a}{b}, \sum_{i=0}^{n}).
Parser fix: same-line whitespace runs use [ \t]* not \s* — \s includes
\n, which with MULTILINE causes (.*?) to bleed into the next line when
the body is empty (regression caught by test_blank_name_dropped).
Test count: 1475 → 1522 (+47).
Gates: ruff clean, mypy clean on explorer.py, full suite green.
Spec: docs/superpowers/specs/2026-04-11-v3.8-tree-search-design.md
§Alien Exploration (lines 231-241).
…e-bridge Fourth and final commit on PR #10 — wires together the proof-graph data layer (e72a7b1), the GVR microkernel (cb0b9e7), and the Alien-style explorer (e466db7) into a single solve() entry point implementing the spec's four-phase algorithm: Phase 1 — Bridge: generate(...) → one full candidate solution Phase 2 — Verify: classify each atom as ANCHORED or FAILED from the verifier's ATOM CONFIDENCES (fallback to verdict if no per-atom data) Phase 3 — Gap-fill: PUCT-driven gap selection → enumerate_techniques → puct_select_technique → gvr_microkernel → status update. Loop until the graph completes OR every gap exhausts its technique_budget. Phase 4 — Re-bridge: summarize the failed path, push the summary into failed_approaches for the next bridge's strategy reset, restart from Phase 1. Bounded by max_bridges; UNSOLVED with best-seen on exhaust. Spec: docs/superpowers/specs/2026-04-11-v3.8-tree-search-design.md §Search Layer (lines 21-39, 126-202, 204-218, 258-267) and §Presets (lines 295-302). Modules added ------------- - src/alethic/search.py (~520 LOC): - SearchConfig frozen dataclass with PRESETS for default/thorough/ extreme (matches the spec preset table exactly). Validates all fields in __post_init__; from_preset() supports overrides. - _GapState mutable dataclass: per-gap auxiliary state (failures, last_error_category, technique_attempts). - puct_score(): standard PUCT formula Q + c·P·√N_total / (1 + N_this). n_total bumped to max(n_total, 1) so a cold gap pool still gets a nonzero exploration term (mirrors MCTS PUCT papers using √N_parent). - gap_prior(): error-category-weighted prior. algebra/citation keep baseline 1.0 (mechanically fixable, worth more attempts); logic/missing_case/interpretation get 0.5× (need different technique, not more attempts at same one). Per spec §PUCT Scoring lines 213-218. - puct_select_gap(): selects the next gap via PUCT, filtering out technique-budget-exhausted gaps. Ascending-ID tiebreak for determinism (matches ProofGraph._topo_order convention). - puct_select_technique(): selects next technique within a gap. Coherence acts as Q, novelty (1.0 untried, 0.1 tried) as prior. Input-order tiebreak preserves explorer's ordering. - _classify_atoms_from_verification(): mark ANCHORED/FAILED in-place from VerificationResult.atom_confidences (if present, per-atom threshold check) or verdict-only fallback (CORRECT → all anchor; else → all fail). Synthetic preamble/residual atoms (id<0) never touched. - summarize_failed_path(): one-paragraph summary fed to the next bridge via subagents.generate(failed_approaches=...). - solve(): the four-phase entry point. Returns AgentResult with verdict=CORRECT on completion (assemble_solution from graph, confidence = min over all atom confidences), or UNSOLVED with best-seen on bridge budget exhaust. - src/alethic/models.py: five new EventType values for v3.8 events (BRIDGE_GENERATED, GAP_FILLED, GAP_FAILED, GAP_SUBDIVIDED, RE_BRIDGE_TRIGGERED). Existing AgentResult.to_dict serializer picks them up automatically via e.type.value spread (no schema change needed). Design decisions baked in ------------------------- - SearchConfig is a separate dataclass, NOT new fields on AgentConfig. Wiring search_mode / max_bridges / etc. into AgentConfig is the next stacked commit per the state file's Next Step #2. Keeps PR #10's commits independently reviewable. - Newly subdivided children are flipped from PENDING to FAILED in search.py (via _mark_children_as_gaps) so they enter the gap pool for puct_select_gap. ProofGraph.subdivide() leaves them PENDING because "never verified" is semantically correct at the data layer. graph.gaps() filters strictly on FAILED because "verified and failed" is semantically correct as a gap definition. The policy decision "treat unverified subdivision children as gaps" lives in the orchestrator (search.py), keeping the data-layer module oblivious to search-layer policy. - Re-bridge prompting reuses the existing subagents.generate( failed_approaches=...) keyword arg. The generator already appends a "previously attempted strategies that did NOT work" section to the user message — no new prompt machinery, no OracleRouter coupling required for this commit. - Two subdivision triggers, both implemented per spec §Recursive Subdivision lines 252-254: 1. Microkernel returns status="too_large" (verifier-detected complexity hint OR explicit GAP TOO LARGE from generator/reviser). 2. K consecutive failed-status returns on the same gap (failure_subdivision_threshold, default 3). Subdivision capped by max_depth — gaps at max depth that hit either trigger become terminal failures rather than recursing. - Empty-technique-list defense: if enumerate_techniques returns [] (or all candidates filter as previously-tried), the gap is marked exhausted by injecting a placeholder "__exhausted__" key with the full technique_budget — guaranteeing the next puct_select_gap call skips it. Prevents infinite loops when the explorer can't think of anything (test_empty_technique_list_skips_gap_eventually_breaks). - AgentResult.iterations_used in tree-search mode counts bridges (one bridge = one full solution generation), the closest analog of the flat-GVR iteration. candidates_per_iteration stays 1 — v3.8 parallelism is at the gap level, not the candidate level. Tests ----- tests/test_search.py — 57 tests across 14 test classes: - TestSearchConfig (12): defaults match spec preset table, frozen, all 7 fields validated, presets default/thorough/extreme + overrides. - TestPuctScore (4): baseline formula, zero-Q exploration, exploration- beats-exploitation regime, monotonic in Q. - TestGapPrior (7): default uniform, algebra/citation baseline, logic/missing_case/interpretation 0.5×, unknown category default, n_gaps=0 graceful. - TestGapState (2): defaults + sum helper. - TestPuctSelectGap (6): empty gaps, single gap, two-cold-gap ID tiebreak, Q-dominance when c_puct=0, exhausted-gap filter, all- exhausted returns None. - TestPuctSelectTechnique (4): empty list, coherence dominance, novelty penalty for tried techniques, input-order tiebreak. - TestSummarizeFailedPath (3): counts in summary, lists tried techniques + error category, empty-graph degenerate case. - TestClassifyAtomsFromVerification (4): CORRECT anchors all, atom_confidences per-atom classification, no-per-atom-data fallback, synthetic preamble preserved. - TestSolveBridgeHappyPath (1): first bridge CORRECT → no microkernel calls, ACCEPT event emitted. - TestSolveGapFilling (1): single failed atom → microkernel fills, assembled solution contains the fix, confidence = min of atoms. - TestSolveSubdivisionTooLarge (1): too_large response → subdivide → two children fill → 3 mk calls total, GAP_SUBDIVIDED event with reason="too_large". - TestSolveSubdivisionFailureCount (1): K=3 failed responses on same gap → auto-subdivide → children fill, GAP_SUBDIVIDED event with reason="failure_count". - TestSolveMaxDepthCap (1): max_depth=0 → no subdivision regardless of trigger → UNSOLVED. - TestSolveReBridge (1): bridge 0 exhausts → bridge 1 starts with failed_approaches kwarg containing the summary, then succeeds. - TestSolveBridgesExhausted (1): both bridges fail → UNSOLVED with best-seen (bridge 0's 0.6 beats bridge 1's 0.5). - TestSolveEvents (2): bridge_index in BRIDGE_GENERATED data, technique+confidence+gap_id in GAP_FILLED data. - TestSolveExplorationGivesNoTechniques (1): enumerate returns [] → gap marked exhausted → search terminates (no infinite loop). - TestSolveTechniqueBudgetExhausted (1): technique_budget=3 caps the number of microkernel calls on a single gap. tests/test_new_types.py: TestEventType.test_member_count updated from 10 → 15 to reflect the five new v3.8 EventType values. 1522 → 1579 tests pass (+57). 2 skipped, 3 xfailed unchanged. ruff clean on src/alethic/search.py, src/alethic/models.py, and both test files. mypy clean on src/alethic/search.py. Out of scope (next stacked commit / follow-up) ---------------------------------------------- - AgentConfig wiring for search_mode / max_bridges / max_depth / c_puct / technique_budget / atom_revisions (Next Step #2 in the state file). - agent.py dispatch: when config.search_mode == "tree", route through search.solve() instead of the existing flat GVR (Next Step #3). - propagate_reverify() — when a gap fills, re-verify downstream atoms whose meaning depends on the new content. Spec line 178 mentions it but isn't required for the minimum-viable v3.8 search. - Skill-side parity — orchestrator cannot use ThreadPoolExecutor; defer the sequential-only design decision until the library implementation stabilizes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Port the v3.7.1 library fix (oracle_router.rank_candidates) to the skill orchestrator: rank candidates by verdict tier first, confidence second. Pure max-confidence selection let UNSOLVED@1.00 beat CORRECT@0.99. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- Delete classify_errors_routed() and get_all_categories(): no production callers since v3.7 wired _ORACLE_ROUTING directly into OracleRouter.route(). Tests repointed at the production path (classify_errors + _ORACLE_ROUTING lookup) so routing-table coverage is preserved. - Add docs/skill-parity.md: defines which semantics must stay synced between library and skills, and which features are intentionally library-only. - Gitignore experiment artifacts (data/calibration/, docs/results/, scenario/, .planning/). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Skill parity uplift (per docs/skill-parity.md must-sync table):
- Disproof escalation (library v3.7.1): on stall reset, when the previous
error category is false_premise/interpretation/counterexample OR the last
2 iteration verdicts are both UNSOLVED, append a domain-specific
{disproof_addendum} to the reset context. Mirrors
oracle_router._should_disproof(). Addenda ported from
DISPROOF_STRATEGY_ADDENDUM / PHYSICS_DISPROOF_STRATEGY_ADDENDUM into the
solve/derive SKILL.md configurators.
- Classifier categories (library v3.7.2): add false_premise and wrong_method
keyword lists to both orchestrator classifier sites and reorder to the
library's hierarchical priority (problem > approach > structural >
mechanical > presentation). Add false_premise to the dynamic-N escalation
row and revision addenda for both new categories.
- stall_reset events gain a disproof field; dashboard prints
[STALL RESET + DISPROOF] when fired.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Opt-in tree search via AgentConfig.search_mode, agent-level dispatch, tree-mode checkpoint/resume, oracle-routing scaffolding consumption, CLI --search flag, eval harness pass-through. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e/search Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The shared orchestrator must not hardcode 'mathematical' (test_no_hardcoded_math_in_instructions); introduced in 21f7e32. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…sume from tree_state.json Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…s; persist total_revisions Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…al verify via extra_system Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…MicrokernelTask docstring Spec-review follow-up for fc4abe1 (plan Task 5 Step 5.3a). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…-loop verify Quality-review follow-up for fc4abe1: prior tests only asserted the Phase-2 verify call; the revision-loop verify site was unpinned. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ion handling Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…lat divergences Quality-review follow-up for ad79319: unsolved finalization, resume forwarding, and no-clobber-when-self-checkpointed are now pinned; _solve_tree docstring documents exhaustion propagation (deliberate), ledger restart on resume, and flat-only calibration/autopsy. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…heckpointError exit Quality-review follow-up for d6de1a8: guard messages now name the --search flag; tree exhaustion checkpoint logs a resume command; main() exits cleanly on checkpoint errors; --search choices share a constant; explicit '--search flat' no-op pinned by test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…k reports Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…l metrics Quality-review follow-up for 8193290. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…problem mismatch Final-review fix: resuming a tree checkpoint with max_bridges <= the checkpointed bridge_index produced an empty bridge range — the restored graph was never consumed and the finalization write destroyed the live checkpoint (graph_dict=None, status=unsolved). Now fails loud with CheckpointError before touching the checkpoint. tree_state.json gains max_bridges and problem fields (optional, old checkpoints tolerated); tree resume now warns on problem mismatch like the flat path. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
All 45 step checkboxes ticked; status banner added with final gate numbers and the final-review fix reference. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
hyperion-git
marked this pull request as ready for review
June 11, 2026 05:48
hyperion-git
changed the title
hyperion-git
added a commit
that referenced
this pull request
Jul 29, 2026
The repo had no CI of any kind — no .github/, no pre-commit — while carrying four open PRs totalling ~10,400 unreviewed added lines. Every merge to date has been gated only by someone running the suite locally. Gates on pytest and mypy. Ruff runs advisory (continue-on-error) because main carries 111 pre-existing findings, 93 of them in tests/ and mostly unused imports and import ordering; gating on that today would block every merge on unrelated debt. Clean those in a dedicated pass, then drop continue-on-error. No ANTHROPIC_API_KEY is provided, deliberately: the suite is fully mocked and must stay that way, so a test that starts needing a live key will fail here. Landing this via PR #12 rather than a separate PR so it takes effect after PR #11 brings mypy to 0, which means it gates the two merges that actually carry risk (#10 at 8467 lines, #9 with three conflict hunks). Assisted-by: Claude Code:claude-opus-5 Signed-off-by: A. Friedrich <alex@f2media.de>
Brings in PR #11 (mypy 18->0), PR #12 (RQGM analysis, eval metric split, tracked evidence, CI workflow). One conflict, in the run_benchmark() return dict — both sides added keys and both are kept. The merged report now carries all three axes needed to compare two runs: search_mode which code path ran (#10) anchor_sha256 which problem set ran (#12) gate_epoch how outcomes were scored (#12) Also un-ignores data/calibration/ and docs/results/. They were ignored as "generated outputs", but they hold the project's only measurement record and that record sat untracked for months. New runs now surface as untracked so they get a keep/discard decision instead of being dropped silently. Verified: 1653 passed, 2 skipped, 3 xfailed. Assisted-by: Claude Code:claude-opus-5 Signed-off-by: A. Friedrich <alex@f2media.de>
hyperion-git
added a commit
that referenced
this pull request
Jul 29, 2026
Brings in PR #11 (mypy), PR #12 (metric split, evidence, CI), PR #10 (v3.8 tree search). Three conflicts, all keep-both: models.py EventType REVISER_ALL_DECLINED (#9) + the 5 v3.8 search events -> 16 members (10 in v3.7, +5, +1) models.py AgentConfig enable_surveyor/enforce_checks_floor (#9) + search_mode/search (#10) test_new_types.py len(EventType) assertion 11 vs 15 -> 16 Also fixes a mypy regression this merge exposed: _parse_survey() bound `m` twice for two different types — Match[str] from enumerate() at line 115, then Match[str] | None at 133. Renamed the second to `sanity` rather than annotating it, since the reuse was the actual defect. Without this, merging #9 would have silently undone part of #11's mypy cleanup. Verified: 1707 passed, 2 skipped, 3 xfailed; mypy 0 errors across 41 files. Assisted-by: Claude Code:claude-opus-5 Signed-off-by: A. Friedrich <alex@f2media.de>
hyperion-git
added a commit
that referenced
this pull request
Jul 29, 2026
No PR owned the version bump, so the repo declared 3.7.0 while main already contained the v3.8 hierarchical proof search milestone. Bumps all five sites: pyproject.toml, .claude-plugin/plugin.json, .claude-plugin/marketplace.json, src/alethic/__init__.py, and the CLAUDE.md manual-install DEST path. 3.8.0 rather than 3.7.3: #10 and #9 both add features (tree search; surveyor and checks-floor). Tree search is opt-in — search_mode defaults to "flat" in all four presets, verified — so the classic GVR path is unchanged. Assisted-by: Claude Code:claude-opus-5 Signed-off-by: A. Friedrich <alex@f2media.de>
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
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
The complete v3.8 hierarchical proof search milestone (user chose Model F / PUCT tree search on 2026-04-02 after the E-vs-F experiment came back indecisive). 19 commits across two phases:
proof_graph.py(data),microkernel.py(atom-scoped GVR),explorer.py(Alien-style technique enumeration),search.py(PUCT gap selection + re-bridge orchestration).docs/superpowers/) —SearchConfiginmodels.py+AgentConfig.search_mode/searchfields, graph JSON serialization, tree-mode checkpoint/resume (tree_state.json),_ORACLE_ROUTINGconsumption on gap retries (adversarial verify viaextra_system),MathAgent._solve_tree()dispatch with bidirectional resume guards, CLI--search flat|tree, eval-harnesssearch_modepass-through withbridges_used/gaps_filledmetrics, docs.Rollout is opt-in:
search_modedefaults to"flat"for every preset — flat-path behavior is provably unchanged (dispatch early-return + resume guard are the onlysolve()changes). The spec's preset table (default/thorough/extreme → tree) applies only after a benchmark gate, as a future v4.0 edit.How it works
A full candidate solution is a "bridge"; verification classifies its atoms as anchors (verified) or gaps (failed). PUCT (
Q + c·P·√N_total/(1+N)) selects which gap to attack; the explorer enumerates bridging techniques (coherence × novelty); the GVR microkernel fills one gap between two anchors. Gaps that resist subdivide (verifier-detectedtoo_largeor K=3 failure count); bridges that exhaust re-generate with the failed-path summary injected. On context exhaustion,search.solve()self-checkpoints totree_state.json; resume restores graph + gap states (--search tree --resume <dir>).Review process
Every integration task went through subagent-driven development with two-stage review (spec compliance, then code quality), each followed by fix + re-review loops. A final whole-implementation review traced the CLI→agent→search→checkpoint→resume seams end-to-end; its one Important finding (resume under a shrunken
max_bridgesdestroyed the live checkpoint via an empty bridge range) is fixed inb948d47— the guard now fails loud withCheckpointErrorbefore any write, andtree_state.jsoncarriesmax_bridges+problemfor diagnostics and mismatch warnings.Known accepted losses (documented in code at the seams)
TokenLedger(cost accounting restarts per process); events list is not persisted across resume.apply_calibration) and autopsy-on-UNSOLVED run only on the flat path.docs/skill-parity.md— no skill counterpart planned.Test plan
pytest -q— 1641 passed, 2 skipped, 3 xfailed (baseline at milestone start: 1422; +219 across foundation + integration).ruff check src tests— zero new findings vs pre-plan baseline (110 → 110, all pre-existing debt).mypy src/alethic— zero new errors (18 → 17; one transient resolved).b948d47).data/benchmarks/*-sample.jsonviaalethic eval run ... --search tree) — post-merge, gates the v4.0 preset flip.🤖 Generated with Claude Code