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 fused ML ops FFI bindings (biasRelu, biasGelu, layerNorm)
Add Lean bindings for existing Metal kernels:
- biasRelu: y = max(0, x + bias) - fused for dense layers
- biasGelu: y = GELU(x + bias) - used in transformers
- layerNorm: (x - mean) * gamma / sqrt(var + eps) + beta

These reduce kernel launch overhead by fusing multiple operations.
  • Loading branch information
alok committed Dec 6, 2025
commit b38656c1ffcdd2dc0924983419b875a6732479d8
148 changes: 148 additions & 0 deletions Metal/metal_backend.mm
Original file line number Diff line number Diff line change
Expand Up @@ -2030,4 +2030,152 @@ LEAN_EXPORT lean_obj_res scilean_accelerate_gemm_f32(
return C;
}

// ============================================================
// Fused ML Operations (Float32)
// ============================================================

// Bias + ReLU: output = max(0, input + bias)
// input: [batch_size, features], bias: [features]
// stride = features (number of bias elements repeated per batch)
LEAN_EXPORT lean_obj_res scilean_metal_bias_relu_f32(
size_t n, // total elements
size_t stride, // bias stride (features per sample)
b_lean_obj_arg input,
b_lean_obj_arg bias
) {
if (!ensure_metal_initialized()) {
return lean_box(0);
}

@autoreleasepool {
id<MTLComputePipelineState> pipeline = get_pipeline(@"bias_relu");
if (!pipeline) return lean_box(0);

id<MTLBuffer> inputBuf = create_buffer_from_byte_array_f32(input, n, true);
id<MTLBuffer> biasBuf = create_buffer_from_byte_array_f32(bias, stride, true);
id<MTLBuffer> outputBuf = [device newBufferWithLength:n * sizeof(float)
options:MTLResourceStorageModeShared];

uint32_t n32 = (uint32_t)n;
uint32_t stride32 = (uint32_t)stride;

id<MTLCommandBuffer> commandBuffer = [commandQueue commandBuffer];
id<MTLComputeCommandEncoder> encoder = [commandBuffer computeCommandEncoder];

[encoder setComputePipelineState:pipeline];
[encoder setBuffer:inputBuf offset:0 atIndex:0];
[encoder setBuffer:biasBuf offset:0 atIndex:1];
[encoder setBuffer:outputBuf offset:0 atIndex:2];
[encoder setBytes:&n32 length:sizeof(n32) atIndex:3];
[encoder setBytes:&stride32 length:sizeof(stride32) atIndex:4];

MTLSize gridSize = MTLSizeMake(n, 1, 1);
NSUInteger tgSize = MIN(pipeline.maxTotalThreadsPerThreadgroup, n);
[encoder dispatchThreads:gridSize threadsPerThreadgroup:MTLSizeMake(tgSize, 1, 1)];
[encoder endEncoding];

[commandBuffer commit];
[commandBuffer waitUntilCompleted];

return buffer_to_byte_array_f32(outputBuf, n);
}
}

// Bias + GELU: output = input * 0.5 * (1 + tanh(sqrt(2/π) * (input + 0.044715 * input³)))
LEAN_EXPORT lean_obj_res scilean_metal_bias_gelu_f32(
size_t n,
size_t stride,
b_lean_obj_arg input,
b_lean_obj_arg bias
) {
if (!ensure_metal_initialized()) {
return lean_box(0);
}

@autoreleasepool {
id<MTLComputePipelineState> pipeline = get_pipeline(@"bias_gelu");
if (!pipeline) return lean_box(0);

id<MTLBuffer> inputBuf = create_buffer_from_byte_array_f32(input, n, true);
id<MTLBuffer> biasBuf = create_buffer_from_byte_array_f32(bias, stride, true);
id<MTLBuffer> outputBuf = [device newBufferWithLength:n * sizeof(float)
options:MTLResourceStorageModeShared];

uint32_t n32 = (uint32_t)n;
uint32_t stride32 = (uint32_t)stride;

id<MTLCommandBuffer> commandBuffer = [commandQueue commandBuffer];
id<MTLComputeCommandEncoder> encoder = [commandBuffer computeCommandEncoder];

[encoder setComputePipelineState:pipeline];
[encoder setBuffer:inputBuf offset:0 atIndex:0];
[encoder setBuffer:biasBuf offset:0 atIndex:1];
[encoder setBuffer:outputBuf offset:0 atIndex:2];
[encoder setBytes:&n32 length:sizeof(n32) atIndex:3];
[encoder setBytes:&stride32 length:sizeof(stride32) atIndex:4];

MTLSize gridSize = MTLSizeMake(n, 1, 1);
NSUInteger tgSize = MIN(pipeline.maxTotalThreadsPerThreadgroup, n);
[encoder dispatchThreads:gridSize threadsPerThreadgroup:MTLSizeMake(tgSize, 1, 1)];
[encoder endEncoding];

[commandBuffer commit];
[commandBuffer waitUntilCompleted];

return buffer_to_byte_array_f32(outputBuf, n);
}
}

