Skip to content
Closed
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
77 commits
Select commit Hold shift + click to select a range
40d0e45
Add Metal GPU backend for accelerated compute
alok Nov 30, 2025
1e6d916
Add reusable benchmark infrastructure
alok Nov 30, 2025
025774f
feat: Add BLAS GEMM integration for Float matrix multiplication
alok Nov 30, 2025
4c6c015
feat: Upgrade to Lean 4.26.0-rc2
alok Nov 30, 2025
936a500
doc: add project philosophy to CLAUDE.md - priorities over proofs
alok Nov 30, 2025
7004850
Fix build errors for Lean v4.26.0-rc2
alok Nov 30, 2025
bcf8c1e
Fix v4.26 compatibility issues in proofs and examples
alok Nov 30, 2025
e1617e4
feat: Add MNIST demo with LeanPlot visualization and GitHub Pages
alok Dec 1, 2025
f76dea6
fix: Update test expected outputs for Lean 4.26 formatting changes
alok Dec 1, 2025
e88f42f
feat: Add Verso documentation site with type-safe neural network exam…
alok Dec 1, 2025
1583d20
Fix compile_inductive panic and upgrade to latest mathlib
alok Dec 2, 2025
baac981
Add explicit LeanBLAS FFI linking for DependentMNIST
alok Dec 2, 2025
11ec2f4
feat: Add NumPy .npy file format support
alok Dec 2, 2025
7483b2c
feat: Add TensorBackend typeclass for device abstraction
alok Dec 2, 2025
690b551
test: Add PyTorch→Lean MNIST verification pipeline
alok Dec 2, 2025
fab24c0
chore: Add test executables and fix DependentMNIST
alok Dec 2, 2025
204f8b9
doc: Add backend architecture notes to CLAUDE.md
alok Dec 2, 2025
29e6d3b
chore: Add Python project config for test scripts
alok Dec 2, 2025
d477ae1
chore: Update .gitignore for Python and test data
alok Dec 2, 2025
cfd2394
chore: Enable doc.verso option in lakefile
alok Dec 2, 2025
0d54ded
fix: Fix Verso doc.verso linting errors
alok Dec 2, 2025
7079fdc
fix: Make simp attributes compatible with doc.verso=true
alok Dec 2, 2025
c11390f
fix: DependentMNIST docstring syntax for doc.verso
alok Dec 2, 2025
a2e8822
feat: Add tinygrad-style ops (mean, argmax, argmin, relu, logSoftmax)
alok Dec 2, 2025
7310ee5
feat: Add LazyTensor compiler module inspired by tinygrad
alok Dec 3, 2025
25199a9
feat: Add movement ops, topological sort, and DataArrayN bridge
alok Dec 3, 2025
8cfb725
feat: Add CUDA backend with JIT compilation architecture
alok Dec 3, 2025
b1d8f49
fix: Clean up slop in LazyTensor and fix file typos
alok Dec 4, 2025
08a4041
fix: Clean up dead code and deprecated files
alok Dec 4, 2025
977e0e0
Add BLASBackend for LazyTensor using LeanBLAS
alok Dec 4, 2025
77013d1
Add LazyTensor interpreter with RTensor runtime type
alok Dec 4, 2025
0e0c95f
fix: Remove unused outSize variable in LazyTensor applyReduce
alok Dec 4, 2025
8e7b533
feat: MPS GEMM integration achieving 12.3 TFLOP/s
alok Dec 5, 2025
94a059f
refactor: AXPY/AXPBY use ByteArray for all params (zero-copy FFI)
alok Dec 5, 2025
1e27e7d
feat: Add Numpy100 exercises and Accelerate GEMM comparison
alok Dec 5, 2025
8a458bb
feat: Add CUDA backend scaffold for cloud GPU testing
alok Dec 6, 2025
1c6d9cd
perf: Add optimized simdgroup GEMM with shared memory prefetch
alok Dec 6, 2025
acda7cf
perf: Add M4-optimized GEMM kernel (experimental)
alok Dec 6, 2025
431549d
perf: Add fused softmax kernels (single memory pass)
alok Dec 6, 2025
f73af79
perf: Optimize Metal GEMM to 2.4+ TFLOP/s, add fused ML ops
alok Dec 6, 2025
d177bfc
perf: Add CPU fallback for small arrays, 25000x faster small ops
alok Dec 6, 2025
b38656c
feat: Add fused ML ops FFI bindings (biasRelu, biasGelu, layerNorm)
alok Dec 6, 2025
8b65913
fix: Remove Intel Mac OpenBLAS path to silence linker warning
alok Dec 6, 2025
b8e27ab
feat: Add fused attention kernels for Metal GPU
alok Dec 6, 2025
60de024
feat: Wire Metal ops into SciLean DataArrayN tensor types
alok Dec 7, 2025
70129c5
feat: Add comprehensive benchmark suite for Metal vs MLX/PyTorch
alok Dec 7, 2025
c6b46e3
feat: Add Conv2D/MaxPool2D/AvgPool2D Metal GPU kernels for CNN inference
alok Dec 11, 2025
9d3c53c
feat: Add optimized Conv2D kernels with 2x speedup for 3x3 convolutions
alok Dec 11, 2025
37e11ee
feat: Add im2col+GEMM Conv2D variant and benchmark comparison
alok Dec 11, 2025
7277bc7
Fix Lean 4.26 deprecations and Metal linking
alok Dec 12, 2025
0b9b2b0
Disable precompile on macOS; add Runge-Kutta steppers; fix deprecations
alok Dec 12, 2025
99cc2e7
Fix lake test on macOS; add einsum notation and smoke tests
alok Dec 14, 2025
3cdedd0
Fix FunctionArgument docs
alok Dec 14, 2025
a004362
Stabilize build + examples (LeanBLAS link, BFGS, WaveEquation)
alok Dec 15, 2025
3f0b1c6
Fix LBFGS line search (remove runtime sorry)
alok Dec 15, 2025
2b4da6b
Add Numpy-style DataArrayN helpers
alok Dec 15, 2025
adffc28
Add DataArrayN.rand and random benchmark
alok Dec 15, 2025
011cb66
Improve DataArray random fill and printing
alok Dec 15, 2025
4656499
Add RandT helper transformer
alok Dec 15, 2025
4a026a5
Use BLAS GEMM for DataArrayN matmul
alok Dec 15, 2025
0cfb4da
Add dtype-parametric C kernel with Lean integration
alok Dec 15, 2025
4289c3e
Add bf16/fp8 (e4m3/e5m2) support to dtype-parametric C kernel
alok Dec 15, 2025
1b6ddd3
Add GPU batching support and fused gemm_bias_relu kernel
alok Dec 16, 2025
59c2407
Fix Metal kernel names and add GPU fused kernel tests
alok Dec 16, 2025
5257bf4
Add batching-aware layer_norm, bias_gelu, avgpool2d to GpuBuffer
alok Dec 17, 2025
468508d
Add GPU batching benchmark
alok Dec 17, 2025
b8eee02
Add flash_attention and flash_attention_causal kernels
alok Dec 17, 2025
e22fd24
Add Metal shader code generator
alok Dec 17, 2025
0eda713
Add batchNorm2d with batching support to GpuBuffer
alok Dec 17, 2025
ca6bd31
Add GPU backward pass kernels for autodiff
alok Dec 17, 2025
91768cc
Optimize Metal GEMM with double-buffered tiling
alok Dec 17, 2025
b7bdf36
Add GPU-accelerated MNIST training example
alok Dec 17, 2025
54abcfe
Add tiled gemmTN and gemmNT kernels
alok Dec 17, 2025
ecf97f6
Add command buffer batching for GPU MNIST training
alok Dec 17, 2025
cb0b45d
Add GPU colSum kernel and optimize training
alok Dec 17, 2025
d3ea5f3
Fix large batch NaN bug with broadcast biasAdd kernel
alok Dec 17, 2025
43b1bc6
Add mini-batch training with GPU buffer slicing
alok Dec 17, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
feat: Add Conv2D/MaxPool2D/AvgPool2D Metal GPU kernels for CNN inference
Metal shaders:
- conv2d_naive: One thread per output element, NCHW format
- conv2d_relu: Fused convolution with ReLU activation
- conv2d_implicit_gemm: Implicit im2col for larger convolutions
- maxpool2d, avgpool2d: Pooling layers
- global_avgpool2d: Global average pooling
- batchnorm2d_inference: Fused batch normalization

