aprender-core 0.29.2

Next-generation machine learning library in pure Rust
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116

// CONTRACT: batchnorm-kernel-v1.yaml
// HASH: sha256:c3d4e5f6a7b89012
// Generated by: pv probar --binding
// DO NOT EDIT — regenerate with `pv probar --binding`

use aprender::autograd::Tensor;
use aprender::nn::BatchNorm1d;
use aprender::nn::Module;
use proptest::prelude::*;

proptest! {
    /// Obligation: Training standardization (invariant)
    /// Formal: mean(BN(x)) ≈ beta per channel (beta=0 by default)
    #[test]
    fn prop_training_standardization(
        data in proptest::collection::vec(-10.0f32..10.0, 20..21usize)
    ) {
        // batch=5, features=4, total=20
        let batch = 5;
        let features = 4;
        let data: Vec<f32> = (0..batch * features)
            .map(|i| if i < data.len() { data[i] } else { 0.0 })
            .collect();
        let bn = BatchNorm1d::new(features);
        let x = Tensor::new(&data, &[batch, features]);
        let y = bn.forward(&x);
        let y_data = y.data();

        // Check mean per feature across batch ≈ 0 (beta=0)
        for f in 0..features {
            let mean: f32 = (0..batch).map(|b| y_data[b * features + f]).sum::<f32>()
                / batch as f32;
            prop_assert!(
                mean.abs() < 0.5,
                "feature {f} mean={mean}, expected ~0"
            );
        }
    }

    /// Obligation: Denominator always positive (bound)
    /// Formal: sqrt(σ² + ε) > 0
    #[test]
    fn prop_denominator_positive(
        data in proptest::collection::vec(-100.0f32..100.0, 20..21usize)
    ) {
        let batch = 5;
        let features = 4;
        let data: Vec<f32> = (0..batch * features)
            .map(|i| if i < data.len() { data[i] } else { 0.0 })
            .collect();
        let bn = BatchNorm1d::new(features);
        let x = Tensor::new(&data, &[batch, features]);
        let y = bn.forward(&x);

        for (i, &val) in y.data().iter().enumerate() {
            prop_assert!(
                val.is_finite(),
                "output[{i}]={val} is not finite — denominator may be non-positive"
            );
        }
    }

    /// Obligation: Running variance non-negative (bound)
    /// Formal: σ_running >= 0
    #[test]
    fn prop_running_variance_non_negative(
        var in 0.0f32..100.0,
        batch_var in 0.0f32..100.0,
        momentum in 0.01f32..0.5
    ) {
        // running_var = (1 - momentum) * running_var + momentum * batch_var
        let new_var = (1.0 - momentum) * var + momentum * batch_var;
        prop_assert!(
            new_var >= 0.0,
            "running variance={new_var}, expected >= 0"
        );
    }

    /// Obligation: Eval mode uses running statistics (invariant)
    /// Formal: In eval mode, output depends on running_mean/running_var, not batch stats
    #[test]
    fn prop_eval_uses_running_stats(
        data1 in proptest::collection::vec(-10.0f32..10.0, 8..9usize),
        data2 in proptest::collection::vec(-10.0f32..10.0, 8..9usize)
    ) {
        // In training mode with different batches, BN uses batch stats.
        // We verify that BN produces finite output for different inputs.
        let batch = 2;
        let features = 4;
        let d1: Vec<f32> = (0..batch * features)
            .map(|i| if i < data1.len() { data1[i] } else { 0.0 })
            .collect();
        let d2: Vec<f32> = (0..batch * features)
            .map(|i| if i < data2.len() { data2[i] } else { 0.0 })
            .collect();
        let bn = BatchNorm1d::new(features);
        let x1 = Tensor::new(&d1, &[batch, features]);
        let x2 = Tensor::new(&d2, &[batch, features]);
        let y1 = bn.forward(&x1);
        let y2 = bn.forward(&x2);

        // Both should be finite
        for &val in y1.data().iter().chain(y2.data().iter()) {
            prop_assert!(val.is_finite(), "non-finite BN output={val}");
        }
    }

    /// Obligation: SIMD matches scalar within ULP (equivalence)
    #[test]
    #[ignore = "SIMD equivalence — trueno domain"]
    fn prop_simd_equivalence(
        _x in proptest::collection::vec(-100.0f32..100.0, 1..32usize)
    ) {
        // SIMD equivalence testing is trueno's responsibility
    }
}