From 75c6a053a04f86ca2d9e521c28f6283d3acad0cc Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Thu, 13 Aug 2026 19:10:55 +0200 Subject: [PATCH] fix(contracts): main is red on a property that is false for small-variance input MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `workspace-test` failed on main at 9b19970db: Test failed: output variance = 0.99547684, expected ~1.0 minimal failing input: v = [-4.983007, -4.9585605, -4.9680285, -5.0763197] Not a layernorm defect, and not introduced by the audit batches — the file was last touched by #1545 and none of #2453/#2454/#2457/#2458 changed a line of it. The arithmetic is exactly right: LayerNorm divides by sqrt(var_in + eps), so var_out = var_in / (var_in + eps) var_in for that input = 2.2e-3, eps = 1e-5 2.2e-3 / 2.21e-3 = 0.99548 <- the observed value, to 5 digits So var_out approaches 1.0 only as var_in grows large relative to eps, and is BELOW 1.0 for every finite input. The property "output variance is ~1.0 within 1e-3" is simply FALSE once var_in drops near eps. The test was asserting something untrue and had been waiting for proptest to draw the input that says so. WHY THE EXISTING GUARD MISSED IT. There was one — it skipped vectors whose RANGE was under 1e-6. Range is a proxy for the wrong quantity. The failing input had range 0.12, five orders of magnitude above that guard, while its variance was only ~220x eps. A guard on a proxy is how a latent flake survives review. FIX: precondition on the quantity that actually governs the error. From |1 - var_in/(var_in + eps)| = eps/(var_in + eps) < TOL => var_in > eps/TOL - eps so `prop_assume!(var_in > EPS / TOL)`. EPS and TOL are now named constants used by the kernel call, the precondition and the assertion, so changing either cannot silently re-open the gap — the old code had 1e-5 and 1e-3 as unrelated literals. VERIFIED: - 20 consecutive runs at PROPTEST_CASES=512 (10,240 cases): 0 failures. - NOT vacuous, which is the risk a prop_assume introduces. Mutating the kernel (denominator scaled by 0.9) turns it RED — "output variance = 0.8099979, expected ~1.0 (input variance 3.8552012)" — and restoring turns it GREEN. The precondition filters the regime where the property is false, not the inputs that would catch a bug. - The failure message now prints var_in too, so the next person sees immediately which regime they are in. Refs #2373 --- .../src/kernels/layernorm.rs | 34 ++++++++++++++----- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/crates/aprender-contracts/src/kernels/layernorm.rs b/crates/aprender-contracts/src/kernels/layernorm.rs index 0187a28c14..dedbae3247 100644 --- a/crates/aprender-contracts/src/kernels/layernorm.rs +++ b/crates/aprender-contracts/src/kernels/layernorm.rs @@ -256,24 +256,40 @@ mod tests { fn prop_layernorm_unit_variance( v in proptest::collection::vec(-10.0_f32..10.0, 4..64) ) { - // Check that not all elements are the same (skip constant vectors) - let min = v.iter().copied().fold(f32::INFINITY, f32::min); - let max = v.iter().copied().fold(f32::NEG_INFINITY, f32::max); - if (max - min).abs() < 1e-6 { - return Ok(()); - } + // LayerNorm divides by sqrt(var_in + eps), so the output variance is + // exactly var_in / (var_in + eps) — it approaches 1.0 only as var_in + // grows large relative to eps, and is BELOW 1.0 for every finite input. + // + // The old guard skipped vectors whose RANGE was under 1e-6, but range is + // a proxy for the wrong quantity. proptest found + // v = [-4.983007, -4.9585605, -4.9680285, -5.0763197]: range 0.12, far + // above that guard, but var_in = 2.2e-3, only ~220x eps. Output variance + // came out 0.99547684 and the 1e-3 assertion failed. That is arithmetic + // working correctly, not a layernorm defect — the PROPERTY is false in + // that regime, so the test was asserting something untrue. + // + // Precondition on the quantity that actually governs the error. From + // |1 - var_in/(var_in + eps)| = eps/(var_in + eps) < TOL, the property + // holds when var_in > eps/TOL - eps. Derived from EPS and TOL rather + // than hardcoded, so changing either cannot silently re-open the gap. + const EPS: f32 = 1e-5; + const TOL: f32 = 1e-3; + let n_in = v.len() as f32; + let mean_in: f32 = v.iter().sum::() / n_in; + let var_in: f32 = v.iter().map(|&x| (x - mean_in) * (x - mean_in)).sum::() / n_in; + prop_assume!(var_in > EPS / TOL); let gamma = vec![1.0_f32; v.len()]; let beta = vec![0.0_f32; v.len()]; let mut output = vec![0.0_f32; v.len()]; - layernorm_scalar(&v, &gamma, &beta, 1e-5, &mut output); + layernorm_scalar(&v, &gamma, &beta, EPS, &mut output); let n = output.len() as f32; let mean: f32 = output.iter().sum::() / n; let var: f32 = output.iter().map(|&x| (x - mean) * (x - mean)).sum::() / n; prop_assert!( - (var - 1.0).abs() < 1e-3, - "output variance = {var}, expected ~1.0" + (var - 1.0).abs() < TOL, + "output variance = {var}, expected ~1.0 (input variance {var_in})" ); }