FFI bindings:
- Metal.Float32.conv2d with optional fused ReLU
- Metal.Float32.maxPool2d, avgPool2d, globalAvgPool2d
- Metal.Float32.batchNorm2d

All tests pass with <0.0001 error. Performance:
- 224x224 x3→64 Conv2D: 63 GFLOP/s
- 28x28 x32→64 Conv2D: 52 GFLOP/s
  • Loading branch information
alok committed Dec 11, 2025
commit c6b46e3df02221aa80a98db27f4ef8fbd20a1df5
362 changes: 362 additions & 0 deletions Metal/kmeans.metal
Original file line number Diff line number Diff line change
Expand Up @@ -1585,3 +1585,365 @@ kernel void flash_attention_causal(
output[q_idx * head_dim + d] = out_d;
}
}

// ============================================================================
// Conv2D kernels for CNN inference
// ============================================================================

// Conv2D naive - one thread per output element
// Input: NCHW format (batch, channels, height, width)
// Kernel: OIHW format (out_channels, in_channels, kernel_h, kernel_w)
// Output: NCHW format
kernel void conv2d_naive(
device const float* input [[buffer(0)]],
device const float* kernel_weights [[buffer(1)]],
device const float* bias [[buffer(2)]],
device float* output [[buffer(3)]],
constant uint& batch_size [[buffer(4)]],
constant uint& in_channels [[buffer(5)]],
constant uint& out_channels [[buffer(6)]],
constant uint& in_height [[buffer(7)]],
constant uint& in_width [[buffer(8)]],
constant uint& kernel_h [[buffer(9)]],
constant uint& kernel_w [[buffer(10)]],
constant uint& stride_h [[buffer(11)]],
constant uint& stride_w [[buffer(12)]],
constant uint& pad_h [[buffer(13)]],
constant uint& pad_w [[buffer(14)]],
uint3 gid [[thread_position_in_grid]]
) {
// Output dimensions
uint out_height = (in_height + 2 * pad_h - kernel_h) / stride_h + 1;
uint out_width = (in_width + 2 * pad_w - kernel_w) / stride_w + 1;

// gid.x = output column, gid.y = output row, gid.z = batch * out_channels + oc
uint ow = gid.x;
uint oh = gid.y;
uint batch_oc = gid.z;
uint batch = batch_oc / out_channels;
uint oc = batch_oc % out_channels;

if (ow >= out_width || oh >= out_height || batch >= batch_size) return;

float sum = bias[oc];

// Convolution
for (uint ic = 0; ic < in_channels; ic++) {
for (uint kh = 0; kh < kernel_h; kh++) {
for (uint kw = 0; kw < kernel_w; kw++) {
int ih = (int)(oh * stride_h + kh) - (int)pad_h;
int iw = (int)(ow * stride_w + kw) - (int)pad_w;

if (ih >= 0 && ih < (int)in_height && iw >= 0 && iw < (int)in_width) {
uint in_idx = batch * in_channels * in_height * in_width
+ ic * in_height * in_width
+ ih * in_width + iw;
uint k_idx = oc * in_channels * kernel_h * kernel_w
+ ic * kernel_h * kernel_w
+ kh * kernel_w + kw;
sum += input[in_idx] * kernel_weights[k_idx];
}
}
}
}

uint out_idx = batch * out_channels * out_height * out_width
+ oc * out_height * out_width
+ oh * out_width + ow;
output[out_idx] = sum;
}

