Repository navigation
8000
feat(export): add a canonical RL transition dataset exporter and validator #9
Description
Problem
MathCorpus currently exports packet records, corpus metadata, and nested packet JSON, but it does not provide a canonical reinforcement-learning transition dataset. Packet rows are theorem records, not state → action → reward → next_state experiences.
MathCorpus needs its own RL export tooling so imported Proof Search trajectories can be validated, split, filtered, and distributed without depending on the Proof Search database or exporter implementation.
This issue should consume the transition format produced by llm-driven-proof-search#238 and align with MCIP v1 from #1.
Scope
Add a versioned RL transition schema and tools to:
- validate imported transition bundles
- join transitions to immutable packet identities and statement hashes
- enforce training eligibility, redaction, contamination, and split policy
- export canonical JSONL
- export optional Parquet with native scalar columns
- group transitions into full episode manifests
- produce dataset cards and aggregate statistics
Required transition fields
Each accepted transition must include or explicitly mark unavailable:
- schema version
- packet ID and formal statement hash
- episode and problem-version IDs
- step index
- state or state-artifact reference
- action
- scalar reward
- next state or next-state artifact reference
- terminated and truncated flags
- terminal/truncation reasons
- action and verifier outcome
- environment, verifier, action, observation, reward-policy, and restriction-profile versions
- model config hash and redaction-aware model metadata
- token, cost, wall-time, and Lean CPU metrics
- diagnostic and dependency artifact references where available
Acceptance criteria
- The exporter never treats
packets.jsonlor packet-shaped records as RL transitions. - Validation rejects transitions missing core RL fields unless an explicit legacy missing-data policy applies.
- Imported transitions are cryptographically bound to the referenced packet statement and environment.
- Train/validation/test assignment follows packet lineage and template-family locking to prevent leakage.
- Public policy can independently redact observations, actions, diagnostics, model metadata, and artifacts while retaining hashes.
- JSONL and Parquet exports contain identical logical records.
- Parquet exposes major scalar fields as native columns rather than only a serialized JSON blob.
- Episode manifests verify ordered, gap-free transition sequences and final outcome consistency.
- Aggregate reports include episode count, transition count, reward distribution, outcome distribution, horizon length, token/cost/timing summaries, missing-field rates, and negative-action rates.
- Conformance fixtures round-trip with the Proof Search exporter from
llm-driven-proof-search#238. - Existing
packets.jsonl, negative-example, SFT, DPO, and MCIP outputs remain separately named and documented.
Dependencies
- feat(schema): define MathCorpus Interchange Protocol v1 for Proof Search enrichment #1 for MCIP v1 identity and hashing rules
- feat(data): add negative-example and repair-trajectory child records #4 for negative-example and repair-trajectory child records
- feat(metrics): add multi-model empirical difficulty and native analytics exports #5 for native analytics exports
- feat(import): add MCIP importer, packet enrichment workflow, and 190-packet backfill #6 for the enrichment import workflow
Mnehmos/llm-driven-proof-search#238for the source transition contractMnehmos/llm-driven-proof-search#231for complete runtime persistence
Activity
Mnehmos commentedon Jul 12, 2026
Started the MathCorpus-side consumer (commit 9d8b5af):
schema/mcip/v1/rl_transition.schema.json— new record type consuming the shapellm-driven-proof-search#238proposes, plus every field this issue lists as required-or-explicitly-unavailable. Required-but-nullable, with amissing_field_reasonshonesty mechanism so a legacy gap is explained rather than defaulted to0/false.tools/mathcorpus/rl_transitions.py— bundle validation, packet join (packet_id+formal_statement_sha256), publish-eligibility (never more permissive than the joined packet's owntraining.eligibility), episode step-index contiguity, and the missing-field honesty check.tools/export_rl_transitions.py— validate → join → policy-filter → canonicalrl_transitions.jsonl+rl_episode_manifest.json.export_eligibility: private_only) round-trip cleanly through validation and the exporter.Leaving this open — real cross-repo blocker, not just remaining scope. Checked
llm-driven-proof-search#238and#231directly: neither has any implementation started (no matching branch, norl_transition/proofsearch.rl_transitionreferences in the tree).#238's JSON shape is currently only a proposal in its issue body, not shipped code, and it explicitly depends on#231(persisting real reward/terminated/truncated/observation values) which is also untouched. There is no real transition data to validate the consumer side against yet.Deliberately deferred rather than guessed at: Parquet native-column export and dataset-card/aggregate-stat generation (both in this issue's scope) — building those now would mean designing against a shape
#238hasn't committed to. Full status and rationale:docs/rl-transitions.md.Next step is on the
llm-driven-proof-searchside:#231then#238. Once real bundles exist,tools/export_rl_transitions.pyshould work against them unmodified (or with a minor schema bump if the shipped shape differs slightly from what's modeled here).seed(queues): populate corpus queues with concrete next-packet candid…
Frontier/erdos dossier work: correct #470's "immediate win" framing
feat(schema): add rl_transition record type and exporter (#9), blocke…