How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Neural ODEs and continuous normalizing flows — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Automatic differentiation and computational graphs
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Discrete continuous and pde adjoint sensitivities
- Euclidean Ordinary Differential Equations with Smooth Dependence
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Neural ODEs and continuous normalizing flows
- Order, Zorn's Lemma, and the Axiom of Choice
- Outward rounded interval and ball arithmetic
- Picard-Lindelöf and First-Order Ordinary Differential Equations
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Inverse and Implicit Function Theorems
- The Riemann Integral: Definition and Integrability
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Logical flowchart
3 · Definitions, theorems and proofs
None yet.
4 · Examples, counterexamples and false statements
A finite Euler adjoint gradient can differ from the exact flow gradient
Example
On , consider the two-rate linear neural ODE , with and objective , for in a neighborhood of . At , the decay rates are and . The exact continuous-flow gradient is . For the fixed-step Euler solver with and equal steps, its step count is the resolution setting; the finite computational graph has output and exact discrete adjoint gradient . Thus changing the solver resolution from to changes the finite gradient from to . These values are exact for this finite calculation and assert no general solver-error or continuous-versus-discrete gradient bound.
Example references
Facts & Assumptions
Given: , , , terminal loss , and the -step forward Euler graph for with .
A parameterized neural ordinary differential equation: a parameterized ODE is the initial-value problem with specified initial state; the neural specialization additionally specifies a finite acyclic network for the field. Here two identity-activation output nodes with input weights and , zero biases, and unused time input realize .
A globally Lipschitz neural ODE has a global smooth flow: the stated smooth uniformly globally Lipschitz field has a unique smooth flow on the full finite interval.
Exact continuous adjoint sensitivity for a neural ODE: the continuous procedure solves the terminal adjoint equation and returns its initial, terminal, running, and vector-field parameter contributions.
The continuous ODE adjoint gives the parameter gradient with endpoint terms: under common-tube and C1 objective hypotheses, the continuous adjoint expression is the exact derivative of the continuous objective.
Finite parameterized state-step graphs and objectives: C1 initial and step maps together with a C1 terminal/running objective define one finite real-arithmetic graph and its reduced objective.
The reverse recursion is the exact gradient of a finite state-step objective: the backward recursion returns the exact gradient of that finite C1 graph.
The real exponential function and the number by a power series: and is the real exponential function.
The exponential function is smooth and : is smooth and .
The exponential is positive and satisfies : for every real .
Sum, product, quotient, and chain rules from difference quotients: the sum, product, chain, and positive-integer power rules apply to the differentiable functions used below.
The exponential addition formula : for real .
Take and , and set . The field is jointly . For every nonempty compact , and give the required state-Lipschitz and origin bounds; the empty compact case is vacuous. By [F7, F8], the exact solution is continuous on the compact set , so its trajectory tube is compact. For the continuous adjoint, take on the open set and on the open set . These objectives are , and their first derivatives are constant, hence bounded and uniformly continuous on the terminal slice and common trajectory tube. Thus the continuous and finite adjoint supplier hypotheses hold.
Verification
By [F7, F8, F10], and satisfy the displayed ODE and initial data. By [F2] this is the unique flow, so and .
The Euler transition is the C1 map . It is a finite state-step objective as in [F5], and induction gives . By [F10], differentiating this polynomial gives ; by [F6], the finite discrete adjoint returns exactly this derivative.
For the continuous adjoint, , , and solves the terminal adjoint equation by [F8, F10]. Substituting into [F4] gives by [F11], which is also the output expression defined by [F3].
At , gives , while gives . By [F9], , so both finite gradients differ from the exact continuous gradient; the two finite gradients also differ from each other. This establishes only the stated finite witness, not a general error bound.
Sources
- Ricky T. Q. Chen, Yulia Rubanova, Jesse Bettencourt, and David Duvenaud, Neural Ordinary Differential Equations, §2 and Appendix B
- George Papamakarios, Eric Nalisnick, Danilo Jimenez Rezende, Shakir Mohamed, and Balaji Lakshminarayanan, Normalizing Flows for Probabilistic Modeling and Inference, §§4.2.1–4.2.2