spec(ml): hslm_f32_study -- f32 vs f64 HSLM trainer, 2000 steps same seed (Closes #10844)

.trinity/seals/ml_hslm_f32_study.json

@@ -0,0 +1,28 @@
+{
+  "built_by": "t27c-bootstrap@0.5.2+78e57be99",
+  "closure": [],
+  "config": "gen=c,rust,verilog,zig;tests=zig",
+  "gen_hash_c": "sha256:2dfc669619005ad563ecd502ceb862b6f1235f51a2d22d59f925d24742d8feb4",
+  "gen_hash_rust": "sha256:b525433f8059339346abe2b4766fc04b0bdf44a8620944ce53d338d6c0bd5009",
+  "gen_hash_verilog": "sha256:eb290fd2f98f954d3050c9bff4128392b43c76420d0671fbc9001e57fd77b7aa",
+  "gen_hash_zig": "sha256:4d7709d44915678d99b055593da9d8b0e626bc160ac0c362e7edc3e222bc33c3",
+  "module": "hslm_f32_study",
+  "ring": 12,
+  "seal_schema": 2,
+  "sealed_at": "2026-10-19T07:53:53Z",
+  "sealed_by": "t27c-bootstrap@0.5.2",
+  "spec_hash": "sha256:481bfc1291a0fc1aff711920b80b151d3396fcbfa8344fb23666f87fa8a97a93",
+  "spec_path": "specs/ml/hslm_f32_study.t27",
+  "tests": {
+    "failed": 0,
+    "failing": [],
+    "forced": false,
+    "passed": 11,
+    "total": 11,
+    "vacuous": 0
+  },
+  "toolchain": {
+    "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10",
+    "zig": "0.16.0"
+  }
+}

specs/ml/hslm_f32_study.t27

@@ -0,0 +1,318 @@
+// SPDX-License-Identifier: Apache-2.0
+; specs/ml/hslm_f32_study.t27 -- the HSLM trainer in f32 against f64: two runs of the same 2000 steps, their loss
+; curves, speed and memory as constants, and the tests that re-derive the speed-up and the largest curve gap and tie
+; the verdict to its stated threshold. Issue: gHashTag/t27#10844 (epic #10024, own_model cell 25).
+; THE QUESTION (owner, 2026-10-19): f32 instead of f64 -- half the memory and twice the SIMD width -- changes the bits, so
+; it needs a new run and a comparison of loss curves. This file is that comparison. It lands the measurement, not the
+; change: specs/ml/train_hslm.t27 and specs/nn/hslm.t27 are not edited here (two other sessions are changing them).
+; THE METHOD. Both runs were made on the Railway lab, side by side, at the same time, from scratch copies that are not
+; committed. The f64 control is specs/ml/train_hslm.t27 unmodified except that its /tmp/hslm/ paths point to a private
+; directory. The f32 run is the same file, ml::train_hslm, nn::hslm and nn::ternary_ste with the type token f64 replaced by f32
+; (a mechanical sed), plus two hand fixes that keep the resumable-state file in its f64 layout: the f64 reader and writer
+; widen or narrow through an f64 local before the u64 bitcast, and the test-only u64 bitcasts became u32. Both compiled with
+; `t27c compile --backend ml` and zig build-exe -O ReleaseFast, and ran with the same seed 1729, the same TinyStories-V2
+; HTOK token files as the release (train.tok, valid.tok), the release schedule (total 8000, warmup 2000, so lr 0.001 at
+; step 2000), loss_positions 27, 66 windows of 27 tokens per step, and a held-out eval every 100 steps on the same 243
+; windows. 2000 steps each.
+; WHAT STAYED f64: NOTHING. In the f32 run every activation, gradient, kernel, LAMB moment and loss accumulator is f32; no
+; part was kept in f64 because the run did not destabilize (no NaN, gnorm tracks the f64 run, the loss falls the same way).
+; Only the state file's byte layout stays f64, which is a file format, not arithmetic.
+; THE CONTROL IS THE RELEASE. The f64 control reproduces the release log (playra/hslm-t27-2m, /tmp/hslm/run.log) at the
+; four shared eval steps 500, 1000, 1500 and 2000 to every printed digit: train, held-out last position and held-out all 27
+; positions. A test checks the 12 numbers, so the baseline is the release run, not a near copy.
+; THE CURVES, per eval step 0, 100 .. 2000:
+;   train       loss of the last 27 positions of the step's batch (step 0: the first_loss of the done line, 6.6079)
+;   valid       held-out loss at the last position (position 26) of 243 windows
+;   valid_full  held-out loss averaged over all 27 positions of the same windows
+; THE SPEED. tok/s per eval interval as the run printed it, and the overall tok/s of the done line (tokens per second of
+; training time). The lab was loaded (load average about 90 on 48 cores) by other jobs, so the absolute figures are lower
+; and noisier than a quiet machine; the two runs shared the conditions, so the ratio is the fair figure.
+; THE MEMORY. Peak resident set (VmHWM of /proc/PID/status, kB) sampled by hand while both ran, last sampled at about
+; step 1300 (f64) and step 1500 (f32). The arrays are allocated once, so the figure does not move after the first steps.
+; THE VERDICT RULE, stated before the numbers were read: ADOPT iff the largest absolute gap between the two valid_full
+; curves over all 21 evals is at most 0.01 nats (about 1% of perplexity) AND the overall speed-up is at least 1.10. One
+; seed, one run each: a gap above 0.01 is treated as "the bits changed the training", not as noise, because rejecting
+; costs nothing and adopting is a change to the trainer.
+; THE RESULT. The speed-up is 1.1507 (361.2 against 313.9 tok/s) and every one of the 20 intervals is faster in f32, the
+; peak RSS is 0.641 of f64's (79920 against 124676 kB), and the curves coincide to 1e-3 nats until step 1400. The largest
+; valid_full gap is 0.0127 nats at step 1900, inside the lr peak (lr 0.30 at step 1700): the two runs round differently
+; and the chaotic phase of the schedule lets that grow. At the last eval the gap is 0.0059 (5.1755 against 5.1814). The
+; rule gives REJECT: the gap is over the threshold by 0.0027 nats. Read it as "not yet", not as "f32 trains worse": f32 ends
+; 0.0059 above f64 on one seed, and a second seed would show whether that is the precision or the seed. The decision on
+; the trainer is the owner's; no trainer change is proposed by this file.
+; NEGATIVE CONTROL, done on the lab and recorded here: with F32_FULL[19] changed from 5.3134 to 5.3200 the largest gap
+; falls to 0.0075, the verdict derived from the rule becomes ADOPT while VERDICT stays REJECT, and three tests fail:
+; the_largest_curve_gap_is_rederived, verdict_is_tied_to_the_threshold and
+; the_verdict_is_reject_because_the_gap_is_over_by_27_ten_thousandths (8 of 11 pass).
+; phi^2 + 1/phi^2 = 3 | TRINITY
+
+module hslm_f32_study;
+
+; THE EVAL STEPS: 0, 100, ..., 2000 -> index i is step 100 * i
+const EVALS : usize = 21;
+const STEP_STRIDE : usize = 100;
+
+; THE f64 CONTROL (= the release run at the shared steps)
+pub const F64_TRAIN : [21]f64 = [6.6079, 6.5913, 6.5766, 6.5312, 6.4768, 6.4112, 6.3664, 6.3159, 6.2606, 6.2286, 6.1408, 6.1026, 6.0396, 5.9432, 5.8952, 5.8238, 5.7652, 5.5996, 5.4627, 5.3478, 5.2038];
+pub const F64_VALID : [21]f64 = [6.5952, 6.5890, 6.5719, 6.5380, 6.4773, 6.4074, 6.3462, 6.2966, 6.2436, 6.1825, 6.1178, 6.0528, 5.9813, 5.9089, 5.8467, 5.7813, 5.6560, 5.5245, 5.4020, 5.2752, 5.1257];
+pub const F64_FULL : [21]f64 = [6.6073, 6.6001, 6.5780, 6.5382, 6.4781, 6.4200, 6.3698, 6.3239, 6.2721, 6.2163, 6.1570, 6.0964, 6.0344, 5.9731, 5.9118, 5.8280, 5.7281, 5.5806, 5.4579, 5.3261, 5.1755];
+
+; THE f32 RUN
+pub const F32_TRAIN : [21]f64 = [6.6079, 6.5913, 6.5766, 6.5312, 6.4768, 6.4112, 6.3663, 6.3159, 6.2606, 6.2285, 6.1408, 6.1026, 6.0396, 5.9433, 5.8957, 5.8260, 5.7515, 5.5991, 5.4650, 5.3533, 5.2054];
+pub const F32_VALID : [21]f64 = [6.5952, 6.5891, 6.5720, 6.5380, 6.4773, 6.4074, 6.3462, 6.2967, 6.2436, 6.1826, 6.1177, 6.0528, 5.9814, 5.9093, 5.8468, 5.7783, 5.6582, 5.5458, 5.3928, 5.2628, 5.1347];
+pub const F32_FULL : [21]f64 = [6.6072, 6.6001, 6.5780, 6.5382, 6.4781, 6.4200, 6.3698, 6.3239, 6.2721, 6.2163, 6.1571, 6.0964, 6.0343, 5.9731, 5.9119, 5.8291, 5.7206, 5.5850, 5.4545, 5.3134, 5.1814];
+
+; THE RELEASE LOG at steps 500, 1000, 1500, 2000 (index 5, 10, 15, 20): train, valid, valid_full
+pub const REL_TRAIN : [4]f64 = [6.4112, 6.1408, 5.8238, 5.2038];
+pub const REL_VALID : [4]f64 = [6.4074, 6.1178, 5.7813, 5.1257];
+pub const REL_FULL : [4]f64 = [6.4200, 6.1570, 5.8280, 5.1755];
+
+; TOK/S per interval, steps 100 .. 2000 (index j is step 100 * (j + 1)); step 0 has no interval
+pub const F64_TOKS : [20]f64 = [267.7, 327.9, 328.2, 322.9, 312.0, 304.0, 268.4, 295.7, 317.2, 320.1, 321.6, 321.0, 325.7, 325.0, 298.6, 315.9, 321.6, 339.5, 333.9, 335.5];
+pub const F32_TOKS : [20]f64 = [308.3, 380.8, 379.1, 382.4, 372.8, 360.7, 352.2, 314.8, 353.6, 350.8, 375.9, 371.3, 368.2, 368.2, 374.4, 374.4, 359.3, 355.0, 366.7, 377.5];
+
+; THE done LINES: overall tok/s and training seconds
+pub const F64_TOK_S : f64 = 313.9;
+pub const F32_TOK_S : f64 = 361.2;
+pub const F64_TRAIN_S : f64 = 11355.71;
+pub const F32_TRAIN_S : f64 = 9868.00;
+
+; PEAK RSS, VmHWM in kB
+pub const F64_RSS_KB : f64 = 124676.0;
+pub const F32_RSS_KB : f64 = 79920.0;
+
+; THE RULE
+pub const GAP_MAX : f64 = 0.01;
+pub const SPEEDUP_MIN : f64 = 1.10;
+pub const ADOPT : i32 = 1;
+pub const REJECT : i32 = 0;
+pub const VERDICT : i32 = 0;
+
+fn study_step(i: usize) -> usize {
+    return i * STEP_STRIDE;
+}
+
+fn study_speedup() -> f64 {
+    return F32_TOK_S / F64_TOK_S;
+}
+
+; the same ratio from the training seconds of the done lines (tokens are equal, so time f64 / time f32)
+fn study_time_ratio() -> f64 {
+    return F64_TRAIN_S / F32_TRAIN_S;
+}
+
+; |ratio of tok/s - ratio written out| : 361.2 / 313.9 is not typed in twice by accident
+fn study_speedup_error() -> f64 {
+    return abs(study_speedup() - 361.2 / 313.9);
+}
+
+fn study_start_gap_valid() -> f64 {
+    return abs(F32_VALID[0] - F64_VALID[0]);
+}
+
+fn study_start_gap_full() -> f64 {
+    return abs(F32_FULL[0] - F64_FULL[0]);
+}
+
+fn study_start_gap_train() -> f64 {
+    return abs(F32_TRAIN[0] - F64_TRAIN[0]);
+}
+
+fn study_mem_ratio() -> f64 {
+    return F32_RSS_KB / F64_RSS_KB;
+}
+
+; the smallest f32/f64 ratio over the 20 intervals
+fn study_min_interval_speedup() -> f64 {
+    var m : f64 = 1.0e9;
+    var j : usize = 0;
+    while (j < 20) {
+        const r : f64 = F32_TOKS[j] / F64_TOKS[j];
+        if (r < m) {
+            m = r;
+        }
+        j = j + 1;
+    }
+    return m;
+}
+
+; the largest |F32_FULL - F64_FULL| over all evals
+fn study_max_gap() -> f64 {
+    var m : f64 = 0.0;
+    var i : usize = 0;
+    while (i < EVALS) {
+        const g : f64 = abs(F32_FULL[i] - F64_FULL[i]);
+        if (g > m) {
+            m = g;
+        }
+        i = i + 1;
+    }
+    return m;
+}
+
+; the eval index where that gap is largest (first one on a tie)
+fn study_max_gap_at() -> usize {
+    var m : f64 = 0.0;
+    var at : usize = 0;
+    var i : usize = 0;
+    while (i < EVALS) {
+        const g : f64 = abs(F32_FULL[i] - F64_FULL[i]);
+        if (g > m) {
+            m = g;
+            at = i;
+        }
+        i = i + 1;
+    }
+    return at;
+}
+
+; the largest |F32_VALID - F64_VALID|, the last-position curve
+fn study_max_gap_valid() -> f64 {
+    var m : f64 = 0.0;
+    var i : usize = 0;
+    while (i < EVALS) {
+        const g : f64 = abs(F32_VALID[i] - F64_VALID[i]);
+        if (g > m) {
+            m = g;
+        }
+        i = i + 1;
+    }
+    return m;
+}
+
+; the largest gap before step 1500, where the schedule is still calm
+fn study_max_gap_calm() -> f64 {
+    var m : f64 = 0.0;
+    var i : usize = 0;
+    while (i < 15) {
+        const g : f64 = abs(F32_FULL[i] - F64_FULL[i]);
+        if (g > m) {
+            m = g;
+        }
+        i = i + 1;
+    }
+    return m;
+}
+
+fn study_final_gap() -> f64 {
+    return abs(F32_FULL[EVALS - 1] - F64_FULL[EVALS - 1]);
+}
+
+; the verdict the rule gives for the constants above
+fn study_derived_verdict() -> i32 {
+    if (study_max_gap() <= GAP_MAX and study_speedup() >= SPEEDUP_MIN) {
+        return ADOPT;
+    }
+    return REJECT;
+}
+
+; how many of the 12 control numbers differ from the release log by 5e-5 or more
+fn study_control_mismatch() -> u64 {
+    var bad : u64 = 0;
+    var k : usize = 0;
+    while (k < 4) {
+        const i : usize = 5 * (k + 1);
+        if (abs(F64_TRAIN[i] - REL_TRAIN[k]) >= 5.0e-5) {
+            bad = bad + 1;
+        }
+        if (abs(F64_VALID[i] - REL_VALID[k]) >= 5.0e-5) {
+            bad = bad + 1;
+        }
+        if (abs(F64_FULL[i] - REL_FULL[k]) >= 5.0e-5) {
+            bad = bad + 1;
+        }
+        k = k + 1;
+    }
+    return bad;
+}
+
+; how many evals show a loss that did not fall against the eval before (a curve must go down in both runs)
+fn study_rises() -> u64 {
+    var n : u64 = 0;
+    var i : usize = 1;
+    while (i < EVALS) {
+        if (F64_FULL[i] >= F64_FULL[i - 1]) {
+            n = n + 1;
+        }
+        if (F32_FULL[i] >= F32_FULL[i - 1]) {
+            n = n + 1;
+        }
+        i = i + 1;
+    }
+    return n;
+}
+
+test the_eval_steps_run_from_0_to_2000_by_100
+    given first = study_step(0)
+    and   mid = study_step(5)
+    and   last = study_step(EVALS - 1)
+    then  first == 0
+    and   mid == 500
+    and   last == 2000
+
+test the_f64_control_is_the_release_run_at_the_4_shared_steps
+    given bad = study_control_mismatch()
+    then  bad == 0
+
+test both_runs_start_from_the_same_initial_loss
+    given dv = study_start_gap_valid()
+    and   df = study_start_gap_full()
+    and   dt = study_start_gap_train()
+    then  dv < 1.0e-9
+    and   df > 0.5e-4
+    and   df < 1.5e-4
+    and   dt < 1.0e-9
+
+test both_curves_fall_at_every_eval
+    given n = study_rises()
+    then  n == 0
+
+test the_speedup_is_rederived_from_the_tok_per_s_constants
+    given s = study_speedup()
+    and   t = study_time_ratio()
+    and   d = study_speedup_error()
+    then  s > 1.1506
+    and   s < 1.1508
+    and   d < 1.0e-12
+    and   t > 1.15
+    and   t < 1.16
+
+test every_interval_is_faster_in_f32
+    given m = study_min_interval_speedup()
+    then  m > 1.04
+    and   m < 1.05
+
+test the_peak_rss_of_f32_is_under_two_thirds_of_f64
+    given r = study_mem_ratio()
+    then  r > 0.640
+    and   r < 0.642
+
+test the_largest_curve_gap_is_rederived
+    given g = study_max_gap()
+    and   at = study_max_gap_at()
+    and   gv = study_max_gap_valid()
+    and   fin = study_final_gap()
+    then  abs(g - 0.0127) < 1.0e-9
+    and   at == 19
+    and   abs(gv - 0.0213) < 1.0e-9
+    and   abs(fin - 0.0059) < 1.0e-9
+
+test the_curves_coincide_before_the_lr_peak
+    given g = study_max_gap_calm()
+    then  g < 1.5e-3
+
+test verdict_is_tied_to_the_threshold
+    given d = study_derived_verdict()
+    and   g = study_max_gap()
+    and   s = study_speedup()
+    then  VERDICT == d
+    and   (VERDICT == ADOPT) == (g <= GAP_MAX and s >= SPEEDUP_MIN)
+
+test the_verdict_is_reject_because_the_gap_is_over_by_27_ten_thousandths
+    given g = study_max_gap()
+    and   s = study_speedup()
+    then  VERDICT == REJECT
+    and   g > GAP_MAX
+    and   g - GAP_MAX > 0.0026
+    and   g - GAP_MAX < 0.0028
+    and   s >= SPEEDUP_MIN