Source-linked AI summary
Automatic Certified Differentiation in Lean
Ramy Shahin
TL;DR
Automating derivatives requires constructing derivative functions and establishing their correctness. This paper uses Lean metaprogramming to apply Mathlib derivative theorems compositionally and return a derivative with a validity domain and proof. On 500 generated functions, indexing made differentiation 8.6 times faster at the median, with all cases completing.
Problem
Automatic differentiation must construct derivative functions while addressing the challenge of ensuring their correctness.
Source: §1 · pp. 1, 3Method
Lean metaprogramming follows input-function structure to compose Mathlib derivative theorems and return a derivative, validity domain, and correctness proof.
Source: §1 · p. 3Results
0.18 s median time per function across 500 randomly generated functions, with indexing 8.6 times faster than without the index.
Source: §1 · p. 3Takeaways & Limitations
The approach handles functions whose derivatives are valid only on restricted domains and returns a sufficient input condition for validity.
Source: §8 · p. 16A generated domain can be unsatisfiable, making its correctness theorem vacuously true and the certificate unusable, though not incorrect.
Source: §6 · p. 13
Abstract
from arXiv · showhide
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.
1 Introduction
The introduction motivates automatic differentiation and presents a Lean framework that derives functions compositionally from Mathlib theorems while constructing correctness proofs. It also reports faster indexed search across 500 generated functions.
1 Introduction
- The paper motivates automated differentiation through applications including scientific computing, machine learning, simulation, graphics, and computational finance.Automated differentiation has been an active research area since the 1960s.Source: §1 · p. 1
- Symbolic differentiation follows the syntax tree of a function and composes primitive derivative theorems, unlike algorithmic differentiation, which computes a derivative value at one input.For log(3/x), the chain and quotient rules yield derivative −1/x, restricted to x ≠ 0.Source: §1 · p. 2
- Lean and Mathlib supply formal derivative theorems, kernel proof checking, and metaprogramming for manipulating function syntax and extending Lean with commands.The paper identifies these as the three ingredients needed for its system.Source: §1 · p. 3
- The framework returns a derivative, a domain where it is valid, and a correctness proof checked by the Lean kernel.It composes existing Mathlib derivative theorems following the input function's structure.Source: §1 · p. 3
- Differentiation with the index had a median time of 0.18 s per function, making it 8.6 times faster than differentiation without the index.Source: §1 · p. 3
2 Background
The background introduces Mathlib's derivative formalization and Lean's proof-metaprogramming model. The framework uses one-dimensional derivatives and Lean metavariables to construct derivative goals and proofs.
2.1 Differentiation in Mathlib
- The framework uses Mathlib's one-dimensional derivatives, restricting its scope to functions of a single variable.Mathlib also has a formalization of Fréchet derivatives.Source: §2.1 · p. 4
- HasDerivAt relates a function, its derivative, and an input point; Mathlib's derivative theorems encode required preconditions as premises.For the logarithm rule, a premise restricts the function argument to non-zero values, and the automatic system must provide such input constraints.Source: §2.1 · p. 5
2.2 Lean Metaprogramming
- Lean represents each proof goal as a metavariable whose type must receive a well-typed term before the kernel accepts the proof.Metavariables can also serve as holes that unification fills with type-sound assignments.Source: §2.2 · p. 5
- The derivative search uses metavariables for the unknown derivative and domain, which Lean's unification algorithm fills while applying theorems.The goal has the form HasDerivAt f (?d x) x under the domain predicate ?a x.Source: §2.2 · p. 6
3 Automatic Certified Differentiation Algorithm
The algorithm finds a derivative while collecting the domain constraints needed to certify it, then completes the proof using those constraints. It returns a derivative, a validity domain, and a proof of correctness.
3 Automatic Certified Differentiation Algorithm
- The algorithm aims to produce a derivative function, a predicate specifying where it is valid, and a proof that it satisfies HasDerivAt on that domain.The correctness theorem has the form ∀x, a x → HasDerivAt f (f' x) x.Source: §3 · p. 6
3.1 Derivative Search
- The algorithm searches for a derivative by recursively applying applicable derivative theorems to the current goal, while tracking prior goals to prevent infinite recursion.Constant functions are handled directly; otherwise, failed theorem applications are undone and the next candidate is tried.Source: §3.1 · p. 7
- The search collects non-derivative side conditions as domain constraints and leaves corresponding holes in the proof for later completion.Recursive HasDerivAt subgoals are searched for their own derivatives and constraints.Source: §3.1 · p. 7
3.2 Domain Completion
- Domain completion conjoins the collected constraints and fills each proof hole using the matching conjunct from the domain hypothesis.The resulting correctness proof applies wherever the constructed domain predicate holds.Source: §3 · p. 6, §3.2 · p. 8
4 Implementation
The implementation exposes differentiation as a Lean command that produces a CDeriv structure, and searches derivative theorems using an index keyed by the function being differentiated. In the log(3/x) example, proof holes for domain conditions are completed from the computed domain.
4.1 Design Decisions
- The differentiate command unfolds the input function and produces a CDeriv containing its derivative, validity domain, and correctness proof.Lean's metaprogramming is used because a Lean function cannot inspect the syntax of its argument; the resulting definition is checked by the Lean kernel.Source: §4.1 · p. 8
4.2 Theorem Indexing
- The theorem index excludes catch-all rules and groups the remaining derivative theorems by the differentiated function's head symbol, reducing costly failed applications.For each goal, search tries the matching head-symbol theorems together with theorems whose head symbol is not fixed.Source: §4.2 · p. 9, §4.1 · p. 9
4.3 Example
- For log(3/x), the tactic derives the quotient-rule condition x ≠ 0 and the logarithm condition 3/x ≠ 0, then fills each proof hole from their conjunction.The derivative is not simplified, but on its computed domain it equals −1/x.Source: §4.3 · p. 10
5 Evaluation
On 500 randomly generated real functions, theorem indexing improved completion and reduced differentiation time compared with searching without the index. The evaluation also checked the computed domains against sampled points.
Evaluation Setup
- 500 test functions spanned 4 to 67 expression-tree nodes, and the evaluation compared indexed and unindexed runs under a 200,000 heartbeat limit.The functions were randomly generated from a limited grammar and restricted to R → R.Source: §5 · pp. 10–11
Results
- 8.6× median speedup: indexing reduced median differentiation time from 2.4 s to 181 ms across the 488 cases completed in both configurations.With indexing, all 500 cases completed; without it, 12 hit the Lean heartbeat limit, while indexed runs for those cases took at most 0.6 s.Source: §5 · pp. 11–12, Table 1 · p. 11, Figure 6 · p. 12
- The index's speedup increased with function size and was larger for restricted-domain functions than universal-domain functions, with median speedups of 13.8× and 5.9×, respectively.The figure plots time against expression-tree size and plots per-case speedup by domain type.Source: §5 · p. 12, Figure 6 · p. 12
Domain Checks
- All but one of the 433 restricted domains held at one or more of 4,000 sampled points in [−20, 20]; the exception's correctness theorem held vacuously.Computed domain conjuncts were non-zero conditions, including denominators, logarithm arguments, and cosine arguments of tan.Source: §5 · p. 12
6 Discussion
The framework supports functions beyond the evaluated grammar when suitable derivative and composition theorems are available, but its computed domain is sufficient rather than necessarily weakest. The theorem index substantially reduces search time, while further optimizations and extensions remain possible.
Generality
- The evaluated grammar is limited, although the framework can use imported derivative theorems beyond it; multivariable derivatives require extending the command.Piecewise functions need derivative theorems holding on parts of the domain, which HasDerivAt can accommodate at a point.Source: §6 · p. 13
Soundness and Precision of Side Conditions
- The collected domain is a sufficient, not necessarily weakest, differentiability precondition because side conditions follow syntax rather than function semantics.A domain predicate can even be unsatisfiable, making the correctness theorem vacuously true; the example 1/(x−x) is constant under total division in Mathlib.Source: §6 · p. 13
- Simplifying domains or searching for witnesses could reject or identify nonempty domains, but proving the domain maximal is outside the paper’s scope.A stronger guarantee would be a nonempty open domain, ensuring validity near some point.Source: §6 · p. 13
Performance and Further Optimizations
- The theorem index cut attempted applications for the same function from 1970 to 79; across the test set, differentiation was 8.6 times faster for the median test case, with no timeouts.Source: §6 · p. 14
- Further search optimizations include whole-function discrimination trees, cheaper reducible-only unification with fallback, and syntactic normalization.Some derivations rely on unfolding arithmetic-operation instances, so reducible-only unification would need a fallback to full unification.Source: §6 · p. 14
Beyond Differentiation
- The framework’s compositional proof construction relies on derivative uniqueness, which ensures confluence of the stepwise proof tree.The discussion presents generalizing the approach to other compositional computations and their preconditions as a future direction.Source: §6 · p. 14
7 Related Work
Related approaches automate differentiation through tactics, conversions, or formal correctness analyses. This work instead searches imported Mathlib theorems and returns a derivative, explicit domain, and closed certificate as a Lean command.
Related Work
- Mathlib’s fun_prop and SciLean’s fun_trans use derivative rules, while this approach infers side conditions and computes the derivative’s valid domain.Earlier Datalog-in-Lean work required user-listed theorems and derivatives valid everywhere; this approach finds applicable theorems automatically and computes the domain.Source: §7 · p. 15
- Unlike other proof-assistant approaches that leave hypotheses or residual goals, this approach packages the derivative, explicit domain, and closed proof in one CDeriv object.It searches imported HasDerivAt theorems and exposes differentiation as a top-level command; it certifies each result rather than verifying the differentiation procedure once and for all.Source: §7 · p. 15
- HOL4, Isabelle/HOL, and Coq also use theorem-driven structural differentiation, while PVS has an automated continuity checker.These systems may carry side conditions as hypotheses or residual goals.Source: §7 · p. 15
- Other formal correctness work studies AD semantics, nondifferentiable cases, or static bug analysis; this approach composes Lean-checked mathematical theorems.Surveys have also covered AD forms, flaws in existing systems, and developer pitfalls.Source: §7 · pp. 14–16
- The paper situates certified programming within broader theorem-prover applications, including CompCert, seL4, and formalized authorization and assurance-case work.Source: §7 · p. 16
8 Conclusion
The paper concludes that its Mathlib-based approach computes derivatives with correctness certificates and sufficient validity predicates. In tests, theorem indexing accelerated the median case by 8.6 times and reached up to 71 times faster, while current support remains first-order and one-dimensional.
8 Conclusion
- 8.6 times faster for the median test case and up to 71 times faster with theorem indexing; the approach handled relatively complex functions, including restricted-domain cases.Source: §8 · p. 16
- The implementation supports only first-order, one-dimensional derivatives; higher-order, partial, and multidimensional derivatives are possible extensions.The computed domain is sufficient for validity but not necessarily largest; proving it non-empty or open would make certificates more informative.Source: §8 · p. 16
- Extending correctness to numerical implementations would require formalizing approximation bounds for fixed-point or floating-point representations.Source: §8 · p. 16