M4 · Verification
In progress
Goal and gate
Prove the owner-selected properties over explicit input boxes, calibrate uncertainty intervals, compare coupled trajectories against Tier A physics and bind the guards to the certificates. The brief requires CI to re-prove properties on surrogate changes. The owner certification review is the human gate; it has not occurred.
Progress
| task | state |
|---|---|
| model storage and verification tooling | approved: committed model candidates/boxes (OQ-23), auto_LiRPA/input splitting (OQ-24) |
| PyTorch export | 13 export checks pass in each mode: all selected members, random box points, local holdouts, physical transforms and served means, with rtol=1e-12 and atol=1e-12 in each declared output unitC-180; numerical parity is not a formal certificate |
| property contracts | six property contracts load; 14 property-validation tests pass in each mode, including malformed-domain, tolerance and output-schema rejectionC-177 |
| transport closed-loop comparison | ITER passes (served-face T_e 7.42%, T_i 8.18%, both passing the 15% limit; whole profile 7.72/9.23%; 34 of 51 final-state faces servedC-178); MAST-U fails (served-face T_e 35.33%, T_i 49.15%, both failing 15%; whole profile 41.51/62.39%; cells with both adjacent faces served give 11.86/23.24%, still failing T_i; 13 of 26 final-state faces servedC-179, K-030) |
| formal proofs, output bounds and local robustness | pending |
| conformal calibration and EC trajectory comparison | pending |
| certificate-bound guards, per-surrogate reports and CI re-proofs | pending |
| certification review | pending |
The transport comparison uses final-state served faces with both temperature profiles interpolated onto the same coordinates. It also reports whole-profile errors and cells with both adjacent faces served. The final-state mask is not trajectory fallback accounting. The owner prioritizes MAST-U remediation before further proofs and calibration (OQ-25). Matched probes and an exact accepted-state replay diagnose flux errors and coefficient rejections (all 17 in-domain final-state probes succeed; on 12 served faces with reference flux above 1 gB, median relative errors are 41.17% Q_e and 74.27% Q_i; an unconstrained v3 control gives 38.05/71.88%C-181, all saved temperature, density and psi values are reproduced exactly; four final inner faces exceed the existing ion-diffusivity guard bound; 44.81% of accepted-state face diagnostics reject the surrogateC-182). A training-only label refresh is complete under the approved compute request (OQ-27); eight local checks pass for approved allocation/time, hashes and lineage, full-input alignment, case budget, unique coordinates, training-only equilibria, source model and finite successful labelsC-183. Artifact synchronization is complete with downloaded checksums verified (entry 45). Retraining data/splits, configuration and bounded smoke are prepared (55 focused checks pass in both normal and Tier A modes; the bounded training-only smoke produces finite predictions and reloads exactlyC-185; entry 46). The approved single training job is complete (164 completion checks pass, binding the saved candidate to the reviewed snapshot and frozen data/splits, with finite parameters/history and tested member/served predictionsC-186), and the local offline report retains mixed regressions. Candidate exports pass numerical parity (all 168 export comparison records pass the unchanged mixed tolerance, covering all 20 members in training/physical units, the served ensemble and JAX JIT/eager arithmeticC-187; entry 47). Matched candidate replay tooling is now prepared (40 focused checks pass in normal and Tier A modes; the two-step training-only candidate smoke is finite and reconstructs the raw accepted-state guard predicate exactlyC-188; entry 48), with reference provenance limits recorded. The approved replay is now consumed: solver convergence passes, but reference coverage fails (the single approved replay finishes in 65 seconds within its 240-second bound, with 40 finite converged steps and 146 passing integrity checks; comparison exits with a reference-coverage failure at candidate-served face 4, normalized radius 0.16C-189; entry 49). Fixed-mask diagnostics retain the electron regression (candidate/baseline serve 15/13 faces with 11 overlapping; fixed-baseline-mask candidate T_e/T_i errors are 42.1252%/48.1182%, versus baseline 35.3331%/49.1458%; candidate whole-profile errors are 29.7365%/41.8856%, and own-mask descriptive distances to the hybrid reference are 29.8865%/40.0063%C-190). Reference admissibility, a separately reviewed next experiment and formal proofs remain ahead; K-030 stays open.
Reference diagnostic preparation passes its synthetic smoke and focused checks (32 focused checks pass in each mode; a two-step synthetic training-equilibrium smoke is finite and reconstructs the raw guard exactly; all 77 source modules pass typing, and lint/format plus batch syntax passC-192). The approved diagnostic is consumed: historical profiles/mask reproduce exactly (the diagnostic completes in 517 seconds within its 30-minute bound, with 40 finite converged steps, exact historical temperature/density/poloidal-flux-profile and final-mask equality, and 171 passing saved-output integrity checksC-193), while negative raw heat diffusivity explains the rejected face (final face 4 at normalized radius 0.16 has valid inputs but raw electron heat diffusivity -0.02792124888 m²/s; negative heat diffusivity rejects that face at 8 of 40 accepted states; reference rejection is 323/1040 accepted-state face records (31.0577%)C-194). Its physical/numerical origin and reference remedy need review (OQ-32); formal candidate acceptance remains not evaluable.
See entry 42 and entry 43, entry 44, and technical verification.