Optimized Neural Network Verification

This module provides high-performance implementations for neural network interval propagation, designed to scale to real-world networks.

Key Optimizations

1. Structure-of-Arrays (SoA) Layout: IntervalArray stores lower and upper bounds in separate contiguous arrays for cache efficiency (~5x improvement).

2. Split-Sign Matrix Decomposition: Pre-decompose W = W⁺ - W⁻ to eliminate branching in interval matrix multiplication (~2x improvement).

3. Common Exponent Integer Arithmetic: Align all values to a common exponent for pure integer (GMP) arithmetic (~10-50x improvement).

Main Types

• IntervalArray - SoA interval vector representation
• QuantizedLayer - Layer with aligned integer representation
• QuantizedNet - Full network with quantized layers

Usage

import LeanCert.ML.Optimized

open LeanCert.ML.Optimized

-- Create quantized network from rational layers
def qnet := QuantizedNet.ofLayers myLayers

-- Fast interval propagation
def output := qnet.forward (QuantizedLayer.alignInput myInput prec)