Прогон, который ничего не проверил

Вы узнаете

Что такое пустой проход, почему зелёный отчёт может его скрыть и как подложенная ошибка отличает настоящие проверки от пустых.

Попробуйте

Найдите строку о пустых проходах и тест, который ломает подложенная ошибка; затем откройте спеку и найдите инвариант, который утверждает только true.

specs/numeric/gfternary.t27

// SPDX-License-Identifier: Apache-2.0
; gfternary.t27 0 GFTernary Format Specification
; 2-bit golden-ratio ternary: representable values { -phi, 0, +phi }
; The phi-scaled limit of the ternary-weight family: GFTernary = phi * {-1,0,+1}
; (a ternary-weight quantizer, cf. TWN / BitNet, with the scale fixed at phi).
; phi^2 + phi^-2 = 3 | TRINITY

module triformat-gaternary;

// ============================================================================
// Constants
// ============================================================================

// Golden ratio phi = (1 + sqrt(5)) / 2 and its reciprocal phi^-1 = phi - 1.
pub const PHI : f64 = 1.6180339887498949;
pub const PHI_INV : f64 = 0.6180339887498949;

// 2-bit code points, stored in the low two bits of a u8 container.
pub const CODE_MASK : u8 = 0x03;
pub const GAT_ZERO : u8 = 0x00;   // 0b00 -> 0
pub const GAT_POS  : u8 = 0x01;   // 0b01 -> +phi
pub const GAT_NEG  : u8 = 0x02;   // 0b10 -> -phi
pub const GAT_RSVD : u8 = 0x03;   // 0b11 -> reserved (folds to zero)

// ============================================================================
// Types
// ============================================================================

pub const GFTernary = u8;

// ============================================================================
// Core functions
// ============================================================================

// gat_canonical(code) GFTernary
// Mask to the low two bits and fold the reserved code 0b11 onto zero.
pub fn gat_canonical(code: GFTernary) GFTernary {
    const c = code & CODE_MASK;
    return if (c == GAT_RSVD) GAT_ZERO else c;
}

// gat_is_zero(code) bool
pub fn gat_is_zero(code: GFTernary) bool {
    return gat_canonical(code) == GAT_ZERO;
}

// gat_sign(code) i8 -> -1, 0, +1
pub fn gat_sign(code: GFTernary) i8 {
    const c = gat_canonical(code);
    return if (c == GAT_POS) 1 else if (c == GAT_NEG) -1 else 0;
}

// gat_from_sign(s) GFTernary  (s in {-1, 0, +1})
pub fn gat_from_sign(s: i8) GFTernary {
    return if (s > 0) GAT_POS else if (s < 0) GAT_NEG else GAT_ZERO;
}

// gat_negate(code) GFTernary  -- flips +phi <-> -phi, zero is fixed.
pub fn gat_negate(code: GFTernary) GFTernary {
    const c = gat_canonical(code);
    return if (c == GAT_POS) GAT_NEG else if (c == GAT_NEG) GAT_POS else GAT_ZERO;
}

// gat_to_f64(code) f64 -> { +PHI, -PHI, 0.0 }
pub fn gat_to_f64(code: GFTernary) f64 {
    const c = gat_canonical(code);
    return if (c == GAT_POS) PHI else if (c == GAT_NEG) -PHI else 0.0;
}

// gat_from_f64(value, threshold) GFTernary
// Ternary-weight quantizer with fixed phi scale (TWN with alpha = phi):
//   |value| <= |threshold|        -> 0
//   value   >  |threshold|        -> +phi
//   value   < -|threshold|        -> -phi
pub fn gat_from_f64(value: f64, threshold: f64) GFTernary {
    const t = if (threshold < 0.0) -threshold else threshold;
    if (value > t) return GAT_POS;
    if (value < -t) return GAT_NEG;
    return GAT_ZERO;
}

// ============================================================================
// Tests (L4 TESTABILITY). f64 checks use a tolerance (L5 IDENTITY).
// ============================================================================

test "gat_three_representable_values" {
    const dp = gat_to_f64(GAT_POS) - PHI;
    const dn = gat_to_f64(GAT_NEG) + PHI;
    try std.testing.expect(gat_to_f64(GAT_ZERO) == 0.0);
    try std.testing.expect(dp > -1e-12 and dp < 1e-12);
    try std.testing.expect(dn > -1e-12 and dn < 1e-12);
}

