topic · 17 notes
GPUs & Systems, as it ships.
Under every model is a stack of systems work: GPU kernels and drivers, CUDA and ROCm, virtualization, memory allocators, compilers and the languages the tooling is written in. These notes cover that layer where it changes what AI workloads can do.
The OpenAI Navier-Stokes proof compiled in Lean with m + 5 where the paper says m + 4
The OpenAI Navier-Stokes proof's Lean code bounds Lemma 8.6 by m + 5, not the paper's m + 4. Cambridge and KCL mathematicians flag the weaker lemma.
ts-rust passes 181,711 ported Go tests and checks in about half of Go's time
ts-rust, an LLM-written Rust port of TypeScript 7, passes 181,711 ported Go tests and type checks in about half of Go's time. Ships on npm as tsc-rs.
virtio-nvgpu: NVIDIA GPU in a KVM guest without passthrough
virtio-nvgpu forwards NVIDIA driver ioctls into a KVM guest, within 2% of bare metal on an RTX 3060, but CUDA is untested and there is no IOMMU boundary.
Microsoft Copilot runtime Rust agentic port cost $120K and a few dozen regressions
Microsoft ported 430,000 lines of Copilot TypeScript to 800,000 lines of Rust for about $120,000 in tokens over 14.5 weeks, with dozens of regressions.
How a 4B model trained with RL produced query plans faster than Postgres
A 4B Qwen model post-trained with SFT and a custom GRPO variant hit a 1.81x geometric mean speedup and 44.7% lower summed latency on 113 join-heavy queries.
What a Linux GPU driver for the M4 Mac Mini gives you today
A Linux GPU driver for the M4 Mac Mini hits OpenGL ES 3.0 conformance and 200fps Minecraft in about a month, but has no compute API and no Vulkan.
Fable 5.1 solved the Cyphral Distich cipher in 44 minutes and 176k tokens
Sir Thomas Urquhart's Cyphral Distich, solved: Claude Fable 5.1 keyed its 64 numbers to his 32 Proquiritations in 44 minutes, then checked 285 positions.
Deltafin Kimi K3 SSD weight streaming on a MacBook: 1 tok/s, 376s first token
A deltafin fork streams Kimi K3's 1.45 TB expert bank off four SSDs on an M5 Max MacBook Pro at 1.00 tok/s, with 376s to first token on 512 tokens.
How well do agents use tests when you only name the technique?
Dan Luu ran 26 prompt conditions and 4 skills at 80 runs each on a Zstd eval: naming a test technique rarely beat giving the agent no instructions.
vLLM speculative decoding on AMD ROCm: five draft methods, no single speedup number
vLLM tested native MTP, Gemma 4 MTP, EAGLE-3, DFlash and DSpark on MI300X and MI355X under ROCm, and reports no single throughput speedup number.
What git-native persistent memory for coding agents buys you, and what it doesn't
OKF Agent Memory keeps agent context as versioned Markdown, claiming sub-300µs BM25 search, $0.00 retrieval cost and 80% less token bloat, no recall data.
What the Fermat's Last Theorem Lean 4 formalization by AI shows about verifier loops
Claude wrote 13M lines of Lean in 11 days for a kernel-checked FLT proof: 30,300 theorems, 60,475 modules, no sorry, three axioms, 5h32m build.
musl with mimalloc is still 26% slower than glibc on a 4-core box
Brokk benchmarked its Rust service Bifrost on 4-core EC2 VMs: musl with mimalloc is still 26% slower than glibc, so musl was dropped as a prebuilt option.
Mojo's compiler goes Apache 2.0 while MAX stays source-available
Mojo 1.0's compiler and toolchain are now Apache 2.0 with LLVM exceptions. MAX is source-available, but kernel work still needs a prebuilt compiler.
Rust Gets Native GPU Offload via rustc and LLVM Backends
Drehwald et al. present a Rust-native GPU offload framework on LLVM Offload. It matches CUDA/HIP kernel performance on RAJAPerf without unsafe pointers.
What a single-model Metal engine buys you over llama.cpp on Apple Silicon
antirez's h3.c runs MiniMax-H3 on hand-written Metal for Apple Silicon; a macOS VM capability shim made llama.cpp 11.08x faster at prompt processing.
Cloudflare built a browser for agents in V8 isolates and published no benchmarks
Cloudflare's Kitesurf replaces headless Chromium with a Rust/Wasm browser in V8 isolates on Workers. No CPU, memory or latency figures published.
Other topics
Hiring for AI or ML?
I am open to AI/ML Engineering, Data Science, and Python roles, plus research collaborations and consulting. New York based, shipping worldwide.