Goal 6 — Equivalence learning grid (gate G6)

[duckyquang]

The discriminative foundation: can a GNN learn E₁ ≡ E₂, and under which representation?

Sub-goals

• 6.0 ML dependency decision (PyTorch + PyG, [ml] extra); training-reproducibility policy (pinned deps, seeds, run metadata)
• 6.1 Trace-rich equivalence-pair dataset: e-graph positives with rule-sequence provenance + step-distance, size-matched hard negatives, tiered verification, group splits, depth-OOD + family-OOD sets (≥50k/5k/5k pairs — this is the Goal 7/8 fuel)
• 6.2 Graph materialization: AST-DAG, pure EML-DAG, motif-EML (train-mined vocab), motif-AST (fair-compression control) as PyG dataset builders + encoding contract
• 6.3 Reusable backbones: GIN encoder (node-type-as-feature, virtual node for depth; Siamese GIN is a candidate architecture), compute-matched prefix transformer, trivial op-count baseline
• 6.4 Training harness: YAML configs, early stopping, 3 seeds/cell, CPU smoke test in CI (train_equiv.py / eval_equiv.py)
• 6.5 Baseline grid: 6 arms × metrics (acc, F1, both OODs, sample efficiency, time, memory, α)
• 6.6 Analysis: accuracy-vs-α curve, graph-benefit vs EML-benefit separation, honest report (GOAL6_SUMMARY.md)
• 6R Reserved repair pass

Gate G6

All GNN arms beat the trivial baseline (else stop and fix the dataset); the EML-vs-AST verdict is recorded either way. If pure EML-DAG loses decisively on OOD, later goals proceed with the EML claim narrowed — the verifier-guided pipeline is representation-agnostic and survives.