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

// =========================================================================
// FALSIFY-AK (ReLU): activation-kernel-v1.yaml contract (aprender ReLU)
//
// Five-Whys (PMAT-354):
//   Why 1: aprender had no inline FALSIFY-AK-* tests for ReLU
//   Why 2: GELU/SiLU have FALSIFY tests but ReLU was omitted
//   Why 3: ReLU was "too simple" to need contract tests
//   Why 4: activation-kernel-v1.yaml covers GELU, SiLU, AND ReLU
//   Why 5: ReLU(x)=max(0,x) seemed un-falsifiable
//
// References:
//   - provable-contracts/contracts/activation-kernel-v1.yaml
//   - Nair & Hinton (2010) "Rectified Linear Units"
// =========================================================================

use super::*;
use crate::autograd::Tensor;

/// FALSIFY-AK-001: ReLU(x) >= 0 (non-negativity)
#[test]
fn falsify_ak_001_relu_non_negative() {
    let input = Tensor::new(&[-3.0, -1.0, 0.0, 1.0, 5.0], &[5]);
    let output = relu(&input);

    for (i, &v) in output.data().iter().enumerate() {
        assert!(v >= 0.0, "FALSIFIED AK-001: ReLU output[{i}] = {v} < 0");
    }
}

/// FALSIFY-AK-002: ReLU(x) = x for x > 0
#[test]
fn falsify_ak_002_relu_positive_identity() {
    let input = Tensor::new(&[0.5, 1.0, 2.5, 10.0], &[4]);
    let output = relu(&input);

    for (i, (&out, &inp)) in output.data().iter().zip(input.data().iter()).enumerate() {
        assert!(
            (out - inp).abs() < 1e-6,
            "FALSIFIED AK-002: ReLU({inp}) = {out}, expected {inp} (positive identity) at [{i}]"
        );
    }
}

/// FALSIFY-AK-003: ReLU(x) = 0 for x <= 0
#[test]
fn falsify_ak_003_relu_zero_for_negative() {
    let input = Tensor::new(&[-5.0, -1.0, -0.01, 0.0], &[4]);
    let output = relu(&input);

    for (i, &v) in output.data().iter().enumerate() {
        assert!(
            v.abs() < 1e-6,
            "FALSIFIED AK-003: ReLU({}) = {v}, expected 0",
            input.data()[i]
        );
    }
}

/// FALSIFY-AK-004: ReLU preserves output length
#[test]
fn falsify_ak_004_relu_output_length() {
    let input = Tensor::new(&[1.0, -2.0, 3.0, -4.0, 5.0, -6.0], &[6]);
    let output = relu(&input);

    assert_eq!(
        output.data().len(),
        6,
        "FALSIFIED AK-004: ReLU output len {} != input len 6",
        output.data().len()
    );
}

mod relu_proptest_falsify {
    use super::*;
    use proptest::prelude::*;

    // FALSIFY-AK-001-prop: ReLU non-negativity for random inputs
    proptest! {
        #![proptest_config(ProptestConfig::with_cases(100))]

        #[test]
        fn falsify_ak_001_prop_relu_non_negative(
            x in -1000.0f32..1000.0,
        ) {
            let input = Tensor::new(&[x], &[1]);
            let output = relu(&input);
            prop_assert!(
                output.data()[0] >= 0.0,
                "FALSIFIED AK-001-prop: ReLU({})={} < 0",
                x, output.data()[0]
            );
        }
    }

    // FALSIFY-AK-002-prop: ReLU(x) = x for positive inputs
    proptest! {
        #![proptest_config(ProptestConfig::with_cases(100))]

        #[test]
        fn falsify_ak_002_prop_relu_positive_identity(
            x in 0.001f32..1000.0,
        ) {
            let input = Tensor::new(&[x], &[1]);
            let output = relu(&input);
            prop_assert!(
                (output.data()[0] - x).abs() < 1e-6,
                "FALSIFIED AK-002-prop: ReLU({})={}, expected {}",
                x, output.data()[0], x
            );
        }
    }
}