// Conv2D with implicit GEMM (im2col approach without materializing im2col)
// More efficient for larger convolutions
kernel void conv2d_implicit_gemm(
device const float* input [[buffer(0)]],
device const float* kernel_weights [[buffer(1)]],
device const float* bias [[buffer(2)]],
device float* output [[buffer(3)]],
constant uint& batch_size [[buffer(4)]],
constant uint& in_channels [[buffer(5)]],
constant uint& out_channels [[buffer(6)]],
constant uint& in_height [[buffer(7)]],
constant uint& in_width [[buffer(8)]],
constant uint& kernel_h [[buffer(9)]],
constant uint& kernel_w [[buffer(10)]],
constant uint& stride_h [[buffer(11)]],
constant uint& stride_w [[buffer(12)]],
constant uint& pad_h [[buffer(13)]],
constant uint& pad_w [[buffer(14)]],
uint2 gid [[thread_position_in_grid]],
uint2 tid [[thread_position_in_threadgroup]],
uint2 tg_size [[threads_per_threadgroup]]
) {
// Output dimensions
uint out_height = (in_height + 2 * pad_h - kernel_h) / stride_h + 1;
uint out_width = (in_width + 2 * pad_w - kernel_w) / stride_w + 1;
uint out_spatial = out_height * out_width;

// gid.x = spatial position (oh * out_width + ow) across all batches
// gid.y = output channel
uint spatial_batch = gid.x;
uint oc = gid.y;

if (oc >= out_channels) return;

uint batch = spatial_batch / out_spatial;
uint spatial = spatial_batch % out_spatial;
uint oh = spatial / out_width;
uint ow = spatial % out_width;

if (batch >= batch_size) return;

// Kernel reduction dimension: in_channels * kernel_h * kernel_w
uint K = in_channels * kernel_h * kernel_w;

float sum = bias[oc];

// Compute dot product between im2col column and kernel row
for (uint k = 0; k < K; k++) {
uint ic = k / (kernel_h * kernel_w);
uint rem = k % (kernel_h * kernel_w);
uint kh = rem / kernel_w;
uint kw = rem % kernel_w;

int ih = (int)(oh * stride_h + kh) - (int)pad_h;
int iw = (int)(ow * stride_w + kw) - (int)pad_w;

float in_val = 0.0f;
if (ih >= 0 && ih < (int)in_height && iw >= 0 && iw < (int)in_width) {
uint in_idx = batch * in_channels * in_height * in_width
+ ic * in_height * in_width
+ ih * in_width + iw;
in_val = input[in_idx];
}

uint k_idx = oc * K + k;
sum += in_val * kernel_weights[k_idx];
}

uint out_idx = batch * out_channels * out_height * out_width
+ oc * out_height * out_width
+ oh * out_width + ow;
output[out_idx] = sum;
}

