Scale By the Bay Scale By the Bay

Thursday, October 28, 2021

Shape safety in tensor programming is easy for a theorem prover
Peng Cheng
Peng Cheng
Schedule One, Lead Engineer

We present shapesafe ( - the most comprehensive compile-time verifier for scala linear algebra - by only exploiting scala's type system as a theorem prover. This new paradigm allows type-level tensor computations, even those as complex as composite neural network blocks, to be rewritten, simplified and verified while being written. We will talk about its design and limitations, and most important, what we have observed and learned from it