From 2638a3fcaef82eb5c0d653317cc5f155f268360b Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 19 Oct 2026 14:54:19 +0700 Subject: [PATCH] spec(ml): hslm_f32_study -- HSLM trainer in f32 against f64, 2000 steps same seed: 1.15x faster, 0.64x peak RSS, largest held-out gap 0.0127 nats, verdict REJECT by the stated 0.01 threshold (Closes #10844) Two runs on the Railway lab, side by side: the f64 control (reproduces the release log at steps 500/1000/1500/2000 to every printed digit) and a mechanical f64->f32 copy of train_hslm, nn/hslm and nn/ternary_ste with everything f32, LAMB moments and loss accumulators included (no destabilization). The spec holds both curves, tok/s and VmHWM as constants; its tests re-derive the speed-up, the largest gap and tie the verdict to the threshold. train_hslm.t27 and nn/hslm.t27 are not touched. Co-Authored-By: Claude Sonnet 5.5 --- .trinity/seals/ml_hslm_f32_study.json | 28 +++ specs/ml/hslm_f32_study.t27 | 318 ++++++++++++++++++++++++++ 2 files changed, 346 insertions(+) create mode 100644 .trinity/seals/ml_hslm_f32_study.json create mode 100644 specs/ml/hslm_f32_study.t27 diff --git a/.trinity/seals/ml_hslm_f32_study.json b/.trinity/seals/ml_hslm_f32_study.json new file mode 100644 index 0000000000..387203c434 --- /dev/null +++ b/.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" + } +} \ No newline at end of file diff --git a/specs/ml/hslm_f32_study.t27 b/specs/ml/hslm_f32_study.t27 new file mode 100644 index 0000000000..8a09804d4c --- /dev/null +++ b/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