// Conv2D fused with ReLU activation
kernel void conv2d_relu(
device const float* input [[buffer(0)]],
device const float* kernel_weights [[buffer(1)]],
device const float* bias [[buffer(2)]],
device float* output [[buffer(3)]],
constant uint& batch_size [[buffer(4)]],
constant uint& in_channels [[buffer(5)]],
constant uint& out_channels [[buffer(6)]],
constant uint& in_height [[buffer(7)]],
constant uint& in_width [[buffer(8)]],
constant uint& kernel_h [[buffer(9)]],
constant uint& kernel_w [[buffer(10)]],
constant uint& stride_h [[buffer(11)]],
constant uint& stride_w [[buffer(12)]],
constant uint& pad_h [[buffer(13)]],
constant uint& pad_w [[buffer(14)]],
uint3 gid [[thread_position_in_grid]]
) {
uint out_height = (in_height + 2 * pad_h - kernel_h) / stride_h + 1;
uint out_width = (in_width + 2 * pad_w - kernel_w) / stride_w + 1;

uint ow = gid.x;
uint oh = gid.y;
uint batch_oc = gid.z;
uint batch = batch_oc / out_channels;
uint oc = batch_oc % out_channels;

if (ow >= out_width || oh >= out_height || batch >= batch_size) return;

float sum = bias[oc];

for (uint ic = 0; ic < in_channels; ic++) {
for (uint kh = 0; kh < kernel_h; kh++) {
for (uint kw = 0; kw < kernel_w; kw++) {
int ih = (int)(oh * stride_h + kh) - (int)pad_h;
int iw = (int)(ow * stride_w + kw) - (int)pad_w;

if (ih >= 0 && ih < (int)in_height && iw >= 0 && iw < (int)in_width) {
uint in_idx = batch * in_channels * in_height * in_width
+ ic * in_height * in_width
+ ih * in_width + iw;
uint k_idx = oc * in_channels * kernel_h * kernel_w
+ ic * kernel_h * kernel_w
+ kh * kernel_w + kw;
sum += input[in_idx] * kernel_weights[k_idx];
}
}
}
}

uint out_idx = batch * out_channels * out_height * out_width
+ oc * out_height * out_width
+ oh * out_width + ow;
output[out_idx] = max(0.0f, sum); // ReLU
}

// MaxPool2D - one thread per output element
kernel void maxpool2d(
device const float* input [[buffer(0)]],
device float* output [[buffer(1)]],
constant uint& batch_size [[buffer(2)]],
constant uint& channels [[buffer(3)]],
constant uint& in_height [[buffer(4)]],
constant uint& in_width [[buffer(5)]],
constant uint& pool_h [[buffer(6)]],
constant uint& pool_w [[buffer(7)]],
constant uint& stride_h [[buffer(8)]],
constant uint& stride_w [[buffer(9)]],
uint3 gid [[thread_position_in_grid]]
) {
uint out_height = (in_height - pool_h) / stride_h + 1;
uint out_width = (in_width - pool_w) / stride_w + 1;

uint ow = gid.x;
uint oh = gid.y;
uint batch_c = gid.z;
uint batch = batch_c / channels;
uint c = batch_c % channels;

if (ow >= out_width || oh >= out_height || batch >= batch_size) return;

float max_val = -INFINITY;

for (uint ph = 0; ph < pool_h; ph++) {
for (uint pw = 0; pw < pool_w; pw++) {
uint ih = oh * stride_h + ph;
uint iw = ow * stride_w + pw;
uint in_idx = batch * channels * in_height * in_width
+ c * in_height * in_width
+ ih * in_width + iw;
max_val = max(max_val, input[in_idx]);
}
}

uint out_idx = batch * channels * out_height * out_width
+ c * out_height * out_width
+ oh * out_width + ow;
output[out_idx] = max_val;
}

