M4 · Verification
Certified within stated limits; unresolved properties retained
Current package
ITER version 2 is packaged beside the original model, with fresh operating-box, local-state, calibration and integrity evidence. 12 states proved, three unknown and five outside domain under the actual local-robustness toleranceC-326. Finite bounds do not establish full local robustness, and M5 keeps version 1. The served output envelope and bare-network bounds have different scopes. The owner grants certification within the stated limits under OQ-52. The table below retains the historical v1 review.
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. OQ-52 records the owner’s scoped certification. The earlier request for further transport-bound work remains part of the review history; unresolved properties are not certified as proved.
Current review package
The four verification records, guard integration and CI re-proof are assembled for owner review. Available output certificates apply only inside exact proof boxes (all four verified input boxes match the previous loaders; 48 of 48 retained pedestal states keep identical predictions and decisions; none of the 57 EC states is inside the exact proof boxes, so no EC certificate-based output check applies thereC-284). The owner adopted the revised report-only fallback alert policy under OQ-50; it changes no inference decisions or physical guard tolerances. The bounded transport investigation remains scientifically unresolved after complete-box partitioning and reserved final-objective optimization (both member-zero pilots retain overflowing physical enclosures despite complete input-box coverage; no sampled overflow witness was found, and all forty transport V5 results remain unresolvedC-293, both full-box pilots retain nonfinite physical enclosures after all final objectives run; independent graph, constraint and corrected-dual replay passes, with no finite physical candidateC-297). No ensemble sweep follows. Transport local robustness, EC complete local boxes and the MAST-U reference remain limitations. Historical ITER and fixed-equilibrium EC comparisons retain their original scope. Passing software checks (1095 tests pass with two intentional heavy-proof skips in each full normal and Tier-A-only suite; lint, typing and quick verification also passC-294) do not grant certification.
Earlier progress and retained evidence
| 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); the MAST-U reference comparison is not evaluable and MAST-U certification scope is limited accordingly (OQ-42) |
| transport monotonicity | all 20 members of each ensemble pass both heat-flux monotonicity properties, with derivative lower bound zero over the full training boxC-247 |
| output bounds | EC and pedestal bounded (all five EC members have finite CROWN bounds for both launcher families; current and width bounds remain very looseC-262, all nine pedestal pressure and half-width pairs have finite bounds over the recorded ITER trajectory box, with the widening and domain clipping statedC-263); transport remains unresolved after independently audited partition and reserved-final-objective pilots (both member-zero pilots retain overflowing physical enclosures despite complete input-box coverage; no sampled overflow witness was found, and all forty transport V5 results remain unresolvedC-293, both full-box pilots retain nonfinite physical enclosures after all final objectives run; independent graph, constraint and corrected-dual replay passes, with no finite physical candidateC-297) |
| local robustness | EC local boxes all out of domain (all 57 complete EC local boxes are out of domain, including all 45 served states; zero robustness proofs or model counterexamples are claimedC-276), retained as the OQ-45 limitation; transport depends on V5 |
| conformal calibration | completed (90% intervals calibrated on the v1 validation split cover 0.887–0.907 on the v1 test and v2-random splits (6 outputs, ITER and MAST-U); 9 of 12 lie in the 0.893–0.907 range expected for exchangeable data, the other three miss it by at most 0.006C-256, 90% intervals calibrated on 190 guard-accepted validation states (4 runs) cover 0.876–0.978 of 548 served test states (8 runs); all six outputs lie within or above the 0.856–0.938 range expected for exchangeable data; per-run coverage 0.78–1.00C-258); loop-state limitations retained |
| EC trajectory comparison | completed within the fixed-equilibrium convention (40/40 cases pass the unchanged 10% power and signed-current limits, including 31/31 served states; maximum current error 9.606% EL and 7.393% UL, maximum power error 0.07483% EL and 0.02599% ULC-281); K-028 remains |
| certificate-bound guards, per-surrogate reports and cheap CI re-proofs | implemented and checked; expensive unresolved properties remain separate |
| certification review | owner-approved within stated limits (OQ-52) |
Historical position (26 Oct 2026). The MAST-U remediation stopped at its reference step: no admissible TGLF reference trajectory exists for comparing the retrained candidate, and the projected reference of OQ-38 cannot complete on this scenario (150 negative raw heat diffusivities at 19 faces; 46 would reach the 1 gB stop, at 31 of 40 states, the first at state 1C-240). The owner limited the MAST-U scope (OQ-42, entry 70): MAST-U will be presented for certification with that limitation stated, and ITER’s pass stands. The remaining work is transport output bounds, local robustness, the EC closed-loop comparison, certificate-bound guards with a fallback-rate check, the per-surrogate reports, CI re-proofs, and then the certification review. The paragraphs below record the remediation in order.
The alpha-CROWN follow-up tightens the training-space intervals but still cannot supply finite physical transport bounds. Its full domains and weights match the first run; the splitting budgets differ. See the technical account.
The separate direct-ELU proof pilot also leaves both selected members unknown (member 0 of each ensemble remains unknown; both processes complete in about 23 seconds, with physical inverse-transform overflow and looser intervals than the earlier optimized runC-268); its focused checks pass (40 focused checks pass in both normal and Tier A modes; lint, formatting and typing passC-269). It was not expanded to the other members. V5 remains open.
Optimizing the direct-ELU tangents tightens those two members’ intervals but still leaves their physical bounds unknown (both selected members remain unknown despite interval-width reductions of about 30–275 times against the same-graph fixed-tangent baseline; physical inverse-transform overflow persistsC-272). The new diagnostics point to intermediate interval growth; focused validation is 50 focused checks pass normally and with Tier B disabled; repository lint, formatting and typing of all 91 source modules passC-273. A further member-level experiment needs tighter intermediate intervals before any ensemble expansion.
The intermediate-range pilot also leaves physical transport bounds unknown (both selected transport members remain physically unknown; largest baseline activation widths fall to 0.246 and 0.449 of the preceding pilot, but inverse signed-log overflow persistsC-274). EC recordings now retain exact state features (30 upper-launcher states (29 served) and 27 equatorial-launcher states (16 served) retain exact features, profiles, outputs, model identity, configurations and guard decisionsC-275), but every prescribed local box leaves the training domain (all 57 complete EC local boxes are out of domain, including all 45 served states; zero robustness proofs or model counterexamples are claimedC-276). K-034 and the adopted OQ-45 scope preserve that limitation; no box was clipped. Focused validation is 70 focused checks pass normally and with Tier B disabled; lint, formatting and typing of all 92 source modules passC-277.
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 remain unresolved; OQ-32 selects retaining the nonnegative contract while investigating. Formal candidate acceptance remains not evaluable.
The read-only conversion review narrows the sign diagnosis (the final electron heat flux is inferred as -0.001689376033 gB; all 9 negative channel records at 8 accepted states have outward-decreasing temperature and no denominator-epsilon sign reversal, with maximum epsilon ratio 1.03e-11; all negative magnitudes are below 1 gBC-195) and passes its numerical/synthetic checks (33 focused checks pass in each mode, including 14 new sign/units/history tests; all 80 native heat-converter round trips meet the mixed 1e-12 parity criterion (maximum absolute difference 8.88e-16 m²/s), 32 numerical source files match the diagnostic bindings, and all 78 source modules pass typingC-196). Its inferred fluxes are not independent solver observations. The richer native diagnostic route passes preparation checks (55 focused checks pass in each mode, including 22 direct-output and settings checks; all 79 source modules pass typing; the compiled synthetic writer preserves signed species heat and passes total/low-k spectral parity without calling TGLFC-197); OQ-33 authorizes bounded runs shorter than six hours. Direct evidence and reference admissibility remain separate. Current model/guard and K-030 remain selected. OQ-17 selects MIT for original toolkit code/documentation; repository privacy remains in force.
See entry 42 and entry 43, entry 44, and technical verification.
The complete richer collection is retained despite its terminal tracking failure (648 integrity checks pass on the complete 15-state collection; all affected signed states agree between backends, but four control states fail the existing parity criterion; original terminal tracking failure is preserved and archive recovery calls no solverC-199). OQ-34 approves a signed reference specification and staged verification. Numerical repeatability tooling passes synthetic checks (31 synthetic diagnostic tests pass in each mode, including archive identity and repeatability completeness/discrepancy checks; 33 unchanged focused records are retained, giving 64 focused recorded passes per modeC-200); reference admissibility and a stable energy closure remain unresolved. K-030 stays open; no surrogate or guard replacement is adopted.
The bounded repeatability collection is complete (521 saved-output checks pass; every within-backend fresh-process repeat is exactly equal and agrees with its consumed output, while all four cross-backend discrepancies persist; native accounting completes within the reviewed bound and the offline archive copy matches its checksumC-201): both backends reproduce their own outputs exactly, while prior cross-backend discrepancies persist. Review numerical convergence and a conservative stable energy closure next. The current model/guard and K-030 remain unchanged.
Bounded numerical refinement is complete and audited (2076 integrity checks pass on the complete bounded study; baseline reproduction, signed species outputs, spectral accounting, native completion and the local archive copy are verified, while electron-flux signs change across refinement levels and finest-level backend differences remainC-203), but the reference remains unconverged: heat-flux signs change across levels and finest-level backend differences persist. Isolate width-search basis from final basis before a reference closure or candidate acceptance decision. Preparation checks pass (40 focused synthetic checks pass in each mode after the input-path correction, covering signed channels, refinement identities, baseline drift, incomplete evidence and existing diagnostic output handlingC-202); earlier failed attempts remain recorded.
The separated-basis diagnostic is complete and audited (2139 integrity checks pass on the complete 54-pair basis grid and all 36 consumed-control comparisons reproduce the preceding study; electron flux changes sign at every state, steps reach 4.28 gB along the final basis and 4.11 gB along the search basis, and at the largest final basis the flux is a residual of order 1e-3 gBC-205). Both the width-search and final-solve basis change the flux, and they interact. At the largest final basis the flux is a residual of order 1e-3 gB; the width search often stops at its upper bound. Convergence is still not established.
The basis and width-range extension is complete and audited (3029 integrity checks pass on the complete 78-pair extension and all 36 control comparisons reproduce job 2687308; NBASIS_MAX 16 still moves electron flux by up to 0.48 gB per step, and widening the width search from 1.65 to 3.3 changes it from about 1e-3 gB to as much as 181 gBC-206). A larger final basis does not settle the flux, and widening the width search changes it by orders of magnitude; the standard settings act as a convention (K-032). OQ-38 selects the standard-settings projected-reference convention. That attempt is consumed and stopped at its approved limit (the projected-reference job failed after 108 s when the log reported 3.93119 gB against the 1 gB stop limit; no completed reference was savedC-217). The review fixes lost stop diagnostics and tightens future acceptance checks. There is no completed reference, so R6/R7 and K-030 remain open. OQ-42 then limited the MAST-U scope, as recorded above.