test "gat_reserved_code_folds_to_zero" {
    try std.testing.expect(gat_is_zero(GAT_RSVD));
    try std.testing.expect(gat_to_f64(GAT_RSVD) == 0.0);
}

test "gat_negate_symmetry" {
    const d = gat_to_f64(gat_negate(GAT_POS)) + PHI;
    try std.testing.expect(d > -1e-12 and d < 1e-12);
    try std.testing.expect(gat_negate(GAT_ZERO) == GAT_ZERO);
}

test "gat_sign_roundtrip" {
    try std.testing.expect(gat_from_sign(gat_sign(GAT_POS)) == GAT_POS);
    try std.testing.expect(gat_from_sign(gat_sign(GAT_NEG)) == GAT_NEG);
    try std.testing.expect(gat_from_sign(gat_sign(GAT_ZERO)) == GAT_ZERO);
}

test "gat_quantizer_threshold" {
    try std.testing.expect(gat_from_f64(2.0, 0.5) == GAT_POS);
    try std.testing.expect(gat_from_f64(-2.0, 0.5) == GAT_NEG);
    try std.testing.expect(gat_from_f64(0.1, 0.5) == GAT_ZERO);
}

// L5 IDENTITY: phi^2 = phi + 1; phi^2 + phi^-2 = 3; phi * phi^-1 = 1.
test "gat_phi_identity_l5" {
    const d1 = PHI * PHI - (PHI + 1.0);
    const d2 = PHI * PHI + PHI_INV * PHI_INV - 3.0;
    const d3 = PHI * PHI_INV - 1.0;
    try std.testing.expect(d1 > -1e-12 and d1 < 1e-12);
    try std.testing.expect(d2 > -1e-12 and d2 < 1e-12);
    try std.testing.expect(d3 > -1e-12 and d3 < 1e-12);
}

// ============================================================================
// Bench (L4 TESTABILITY)
// ============================================================================

bench "bench_gft_decode_latency" {
    // measure: nanoseconds to decode a code to f64
    // target: < 20ns (mask + two compares)
    @setEvalBranchQuota(10000);
    var result: f64 = 0.0;
    const code: GFTernary = GAT_NEG;
    for (0..1000) |_| {
        result = gat_to_f64(code);
    }
    _ = result;
}

bench "bench_gft_quantize_latency" {
    // measure: nanoseconds to ternary-quantize one f64 with a threshold
    // target: < 30ns (abs + two compares)
    @setEvalBranchQuota(10000);
    var result: GFTernary = 0;
    const v: f64 = 1.3;
    const thr: f64 = 0.5;
    for (0..1000) |_| {
        result = gat_from_f64(v, thr);
    }
    _ = result;
}

// =====================================================================
// Phase C1/C2 (epic #181) -- GFTernary {-phi,0,+phi} vs BitNet {-1,0,+1} (appended)
// Falsification: phi-ternary within MC error of integer-ternary => phi-scale falsified.
// =====================================================================

pub const INT_TERNARY_SCALE : f64 = 1.0;

// GFTernary arm scale (phi -- defined in existing constants above as PHI).
// [Open conjecture]: phi scale may improve over int-ternary; not proven.
// pub const PHI already defined above; re-reference only.

// Scaled ternary arm: alpha = PHI used as initial guess; to be optimised.
// This arm checks whether ANY fixed scale beats tuned alpha.
pub const SCALED_TERNARY_INIT_ALPHA : f64 = PHI;

// MC error threshold: below this delta in BPB the claim is falsified.
pub const MC_ERROR_BPB : f64 = 0.003;

// GFTernary weight L2-norm per element (for normalisation comparison).
// gat_weight_l2 = phi (non-zero arms); int_ternary_weight_l2 = 1.0.
// A scale factor of phi inflates norms -- must be tracked in comparison.
pub const GAT_WEIGHT_NORM : f64 = PHI;
pub const INT_TERNARY_WEIGHT_NORM : f64 = INT_TERNARY_SCALE;

// ============================================================================
// C1 Tests (L4 TESTABILITY)
// ============================================================================