// AvgPool2D - one thread per output element
kernel void avgpool2d(
device const float* input [[buffer(0)]],
device float* output [[buffer(1)]],
constant uint& batch_size [[buffer(2)]],
constant uint& channels [[buffer(3)]],
constant uint& in_height [[buffer(4)]],
constant uint& in_width [[buffer(5)]],
constant uint& pool_h [[buffer(6)]],
constant uint& pool_w [[buffer(7)]],
constant uint& stride_h [[buffer(8)]],
constant uint& stride_w [[buffer(9)]],
uint3 gid [[thread_position_in_grid]]
) {
uint out_height = (in_height - pool_h) / stride_h + 1;
uint out_width = (in_width - pool_w) / stride_w + 1;

uint ow = gid.x;
uint oh = gid.y;
uint batch_c = gid.z;
uint batch = batch_c / channels;
uint c = batch_c % channels;

if (ow >= out_width || oh >= out_height || batch >= batch_size) return;

float sum = 0.0f;
float count = (float)(pool_h * pool_w);

for (uint ph = 0; ph < pool_h; ph++) {
for (uint pw = 0; pw < pool_w; pw++) {
uint ih = oh * stride_h + ph;
uint iw = ow * stride_w + pw;
uint in_idx = batch * channels * in_height * in_width
+ c * in_height * in_width
+ ih * in_width + iw;
sum += input[in_idx];
}
}

uint out_idx = batch * channels * out_height * out_width
+ c * out_height * out_width
+ oh * out_width + ow;
output[out_idx] = sum / count;
}

// Global Average Pooling - reduces spatial dimensions to 1x1
kernel void global_avgpool2d(
device const float* input [[buffer(0)]],
device float* output [[buffer(1)]],
constant uint& batch_size [[buffer(2)]],
constant uint& channels [[buffer(3)]],
constant uint& height [[buffer(4)]],
constant uint& width [[buffer(5)]],
uint2 gid [[thread_position_in_grid]]
) {
uint batch = gid.x;
uint c = gid.y;

if (batch >= batch_size || c >= channels) return;

float sum = 0.0f;
uint spatial = height * width;

for (uint h = 0; h < height; h++) {
for (uint w = 0; w < width; w++) {
uint in_idx = batch * channels * height * width
+ c * height * width
+ h * width + w;
sum += input[in_idx];
}
}

output[batch * channels + c] = sum / (float)spatial;
}

// BatchNorm2D inference - fused with optional ReLU
// Computes: y = (x - mean) / sqrt(var + eps) * gamma + beta
// For inference: mean and var are running statistics
kernel void batchnorm2d_inference(
device const float* input [[buffer(0)]],
device const float* gamma [[buffer(1)]], // scale
device const float* beta [[buffer(2)]], // bias
device const float* running_mean [[buffer(3)]],
device const float* running_var [[buffer(4)]],
device float* output [[buffer(5)]],
constant uint& batch_size [[buffer(6)]],
constant uint& channels [[buffer(7)]],
constant uint& height [[buffer(8)]],
constant uint& width [[buffer(9)]],
constant float& eps [[buffer(10)]],
constant uint& apply_relu [[buffer(11)]],
uint3 gid [[thread_position_in_grid]]
) {
uint w_idx = gid.x;
uint h_idx = gid.y;
uint batch_c = gid.z;
uint batch = batch_c / channels;
uint c = batch_c % channels;

if (w_idx >= width || h_idx >= height || batch >= batch_size) return;

uint idx = batch * channels * height * width
+ c * height * width
+ h_idx * width + w_idx;

float x = input[idx];
float mean = running_mean[c];
float var = running_var[c];
float g = gamma[c];
float b = beta[c];

float y = (x - mean) * rsqrt(var + eps) * g + b;

if (apply_relu) {
y = max(0.0f, y);
}

output[idx] = y;
}
Loading