Repository navigation
feat(schema): empirical proof_profile measures + a trajectory "research record", once #231 ships real data #10
Description
Problem
An external review of the current export correctly identified two directions the schema
isn't covering yet, but its examples described schema capability more than populated
data — worth grounding before this becomes a design target, so this issue records both the
proposal and the actual current state.
Verified against the live corpus (358 packets) before filing:
| Field | Populated on |
|---|---|
proof_variants[] with >1 variant (e.g. canonical + restricted) |
2 of 328 formal packets |
proof_profile.{retrieval_depth,planning_depth,dependency_composition_depth,branch_count} |
5 of 330 variant instances (pre-existing fixtures, not the #9-adjacent population pass) |
dependency_manifest.retrieved_unused_candidates (non-empty) |
0 of 328 |
dependency_manifest.retrieval_candidates != used_theorem_deps |
0 of 328 (always identical today) |
Negative examples with repair_trajectories + real episode_id |
1 of 29 standalone negative-example packets |
None of this is a defect in #1-#8's work — the 313-packet population pass that added
proof_variants/dependency_manifest corpus-wide deliberately left these numeric/richer
fields unset rather than fabricate search-tree or retrieval-rejection data that was never
recorded. The schema already has room for it; there's just no real trajectory data behind it
yet for the bulk of the corpus.
Proposal
Two schema extensions, both gated on real data existing to design against:
1. Empirical proof_profile measures — extend the static classification
(primary_proof_class, automation_level, uses_*) with measures derived from an actual
search/repair process:
{
"search_width": null,
"repair_count": null,
"failed_attempts": null,
"models_used": null,
"verification_rounds": null
}2. A "research record" / trajectory object — the packet currently only exports the
destination (a verified proof); the journey (goal -> attempt -> failure -> observation ->
new helper lemma -> repair -> proof) isn't captured anywhere. This is conceptually adjacent
to repair_trajectory (#4) and rl_transition (#9) but oriented at human/model-readable
narrative rather than RL steps or diagnostic bookkeeping — needs its own design pass to avoid
overlapping either.
Why this is blocked, not just unscoped
Every one of these fields requires real proof-search trajectory data (search tree shape,
repair counts, per-model attempt history) that MathCorpus does not retain for the packets
already in this corpus, and that the live pipeline doesn't yet produce either —
llm-driven-proof-search#231 (persisting real reward/terminal/observation/trajectory data in
the runtime) is still open with no implementation started, same blocker already tracked in
#9. Populating these fields today would mean fabricating plausible-looking zeros/counts,
which this repo's export policy treats as a hard no (see docs/rl-transitions.md's honesty
rule for the same reasoning applied to rl_transition).
Scope (do not start until #231 ships)
- Design
search_width/repair_count/failed_attempts/models_used/verification_rounds
against real distributions once #231-derived trajectory data is importable — thresholds and
even field necessity may change once real numbers are visible. - Design the research-record object's shape against a real trajectory export, decide its
relationship torepair_trajectory(feat(data): add negative-example and repair-trajectory child records #4) andrl_transition(feat(export): add a canonical RL transition dataset exporter and validator #9), and decide whether it's a
new MCIP record type or a derived/aggregated view overrl_transitionsteps. - Both are additive (minor schema bump), matching
schema/mcip/v1/README.md's versioning
policy.
Dependencies
llm-driven-proof-search#231— real trajectory/reward/terminal persistence (hard blocker)- feat(export): add a canonical RL transition dataset exporter and validator #9 — the
rl_transitionschema/exporter this may end up building on top of or alongside - feat(data): add negative-example and repair-trajectory child records #4 — existing
repair_trajectoryrecord type this must not duplicate - feat(schema): define MathCorpus Interchange Protocol v1 for Proof Search enrichment #1 — MCIP v1 base
Activity