test "gat_control_arm_definitions" {
    // Arm A: GFTernary scale is phi
    const arm_a_scale : f64 = PHI;
    // Arm B: IntTernary scale is exactly 1.0
    const arm_b_scale : f64 = INT_TERNARY_SCALE;
    // Arm C: ScaledTernary initial alpha = phi (will be optimised)
    const arm_c_init : f64 = SCALED_TERNARY_INIT_ALPHA;
    // Assert phi scale is not trivially the same as int-ternary scale.
    const d_ab = arm_a_scale - arm_b_scale;
    try std.testing.expect(d_ab > 0.5);  // phi - 1 ~ 0.618 > 0.5
    // Assert arm C initialises at phi (same as arm A)
    const d_ac = arm_a_scale - arm_c_init;
    try std.testing.expect(d_ac > -1e-12 and d_ac < 1e-12);
}

test "gat_falsification_criterion_bpb_gap" {
    // Given: bpb_gft (arm A) and bpb_int (arm B) from a hypothetical run.
    // The test checks the logic: claim survives iff gap > MC_ERROR_BPB.
    //
    // Scenario 1: GFTernary wins by more than MC error => claim survives.
    const bpb_gft_wins : f64 = 2.195;
    const bpb_int_ref  : f64 = 2.210;
    const gap_wins = bpb_int_ref - bpb_gft_wins;
    try std.testing.expect(gap_wins > MC_ERROR_BPB);  // 0.015 > 0.003

    // Scenario 2: Gap is within MC error => phi-specificity falsified.
    const bpb_gft_tied : f64 = 2.209;
    const gap_tied = bpb_int_ref - bpb_gft_tied;
    // gap_tied = 0.001 < 0.003 => falsified; confirm the arithmetic:
    try std.testing.expect(gap_tied < MC_ERROR_BPB);

    // Scenario 3: IntTernary wins => phi-specificity also falsified.
    const bpb_gft_worse : f64 = 2.215;
    const gap_worse = bpb_int_ref - bpb_gft_worse;
    // gap_worse < 0 => falsified
    try std.testing.expect(gap_worse < 0.0);
}

test "gat_weight_norm_ratio" {
    // GFT weights have L2 norm phi per non-zero element.
    // Int-ternary weights have L2 norm 1.0.
    // Ratio = phi; must be accounted for in effective learning-rate comparison.
    const ratio = GAT_WEIGHT_NORM / INT_TERNARY_WEIGHT_NORM;
    const expected_ratio = PHI;
    const d = ratio - expected_ratio;
    try std.testing.expect(d > -1e-12 and d < 1e-12);
}

test "gat_mc_error_threshold_positive" {
    // MC_ERROR_BPB must be strictly positive and small.
    try std.testing.expect(MC_ERROR_BPB > 0.0);
    try std.testing.expect(MC_ERROR_BPB < 0.01);
}

test "gat_phi_l5_identity_in_ablation_context" {
    // L5 IDENTITY: phi^2 + phi^-2 = 3 holds exactly for the scale constant.
    // [Verified] -- the ONLY verified phi fact.
    const phi2 = PHI * PHI;
    const phiinv2 = PHI_INV * PHI_INV;
    const trinity = phi2 + phiinv2;
    const d = trinity - 3.0;
    try std.testing.expect(d > -1e-12 and d < 1e-12);
}

// ============================================================================
// C1 Invariants (L4 TESTABILITY)
// ============================================================================

invariant "gat_phi_scale_distinct_from_unit" {
    // phi != 1.0 -- the ternary arms are numerically different.
    // [Verified trivially from phi definition; not a conjecture.]
    @compileAssert(PHI > 1.5);          // phi ~ 1.618
    @compileAssert(INT_TERNARY_SCALE == 1.0);
}

invariant "gat_integer_ternary_scale_unit" {
    // The integer ternary baseline (BitNet b1.58) uses scale exactly 1.0.
    @compileAssert(INT_TERNARY_SCALE == 1.0);
}

invariant "gat_mc_error_positive" {
    // MC error threshold must be positive to be a valid falsification bound.
    @compileAssert(MC_ERROR_BPB > 0.0);
}

invariant "gat_arm_scales_distinct" {
    // Arms A and B must have different scales to be a real ablation.
    // PHI > 1.0 == INT_TERNARY_SCALE is guaranteed by phi > 1.
    @compileAssert(PHI > INT_TERNARY_SCALE);
}

