Repository navigation
feat(metrics): add multi-model empirical difficulty and native analytics exports #5
Description
Problem
level and difficulty_bin are primarily author-assigned, and the authoring tool defaults unspecified packets to D0. MathCorpus does not yet preserve multi-model pass rates, attempts, tokens, cost, verifier time, or failure distributions as standardized evidence. Nested enrichment data is also hidden inside packet_json in Parquet exports.
Scope
Add ModelRun and EmpiricalDifficultyAggregate records with:
- evaluation-suite and policy versions
- model family/version/config hash
- episode count and seeds
- first-attempt and eventual pass rates
- attempts-to-pass distribution
- tokens, cost, wall time, and Lean CPU time
- failure-category distribution
- observed difficulty score and calibrated bin
Keep author-assigned and empirically observed difficulty separate.
Acceptance criteria
- Aggregates are reproducible from referenced model-run records.
- Multiple suites and historical aggregates can coexist.
- Missing or censored model metadata is represented honestly.
- Parquet/JSONL exports expose major fields as native columns, not only nested JSON.
- Corpus-level reports summarize proof classes, dependency depth, negative counts, and model performance.
- Existing packet difficulty is never silently overwritten by observed difficulty.
Activity
Mnehmos commentedon Jul 12, 2026
Implemented (local commit
ed2e1a7, stacked onb3bfa63/bcdb683/8c74201/7f1ac10— not yet pushed, see notes on #1-#4):packet.schema.jsongainsmodel_runs[]/empirical_difficulty_aggregates[], mirroring MCIP'sModelRun/EmpiricalDifficultyAggregatefrom feat(schema): define MathCorpus Interchange Protocol v1 for Proof Search enrichment #1, strictly additive to the top-level author-assigneddifficulty_bin— no code path in this repo writes to that field from empirical data.tools/mathcorpus/difficulty.pyimplements a versioned formula (calibration_version: "v1":1 -meaneventual_pass_rateacross referenced runs → fixed-threshold bin).policy.check_empirical_difficulty_aggregatesrecomputes bothobserved_difficulty_scoreandcalibrated_difficulty_binfrom the packet's ownmodel_runsand rejects a mismatch. A future recalibration gets a new version rather than silently changing what an existing stored score means.model_run.censored_fields[]names fields whose true value is known but deliberately withheld — distinct fromnull("not collected").empirical_difficulty_aggregatesis an array; an exact-duplicate(suite, policy, calibration_version, model_run_ids)signature is flagged as a warning, not blocked.author_difficulty_binon an aggregate is only ever an echo for comparison; a mismatch against the packet's currentdifficulty_binis a warning ("expected for a historical aggregate"), never a write.tools/mathcorpus/aggregates.py(proof-class distribution, dependency transitive depth, negative counts, per-model-family episode-weighted pass rate) used by bothbuild_manifests.py(refactored, removing the duplicate logic feat(schema): standardize dependency manifests and retrieval evidence #3 had added) and an extendedcorpus_stats.py, so the two reporting surfaces agree.packet_json:tools/export_parquet.pynow hoists 9 enrichment summaries (proof_variant_count,canonical_proof_class,dependency_transitive_depth,attempt_count,attempt_failed_count,negative_example_count,model_run_count,best_eventual_pass_rate,observed_difficulty_bin) into native columns — the issue's specific complaint._flatten()logic verified directly against the real 303-row public export since pyarrow isn't installed in this environment. JSONL was already fine (each row is a full nested JSON object); no change needed there.packets/_fixtures/model_performance_conformance.v1.json(kind: concept,training.eligibility: private_audit_only) demonstrates the schema with two illustrative models and a genuinely recomputed (not hand-picked) aggregate; confirmed excluded from every export lane by grepping a full export run.This closes out the "embed MCIP shapes into packet.schema.json" arc from #1 (#2-#5). Tracked in
agents/github_issues/DONE.md,FEATURES.md,HANDOFF.md.feat(metrics): add multi-model empirical difficulty and native analyt…
feat(import): add MCIP importer, packet enrichment workflow, and back…