GreenCert: Signed-Response Verification of Neural Training Trajectories

We introduce GreenCert, a matrix-free verifier for certifying neural-network training trajectories over thousands of optimizer updates from a fixed checkpoint. GreenCert propagates the signed response to a proposed path’s one-step defects, preserving cancellation before bounding the remaining nonlinear error. We derive a self-consistency condition guaranteeing an enclosure of the exact-real optimizer trajectory. Output-margin bounds then certify persistent-event times, later reversals, or the absence of a target within the verified window on a fixed evaluation set. When the required conditions cannot be established, GreenCert abstains. The verifier uses explicit derivative and arithmetic-error bounds, together with an ideal-Gaussian assumption for randomized operator estimates. On classification and modular-arithmetic tasks, the signed construction closes in cases where its matched unsigned counterpart fails. In the tested small-network long-window studies, GreenCert completes full-trajectory guarantees within budgets exhausted by the sequential comparators. The cost advantage depends on the problem and horizon: direct continuation remains cheaper on the larger digits task through 1,024 updates. In a separate short-window experiment, GreenCert certifies a persistent-event onset to a single optimizer update in a million-parameter LayerNorm Transformer, matching the onset subsequently observed in a separately executed float64 continuation.