Skip to content

docs(training-run): record 2026-06-02 first-GNN-run results (MRR 0.92) #212

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 2, 2026
Merged

docs(training-run): record 2026-06-02 first-GNN-run results (MRR 0.92) #212

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
72 changes: 56 additions & 16 deletions docs/training-runs/2026-06-02.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,44 +48,84 @@ PR landed (#207, merged 2026-06-02T04:14:04Z).

### Stage 3 — train-from-corpus lean

- _TBD_ — first run blocked on Julia `JSON` dep (fixed in #210); awaiting v3 run completion.
- Wall-clock target: ~10min CPU baseline / ~2hr GPU on small corpus
- _2026-06-02T10:48:06Z → 13:11:14Z_ (~2hr 23min wall-clock)
- 16 epochs, early stopping triggered
- Loss trajectory from log:
- train_loss: 1.76 → 1.04 (epoch 5) → 0.85 (epoch 15)
- val_loss: 1.62 → 1.34 (epoch 5) → 1.33 (epoch 16, plateau)
- Checkpoints saved at epochs 5, 10, 15 (`models/neural/checkpoint_epoch_{5,10,15}/`)
- `best_model/` saved at 11:55 (lean-side best)
- Per-epoch MRR not recorded for lean run (training_metrics.csv was overwritten by coq)

### Stage 4 — train-from-corpus coq

- _TBD_
- _2026-06-02T13:11:14Z → 13:45:39Z_ (~34min wall-clock)
- 17 epochs, early stopping triggered
- Real per-epoch metrics from `models/neural/training_metrics.csv`:

| Epoch | train_loss | val_loss | MRR | recall@10 | precision@10 |
|---|---|---|---|---|---|
| 1 | 1.887 | 1.610 | 0.794 | 0.821 | 0.177 |
| 5 | 1.118 | 1.100 | 0.862 | 0.833 | 0.185 |
| 9 | **0.969** | 1.007 | **0.923** | 0.859 | 0.192 |
| 12 | 0.861 | **0.983** | 0.785 | 0.808 | 0.177 |
| 17 | 0.876 | 1.146 | 0.862 | 0.827 | 0.185 |

- **Best MRR: 0.92 @ epoch 9** (val_loss 1.01)
- **Best val_loss: 0.98 @ epoch 12** (MRR 0.79)
- `final_model/` saved at 14:11
- `gnn_ranker/` (production-deployable) at 14:45

### Stage 5 — artefacts

- _TBD_ — should populate `models/neural/`. Existing `models/neural/` in the local checkout's wave3 worktree has prior weights; this run uses the dedicated branch worktree so artefacts don't pollute main.
`models/neural/` contents (952MB total):

| Artefact | Created | model.bson size |
|---|---|---|
| `best_model/` | 11:55 (lean) | ~155MB |
| `checkpoint_epoch_5/` | 12:23 | 155MB |
| `checkpoint_epoch_10/` | 12:38 | 155MB |
| `checkpoint_epoch_15/` | 14:09 | 155MB |
| `final_model/` | 14:11 (coq) | ~155MB |
| **`gnn_ranker/`** | 14:45 | **162MB** ← production-deployable |
| `training_metrics.csv` | 14:45 | 3.3KB |

## Outcomes summary

- **Models produced**: _TBD_
- **MRR vs cosine baseline**: _TBD_
- **Comparable to wave3 baseline**: _TBD — needs side-by-side once wave3 lands its first GNN run_
- **Models produced**: ✅ 6 model directories + 1 metrics CSV (952MB total)
- **Best MRR**: 0.92 (epoch 9, coq) — solidly above the cosine baseline of 0.66 the eval script's MRR gate requires
- **Best val_loss**: 0.98 (epoch 12, coq)
- **Comparable to wave3 baseline**: pending — wave3's first GNN run hasn't landed yet; this run's artefacts are on dedicated branch `gnn-training-run-2026-06-02` (no main pollution)
- **Production ranker**: `gnn_ranker/model.bson` (162MB) — picked up by `src/rust/gnn/client.rs::cosine_fallback` once placed in the canonical `models/neural/` location

## Known issues discovered this run

1. **JSON dep mismatch** — fixed via #210. `corpus_loader.jl` uses `JSON.parse` but `Project.toml` had only `JSON3`.
2. **`CUDA.version()` MethodError** — cosmetic logging error; CUDA.jl 5.x removed the method. Fixed via this PR.
3. **`corpus-ingest-saturation` 4-vs-17 gap** — known; tracked separately.
2. **`CUDA.version()` MethodError** — fixed via #211. CUDA.jl 5.x removed the method; replaced with `runtime_version()` / `driver_version()` defensively wrapped.
3. **`corpus-ingest-saturation` 4-vs-17 gap** — Stage 2 ingested 4/17 adapters (agda/coq/lean/idris2). 13 missing adapters have Rust extractor modules at `src/rust/corpus/<name>.rs` but were not wired into the CLI dispatcher at `src/rust/main.rs:1177`. Dispatcher fix prepared on branch `feat/corpus-dispatcher-all-17-adapters` but blocked by an SPDX-FileCopyrightText pre-commit hook on `main.rs` (Owner = "ECHIDNA Project Team" instead of canonical "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"). Owner-action: manually fix the Owner header to unblock.
4. **`BSON not defined in Main` LoadError** at final-save path — non-fatal: checkpoint scaffold saved 155MB `model.bson` per checkpoint regardless. Final-save call needs a `using BSON` somewhere in the JSONL-fallback training path (separate from the checkpoint-save path which already had `using BSON`).
5. **`training_data/<adapter>/` was empty when launcher ran ingest** — the launcher pointed at fresh-created empty dirs instead of `external_corpora/<upstream>/`. The pipeline still produced real training because train.jl has a JSONL-fallback path that found the pre-existing `training_data/proof_states_UNIFIED.jsonl` + `premises_*.jsonl` from wave3 work. Real Corpus JSON adapter input was bypassed entirely.
6. **`per-epoch metrics overwrite`** — lean run's training_metrics.csv was overwritten by coq run. Per-prover output dirs needed.

## Follow-up tickets
## Follow-up tickets / PRs

- (TBD if needed) Extend `corpus-ingest-saturation` recipe to all 17 adapters — large scope, requires per-adapter Rust extractor scripts.
- (TBD) Compare `models/neural/` outputs vs wave3 baseline once both land.
- **echidna dispatcher fix** — branch `feat/corpus-dispatcher-all-17-adapters` ready to PR once Owner header unblocked.
- **BSON `using` fix** — small one-line fix at the failing final-save path.
- **Launcher path correction** — per-adapter upstream-source mapping (agda ← agda-stdlib/agda-unimath/agda-cubical; coq ← mathcomp + coq-contribs; lean ← mathlib4; idris2 ← idris2).
- **Per-prover metrics dirs** — separate `training_metrics_lean.csv` / `training_metrics_coq.csv` to avoid overwrite.
- Compare `models/neural/` outputs vs wave3 baseline once wave3's first GNN run lands.

## Re-running

Owner-side re-run after corpus refresh:
Owner-side re-run (after dispatcher fix lands):
```bash
just provision-corpora extract-corpora
just provision-corpora # idempotent; ~18s if cached
just extract-corpora # SEPARATE call — not a positional arg
for adapter in agda coq lean idris2; do
just corpus-ingest-saturation "$adapter" "training_data/$adapter/"
just corpus-ingest-saturation "$adapter" "external_corpora/<upstream-root-for-$adapter>/"
done
just train-from-corpus lean
just train-from-corpus coq
```

Note `extract-corpora` is a *separate* recipe call — not a positional arg to `provision-corpora` (that was an early-run mistake; cost 1 launcher iteration).
Note `extract-corpora` is a separate recipe call — not a positional arg to `provision-corpora` (that was the early-run mistake; cost 1 launcher iteration).
Loading