aprender-core 0.31.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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

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

use aprender::autograd::Tensor;
use aprender::nn::functional::{gelu, relu};
use proptest::prelude::*;

proptest! {
    /// Obligation: GELU at zero (invariant)
    /// Formal: GELU(0) = 0
    #[test]
    fn prop_gelu_at_zero(_dummy in 0..1i32) {
        let x = Tensor::new(&[0.0f32], &[1, 1]);
        let y = gelu(&x);
        let val = y.data()[0];
        prop_assert!(
            val.abs() < 1e-6,
            "GELU(0)={val}, expected 0"
        );
    }

    /// Obligation: GELU approximation error (bound)
    /// Formal: |GELU_approx(x) - GELU_exact(x)| < eps for |x| < 10
    #[test]
    fn prop_gelu_approximation_error(
        x_val in -10.0f32..10.0
    ) {
        let x = Tensor::new(&[x_val], &[1, 1]);
        let y = gelu(&x);
        let val = y.data()[0];

        // Reference: GELU(x) = x * Phi(x)
        // Using tanh approximation: 0.5*x*(1 + tanh(sqrt(2/pi)*(x + 0.044715*x^3)))
        let xf = f64::from(x_val);
        let inner = std::f64::consts::FRAC_2_PI.sqrt()
            * (xf + 0.044715 * xf.powi(3));
        let reference = 0.5 * xf * (1.0 + inner.tanh());

        let diff = (f64::from(val) - reference).abs();
        prop_assert!(
            diff < 1e-3,
            "GELU({x_val})={val}, reference={reference}, diff={diff}"
        );
    }

    /// FALSIFY-ACT-003: SiLU at zero (invariant)
    /// Formal: SiLU(0) = 0 * sigmoid(0) = 0
    #[test]
    fn prop_silu_at_zero(dummy in 0..1i32) {
        let _ = dummy;
        let val = aprender::nn::functional::silu_scalar(0.0);
        prop_assert!(val.abs() < 1e-7, "SiLU(0) = {val}, expected 0.0");
    }

    /// Obligation: ReLU monotonic (monotonicity)
    /// Formal: x >= y => ReLU(x) >= ReLU(y)
    #[test]
    fn prop_relu_monotonic(
        a in -100.0f32..100.0,
        b in -100.0f32..100.0
    ) {
        let x_a = Tensor::new(&[a], &[1, 1]);
        let x_b = Tensor::new(&[b], &[1, 1]);
        let y_a = relu(&x_a).data()[0];
        let y_b = relu(&x_b).data()[0];

        if a >= b {
            prop_assert!(
                y_a >= y_b,
                "ReLU not monotonic: a={a} >= b={b} but relu(a)={y_a} < relu(b)={y_b}"
            );
        }
    }

    /// Obligation: ReLU non-negative (invariant)
    /// Formal: ReLU(x) >= 0 for all x
    #[test]
    fn prop_relu_non_negative(
        data in proptest::collection::vec(-1000.0f32..1000.0, 1..128usize)
    ) {
        let n = data.len();
        let x = Tensor::new(&data, &[1, n]);
        let y = relu(&x);
        for (i, &val) in y.data().iter().enumerate() {
            prop_assert!(
                val >= 0.0,
                "ReLU output[{i}]={val}, expected >= 0"
            );
        }
    }

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

// Additional direct tests for boundary conditions
#[test]
fn relu_zero_gives_zero() {
    let x = Tensor::new(&[0.0f32], &[1, 1]);
    let y = relu(&x);
    assert!((y.data()[0]).abs() < f32::EPSILON);
}

#[test]
fn relu_positive_passthrough() {
    let x = Tensor::new(&[5.0f32], &[1, 1]);
    let y = relu(&x);
    assert!((y.data()[0] - 5.0).abs() < f32::EPSILON);
}

#[test]
fn relu_negative_clamps_to_zero() {
    let x = Tensor::new(&[-5.0f32], &[1, 1]);
    let y = relu(&x);
    assert!((y.data()[0]).abs() < f32::EPSILON);
}

#[test]
fn gelu_negative_approaches_zero() {
    let x = Tensor::new(&[-10.0f32], &[1, 1]);
    let y = gelu(&x);
    assert!(y.data()[0].abs() < 0.01);
}