Lean Verified Precision

In A Fix for Softmax and Cross-Entropy, the authors describe a numerical bug in code widely used to train neural networks. The issue appears in standard PyTorch and JAX implementations. It also illustrates a limitation of proofs over real numbers: they do not, by themselves, bound floating-point error. For related discussion, see this thread from ezyang (your favorite blogger's favorite blogger). My guess is that similar problems plague many parts of the deep learning stack; for example, this paper describes how limited precision can hide small parameter updates.

Luckily, this doesn't have to be the case. Formal verification can catch this problem when numerical accuracy is part of the specification. In this blog post, we start from first principles and build up the tools for catching precision bugs. No knowledge about systems or precision is assumed, although you will need to read some math. The code is generated, and the proofs are checked by Lean. This is the fifth post in a series on Lean for deep learning.

• Sasha Rush and Robert George

Approximation and Relative Precision

Before diving into neural networks, let us formalize a notion of numerical approximation. There are several ways to do this, each with its own benefits and issues. We'll follow the exposition of Zielinski and Hsu and use Olver's Relative Precision (RP). We express an approximation to a true value using a multiplicative factor, with its logarithm bounded in magnitude by epsilon:

\widehat{x}=x e^\delta,\qquad |\delta|\le\varepsilon

For positive values, relative precision measures the approximation error. We also define the distance from zero to itself to be zero:

\begin{aligned}\operatorname{RP}(x,\widehat{x})&=\left|\log\frac{\widehat{x}}{x}\right|\\\operatorname{RP}(0,0)&=0\end{aligned}

The same logarithmic formula applies to two negative values. If exactly one value is zero, or the signs differ, RP is infinite. We will use the following Lean predicate to express a finite RP bound.

On positive values, relative precision forms a metric. Its triangle inequality lets us combine approximation bounds across successive steps.

\begin{aligned}&\operatorname{RP}(x,z)=\left|\log\frac{z}{x}\right|\\&\quad=\left|\log\frac{y}{x}+\log\frac{z}{y}\right|\\&\quad\le\operatorname{RP}(x,y)+\operatorname{RP}(y,z)\end{aligned}

Here are the core properties we will use for positive values.

Our key theorems allow us to propagate relative precision through arithmetic operators. For example, dividing two approximations leads to additive precision loss.

\varepsilon_{\div}\le\varepsilon_x+\varepsilon_y

Adding positive numbers gives an RP bound at most as large as the larger input bound.

\varepsilon_{+}\le E=\max(\varepsilon_x,\varepsilon_y)

The sum's approximation ratio is a weighted average of the input ratios, so it stays in the same shaded interval.