Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.36396

Automatic Certified Differentiation in Lean

Ramy Shahin
View original source ↗Read source document ↗Export metadata ↓

Abstract

Automatic differentiation (the automatic computation of numerical function derivatives) has many applications, especially in scientific computing and machine learning. Several approaches to automate the calculation of derivatives have been presented. Common challenges facing those approaches include (1) having to define derivative rules for different classes of functions, (2) having to manipulate program symbols to understand the semantics of the function being differentiated, and construct the derivative function, and (3), more importantly, ensuring that the calculated derivative is correct. In this paper, we present an approach for automatic \emph{certified} differentiation using the Lean proof assistant. By certified, we mean a correctness certificate is computed together with the derivative function and a domain on which the derivative is guaranteed to be valid. Our approach leverages existing derivative theorems included in the Mathlib Lean library instead of having to define our own rules. We also utilize Lean metaprogramming to manipulate the symbolic structure of the input function, and to construct the derivative function. The correctness certificate is computed step-wise as we apply Mathlib theorems. To make the search efficient, we index the derivative theorems by the function they differentiate. We evaluate our approach on 500 randomly generated functions: with the index, all of them are differentiated, with a median time of 0.18\,s per function, 8.6 times faster than without the index.

Explore related subjects

cs.SCcs.MS

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Ramy Shahin. 2026-10-26. Automatic Certified Differentiation in Lean. https://arxiv.org/abs/2610.36396

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

GPU-Accelerated Search for Fast Matrix Multiplication over $\mathbb{F}_2$

We present a GPU-accelerated algorithm for searching for ways to multiply matrices with few scalar multiplications. Our algorithm searches the matrix multiplication flip graph and, on an NVIDIA H200, performs over a billion search steps per second for matrix sizes up to $7\times7$, a roughly $380\times$ improvement over previous GPU-accelerated search on the tensor for $7\times7$ matrix multiplication. We also prove that, over \(\mathbb{F}_2\), the directed matrix multiplication flip graph is strongly connected with only flip and plus edges. This removes the need for computationally expensive reduction edges in the connectivity argument used by previous work. Using this GPU-accelerated search procedure on our simplified flip graph, we find a way to multiply $7\times 7$ matrices over $\mathbb{F}_2$ using 245 multiplications, a three-multiplication improvement over the previous record.

cs.SC↗
arXiv2026

One Loss Resolves Signed Rank-One Gradient Fibers: Exact Decoding on Cycle and Theta Blocks

For masked rank-one least squares with unrestricted signs, gradients reveal weighted margins and the loss reveals the target's squared norm. We prove that this one scalar resolves the gradient ambiguity on bipartite cycle and length-three parallel-path blocks: every target fixed before sampling and nonzero on cycle edges is identified almost surely by one legal positive query drawn from an absolutely continuous law. On six-cycle flowers, open target and query sets retain $3^r$ bounded gradient candidates. A common algebraic witness excludes cross-block energy cancellation. Cactus masks admit explicit exception certificates and target-uniform finite-grid bounds; theta blocks admit an existence guarantee. For nondegenerate cactus reductions, an exact decoder returns complete actual real lists, with bit cost polynomial in input length, the cycle-degree product $D$ and the optional budget parameter $2^κ$. Energy-coordinate propagation certifies singletons without a product join. The product $D$ can grow exponentially in cycle count. Exponential certificate-degree and output bounds, and weak NP-hardness at a fixed uniform query, characterize distinct costs of exact decoding.

cs.SC↗
arXiv2026

Deterministic Root-Finding over Finite Fields with Elliptic Curves

Finding the roots of a polynomial over a finite field $\mathbb F_q$ in deterministic polynomial time is a long-standing open problem. Classical deterministic methods work in the multiplicative group $\mathbb F_q^\times$ and are efficient only when $q-1$ is smooth, which is rarely the case. We propose a method that replaces $\mathbb F_q^\times$ by the groups of rational points of an elliptic curve $E$ and of its quadratic twist $\widetilde E$. The computation splits into an offline phase, which depends only on $\mathbb F_q$ and outputs a short \emph{elliptic preprocessing datum} $\mathcal D$, and an online phase, which processes the input polynomial. Writing $Ξ(\mathcal D)$ for the largest prime factor of $\lvert E(\mathbb F_q)\rvert\cdot\lvert\widetilde E(\mathbb F_q)\rvert$, the online phase is deterministic and finds the roots of any $f\in\mathbb F_q[X]$ of degree $n$ within $\widetilde O(Ξ(\mathcal D)^2\,n\log^2 q+n^ω\log q+n\log^3 q)$ operations in $\mathbb F_q$. A precursor of our method is an algorithm by Rónyai, which recovers the roots through Galois computations over number fields, relies on GRH, and comes with a polynomial bound of unspecified degree; in contrast, our online phase works entirely over $\mathbb F_q$ and is unconditional. Moreover, $\mathcal D$ can be certified deterministically and unconditionally in time polynomial in $\log q$ and $Ξ(\mathcal D)$. We conjecture that every $\mathbb F_q$ of large enough characteristic admits a datum with $Ξ(\mathcal D)\leq(\log q)^{O(1)}$, and support this with a heuristic and with experiments. Constructing such a datum in polynomial time remains open.

cs.SC↗