// Layer Norm: output = gamma * (input - mean) / sqrt(var + eps) + beta
// Simplified version: each sample normalized independently
// n = total elements, hiddenSize = features per sample
LEAN_EXPORT lean_obj_res scilean_metal_layer_norm_f32(
size_t n,
size_t hiddenSize,
b_lean_obj_arg input,
b_lean_obj_arg gamma,
b_lean_obj_arg beta
) {
if (!ensure_metal_initialized()) {
return lean_box(0);
}

@autoreleasepool {
id<MTLComputePipelineState> pipeline = get_pipeline(@"layer_norm");
if (!pipeline) return lean_box(0);

id<MTLBuffer> inputBuf = create_buffer_from_byte_array_f32(input, n, true);
id<MTLBuffer> gammaBuf = create_buffer_from_byte_array_f32(gamma, hiddenSize, true);
id<MTLBuffer> betaBuf = create_buffer_from_byte_array_f32(beta, hiddenSize, true);
id<MTLBuffer> outputBuf = [device newBufferWithLength:n * sizeof(float)
options:MTLResourceStorageModeShared];

uint32_t n32 = (uint32_t)n;
uint32_t hiddenSize32 = (uint32_t)hiddenSize;
float eps = 1e-5f;

id<MTLCommandBuffer> commandBuffer = [commandQueue commandBuffer];
id<MTLComputeCommandEncoder> encoder = [commandBuffer computeCommandEncoder];

[encoder setComputePipelineState:pipeline];
[encoder setBuffer:inputBuf offset:0 atIndex:0];
[encoder setBuffer:gammaBuf offset:0 atIndex:1];
[encoder setBuffer:betaBuf offset:0 atIndex:2];
[encoder setBuffer:outputBuf offset:0 atIndex:3];
[encoder setBytes:&n32 length:sizeof(n32) atIndex:4];
[encoder setBytes:&hiddenSize32 length:sizeof(hiddenSize32) atIndex:5];
[encoder setBytes:&eps length:sizeof(eps) atIndex:6];

MTLSize gridSize = MTLSizeMake(n, 1, 1);
NSUInteger tgSize = MIN(pipeline.maxTotalThreadsPerThreadgroup, n);
[encoder dispatchThreads:gridSize threadsPerThreadgroup:MTLSizeMake(tgSize, 1, 1)];
[encoder endEncoding];

[commandBuffer commit];
[commandBuffer waitUntilCompleted];

return buffer_to_byte_array_f32(outputBuf, n);
}
}

} // extern "C"
18 changes: 18 additions & 0 deletions SciLean/FFI/Metal.lean
Original file line number Diff line number Diff line change
Expand Up @@ -309,4 +309,22 @@ def softmax (sz : USize) (x : ByteArray) : ByteArray :=
-- Use fused version if available
softmaxFused sz x

-- Bias + ReLU: output = max(0, input + bias)
-- n = total elements, stride = features per sample (bias length)
-- Useful for dense layers: y = relu(Wx + b)
@[extern "scilean_metal_bias_relu_f32"]
opaque biasRelu (n stride : USize) (input bias : @& ByteArray) : ByteArray

-- Bias + GELU: output = GELU(input + bias)
-- GELU approximation: x * 0.5 * (1 + tanh(sqrt(2/π) * (x + 0.044715 * x³)))
-- Used in transformer models like GPT/BERT
@[extern "scilean_metal_bias_gelu_f32"]
opaque biasGelu (n stride : USize) (input bias : @& ByteArray) : ByteArray

-- Layer Normalization: output = gamma * (input - mean) / sqrt(var + eps) + beta
-- n = total elements, hiddenSize = features per sample
-- gamma/beta are learned scale/shift parameters
@[extern "scilean_metal_layer_norm_f32"]
opaque layerNorm (n hiddenSize : USize) (input gamma beta : @& ByteArray) : ByteArray

end SciLean.Metal.Float32