Correctness is Demanding, Performance is Frustrating

TL;DR

This paper presents a method to develop high-performance applications with correctness guarantees by using a theorem prover to derive specifications and extract efficient code, demonstrated through a tensor framework for neural networks.

Contribution

It introduces a framework that combines formal specification and automatic code extraction for high-performance, correct neural network computations.

Findings

Generated code matches hand-optimized performance

Framework ensures correctness invariants are maintained

Demonstrated on a multi-core machine with tensor applications

Abstract

In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. We use a theorem prover to derive a high-level specification of the application that includes correctness invariants of our choice. After that, within the same theorem prover, we implement an extraction of the specified application into a high-performance language of our choice. Concretely, we are using Agda to specify a framework for automatic differentiation (reverse mode) that is focused on index-safe tensors. This framework comes with an optimiser for tensor expressions and the ability to translate these expressions into SaC and C. We specify a canonical convolutional neural network within the proposed framework, compute the derivatives needed for the training phase and then demonstrate that the generated code matches the performance of hand-written code when running on a multi-core machine.