invariant "gat_claim_status_open_conjecture" {
    // [Open conjecture]: phi ternary scale superiority over int-ternary is NOT
    // proven by any theorem in this repo. The claim requires the control test.
    // This invariant enforces that no assertion in this file claims it proven.
    @compileAssert(true);  // structural placeholder -- human reviewer checks above
}

// ============================================================================
// C2 -- CPU Inference Baseline (bitnet.cpp / IGLA Cramming Regime)
//
// Reference: Wang et al. 2024, "1-bit LLM: The Era of 1-bit Large Language
//   Models for All", arXiv 2410.16144 (bitnet.cpp CPU kernel).
// Context: Geiping & Goldstein 2022, "Cramming: Training a Language Model on
//   a Single GPU in One Day" -- IGLA regime uses single-GPU training with
//   CPU inference cost as deployment metric.
// Architecture target: SmolLM2 hidden=384, 1-layer ternary linear for bench.
//
// FALSIFICATION context: if GFTernary MAC throughput on CPU is more than 2x
//   slower than IntTernary at equal sparsity (~1/3 non-zero), then GFTernary
//   is disqualified on practical grounds even if BPB is competitive.
// ============================================================================

// Sparsity constant: approximately 1/3 of ternary weights are non-zero
//   (expected for a balanced ternary distribution at threshold 0.5).
pub const TERNARY_NONZERO_FRACTION : f64 = 0.333;

// Width of the linear layer in the CPU bench (SmolLM2 hidden=384).
pub const BENCH_HIDDEN_DIM : u32 = 384;

// Maximum allowed latency ratio: GFT over IntTernary. Above this the
// GFTernary format is impractical for CPU inference.
pub const MAX_LATENCY_RATIO : f64 = 2.0;

// ============================================================================
// C2 Tests
// ============================================================================

test "gat_cpu_bench_constants_sane" {
    // Hidden dim = 384 matches the SmolLM2/IGLA champion config.
    try std.testing.expect(BENCH_HIDDEN_DIM == 384);
    // Non-zero fraction is approximately 1/3.
    const d = TERNARY_NONZERO_FRACTION - 0.333;
    try std.testing.expect(d > -1e-3 and d < 1e-3);
    // Max ratio bound is 2.0 (practical deployment gate).
    try std.testing.expect(MAX_LATENCY_RATIO == 2.0);
}

test "gat_cpu_latency_ratio_gate" {
    // Simulated scenario: ratio 1.05 (GFT 5% slower than IntTernary).
    // A ratio below MAX_LATENCY_RATIO is acceptable.
    const simulated_ratio : f64 = 1.05;
    try std.testing.expect(simulated_ratio < MAX_LATENCY_RATIO);

    // Simulated scenario: ratio 2.5 => GFTernary fails the practical gate.
    const failing_ratio : f64 = 2.5;
    try std.testing.expect(failing_ratio > MAX_LATENCY_RATIO);
}

// ============================================================================
// C2 Bench (L4 TESTABILITY)
// ============================================================================

bench "bench_gft_vs_int_ternary_mac" {
    // Measures: MAC throughput for a ternary-weight matrix-vector product
    //   of shape (BENCH_HIDDEN_DIM x BENCH_HIDDEN_DIM) at ~1/3 sparsity.
    // Compares two code paths:
    //   (a) GFTernary: decode GAT_NEG/GAT_POS to +/-phi, multiply.
    //   (b) IntTernary: decode to +/-1, multiply (same branch structure).
    // Difference: GFTernary multiplies by phi (a float multiply) vs 1.0
    //   (which compilers may elide). This bench quantifies that overhead.
    // Target: ratio (a)/(b) < MAX_LATENCY_RATIO = 2.0.
    //
    // Relation to bitnet.cpp (arXiv 2410.16144): that paper reports
    //   ~1.37 tok/s per W speedup on CPU vs FP16 for int-ternary.
    //   GFTernary must not erode that speedup by more than 2x to remain
    //   competitive in the IGLA CPU inference regime.
    @setEvalBranchQuota(100000);
    const N : usize = BENCH_HIDDEN_DIM;
    var sum_gft : f64 = 0.0;
    var sum_int : f64 = 0.0;
    const codes : [4]GFTernary = [GAT_ZERO, GAT_POS, GAT_NEG, GAT_ZERO];
    const signs : [4]i8 = [0, 1, -1, 0];
    for (0..N) |i| {
        const idx = i & 3;
        // GFTernary path: multiply by phi
        sum_gft += gat_to_f64(codes[idx]) * 0.5;
        // IntTernary path: multiply by sign (no phi scale)
        sum_int += @as(f64, @floatFromInt(signs[idx])) * 0.5;
    }
    _ = sum_gft;
    _ = sum_int;
}

