Skip to content

S5-VERIFICATION-RUNBOOK.adoc

Latest commit

 

History

History
144 lines (108 loc) · 3.97 KB

S5-VERIFICATION-RUNBOOK.adoc

File metadata and controls

144 lines (108 loc) · 3.97 KB
Raw

S5 Verification Runbook: Trained-Weights Verification Flow

Purpose

This runbook proves end-to-end that once just train-cpu produces real weights in models/neural/, (a) the Julia GNN server picks them up and stops using cosine similarity, (b) the Rust backends that call gnn_augment_tactics receive model-derived scores via the /gnn/rank wire format, and (c) MRR on a held-out validation split can be measured and compared against the 0.66 cosine baseline. Steps 1 and 2 can run before training has finished; only Step 3 requires weights.

Prerequisite

just train-cpu (or just train on GPU) has completed and models/neural/gnn_ranker/ (or best_model/ or final_model/) exists.

Step 1 — Confirm wire format (no training needed)

cargo test --test gnn_augment_integration

Spawns an in-process mock HTTP server and asserts:

  • GnnClient::health_status() returns the richer payload (model_path, vocab_size, training_records_received).

  • For every backend in ProverKind whose suggest_tactics is wired through gnn_augment_tactics (S5 pilot 5 + Tier-1 extension 5
    Tier-1 finisher 2 + Tier-2 sweep 33 + Tier-3/niche sweep 53 — full coverage as of 2026-05-30): suggest_tactics returns Tactic::Custom { command: "apply", args: ["lemma_foo"] } as the first tactic, proving the /gnn/rank wire format is consumed correctly by every backend.

Expected output: test result: ok. N passed; 0 failed where N is 1 (health) + |gnn_augment_tactics call-sites|. The exact count tracks the test functions in tests/gnn_augment_integration.rs; do not hardcode it in new docs.

Step 2 — Confirm model load

Start the Julia GNN server:

julia --project=src/julia src/julia/api_server.jl

(or however you normally start it — check src/julia/run_server.jl for args). Then query health:

curl -s http://localhost:8090/gnn/health | jq .

Expected response when weights are loaded:

{
  "status": "ok",
  "gnn_model_loaded": true,
  "model_path": "/absolute/path/to/models/neural/gnn_ranker",
  "vocab_size": <non-zero>,
  "training_records_received": 0,
  "num_gnn_layers": 4,
  "service": "echidna-gnn",
  "version": "2.1.0"
}

gnn_model_loaded: true and vocab_size > 0 confirm the server picked up real weights and is no longer falling back to cosine similarity.

Step 3 — Measure lift

just eval

Loads the trained model, runs compute_metrics on the held-out validation split (20% of training_data/), and appends one JSONL row to training_data/eval_results.jsonl. Read the result:

tail -1 training_data/eval_results.jsonl | jq '{mrr, top1, top5, top10, val_size}'

Acceptance

Result Action

MRR ≥ 0.66

Baseline met. Log the row. Run just train on GPU for full training.

MRR < 0.66

STOP. File a bug. Do not paper over it — this signals architecture mismatch, label leakage, or vocabulary miss.

Troubleshooting

Symptom Check

gnn_model_loaded: false after just train-cpu

Confirm models/neural/gnn_ranker/ exists and contains model.bson, vocabulary.bson, config.bson. Restart the Julia server.

Integration test fails on connection refused

Re-run: cargo test --test gnn_augment_integration. The mock binds 127.0.0.1:0; transient OS port exhaustion is extremely rare but retry once.

just eval errors with No trained model found

Run just train-cpu first.

just eval errors on a missing solver method

File a bug in the EchidnaML Julia module. Do not patch the eval script to bypass.

MRR unchanged from 0.66 after training

Check models/model_metadata.txt — if it still reads 0 words, 0 classes the training run did not write weights. Check training logs.