bench "bench_gft_cpu_inference_bitnet_baseline" {
    // End-to-end latency proxy: decode one row of BENCH_HIDDEN_DIM ternary
    //   weights and accumulate dot product with a f64 input vector.
    // This is the inner loop of a ternary linear layer on CPU.
    // Reference: bitnet.cpp reports sub-2ns/op on modern x86 for int-ternary;
    //   GFTernary target: < 4ns/op (2x tolerance per MAX_LATENCY_RATIO).
    @setEvalBranchQuota(100000);
    const N : usize = BENCH_HIDDEN_DIM;
    var acc : f64 = 0.0;
    var code : GFTernary = GAT_POS;
    for (0..N) |_| {
        // GFTernary decode + multiply (the critical inner loop operation)
        acc += gat_to_f64(code) * 0.25;
        code = gat_canonical(code + 1);
    }
    _ = acc;
}

Открыть спеку урока в плеере ↗

Все уроки

• Модуль 1 · Лаборатория: наши исследования

  Свой формат чисел, честная таблица результатов и таблицы модели, перемноженные на плате.

  1. 01 T27: наш собственный формат чисел
  2. 02 Честная таблица результатов
  3. 03 Таблицы модели на плате

• Модуль 2 · ИИ-числа: блок MX

  Как ИИ-чипы хранят веса в нескольких битах: один общий масштаб на блок, сам байт масштаба и что один выброс делает с соседями.

  1. 04 Один масштаб на блок весов
  2. 05 Байт масштаба на настоящей машине
  3. 06 Один выброс, много нулей

• Модуль 3 · Тернарные веса

  Веса, которые бывают только минус масштаб, ноль или плюс масштаб, пять правил, которые должен пройти тернарный алфавит, и прогон тестов, который ничего не проверил.

  1. 07 Веса минус фи, ноль и плюс фи
  2. 08 Прогон, который ничего не проверил
  3. 09 Пять правил для алфавита весов

• Модуль 4 · Тернарный формат Ternary Network Float

  Правило, которое компилятор проверяет до запуска любого теста, и 17-битное число с плавающей точкой, порядок которого — четыре сбалансированных трита.

  1. 10 Заблокирован — не значит провален
  2. 11 Число, у которого порядок — четыре трита
  3. 12 Дважды сменить знак — получить число обратно

• Модуль 5 · Арифметика чисел со знаком

  Умножить два числа со знаком, сложить их, когда знаки разные, и сделать то и другое сразу в умножении с накоплением.

  1. 13 Знак — это один бит
  2. 14 Разные знаки — вычитание
  3. 15 Умножить, потом сложить

• Модуль 6 · Части нейрона

  ReLU с изломом в нуле, степень двойки для softmax и argmax, который называет ответ.

  1. 16 Излом в нуле
  2. 17 Два в степени x
  3. 18 Выбрать наибольшее

• Модуль 7 · Обучение на ошибке

  Потеря, которая оценивает неверную догадку в битах, один шаг, который сдвигает вес против градиента, и скрытый слой, который нужен XOR.

  1. 19 Потеря в битах
  2. 20 Один шаг вниз по склону
  3. 21 XOR нужен излом

• Модуль 8 · BitNet: тернарные сети

  Порог, который сжимает сумму обратно до трёх значений, один нейрон, который становится другой функцией при смене весов, и нейрон, который читает входы по 27 тритов за раз.

  1. 22 Обратно в три значения
  2. 23 Тот же нейрон, другие веса
  3. 24 Нейрон по кускам

• Модуль 9 · Тернарный MAC как чип

  Скалярное произведение 27 тритов как провода без регистра, та же сумма, которую регистр копит на каждом такте, и небольшая целая сеть в конце курса.

  1. 25 Скалярное произведение из проводов
  2. 26 Складывать на каждом такте
  3. 27 Целая сеть