Alphabeta Math
Pipeline-generated
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.

✓ 1 result · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Neural ODEs and continuous normalizing flows — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A finite Euler adjoint gradient can differ from the exact flow gradient

Example

On [0,1], consider the two-rate linear neural ODE u1′(t)=−u1(t), u2′(t)=θu2(t) with u(0)=(1,1) and objective J(θ)=u2(1;θ), for θ in a neighborhood of −100. At θ=−100, the decay rates are 1 and 100. The exact continuous-flow gradient is J′(−100)=exp⁡(−100). For the fixed-step Euler solver with N∈N and N≥1 equal steps, its step count N is the resolution setting; the finite computational graph has output JN(θ)=(1+θ/N)N and exact discrete adjoint gradient JN′(−100)=(1−100/N)N−1. Thus changing the solver resolution from N=50 to N=100 changes the finite gradient from −1 to 0. These values are exact for this finite calculation and assert no general solver-error or continuous-versus-discrete gradient bound.

Facts & Assumptions

Given: T=1, u(0)=(1,1), vθ(t,u)=(−u1,θu2), terminal loss u2(1), and the N-step forward Euler graph for N∈N with N≥1.

[F1]

A parameterized neural ordinary differential equation: a parameterized ODE is the initial-value problem u˙=vθ(t,u) 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 (−1,0) and (0,θ), zero biases, and unused time input realize vθ(t,u)=(−u1,θu2).

[F2]

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.

[F3]

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.

[F4]

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.

[F5]

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.

[F6]

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.

[F7]

The real exponential function and the number e by a power series: e=exp⁡(1) and exp⁡ is the real exponential function.

[F8]

The exponential function is smooth and (exp⁡)′=exp⁡: exp⁡ is smooth and (exp⁡)′=exp⁡.

[F10]

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.

[F11]

The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y): exp⁡(x+y)=exp⁡(x)exp⁡(y) for real x,y.

[A1]

Take I=Θ=U0=R and Ω=(−101,−99), and set u0(η)=(1,1). The field v(t,u,η)=(−u1,ηu2) is jointly C∞. For every nonempty compact K⊆R, LK=max⁡{1,sup⁡η∈K∣η∣} and MK=0 give the required state-Lipschitz and origin bounds; the empty compact case is vacuous. By [F7, F8], the exact solution uη(t)=(exp⁡(−t),exp⁡(ηt)) is continuous on the compact set [0,1]×Ω‾, so its trajectory tube is compact. For the continuous adjoint, take ϕ(u,η)=u2 on the open set Uϕ=R2×R and ℓ(t,u,η)=0 on the open set Uℓ=R×R2×R. These objectives are C1, 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

1.1A1F1F2F7F8F10givenalgebra

By [F7, F8, F10], u1(t)=exp⁡(−t) and u2(t)=exp⁡(θt) satisfy the displayed ODE and initial data. By [F2] this is the unique flow, so J(θ)=exp⁡(θ) and J′(−100)=exp⁡(−100).

1.2F5F6F10giveninductionalgebra

The Euler transition is the C1 map Ψk(u,θ)=((1−1/N)u1,(1+θ/N)u2). It is a finite state-step objective as in [F5], and induction gives u2,N=(1+θ/N)N. By [F10], differentiating this polynomial gives (1+θ/N)N−1; by [F6], the finite discrete adjoint returns exactly this derivative.

2.1A1F3F4F8F10F11step 1.1algebra

For the continuous adjoint, Duv=diag⁡(−1,θ), p(1)=(0,1), and p(t)=(0,exp⁡(θ(1−t))) solves the terminal adjoint equation by [F8, F10]. Substituting into [F4] gives ∫01exp⁡(θt)exp⁡(θ(1−t)) dt=∫01exp⁡(θ) dt=exp⁡(θ) by [F11], which is also the output expression defined by [F3].

3.1F9step 1.1step 1.2algebra∎

At θ=−100, N=50 gives (1−2)49=−1, while N=100 gives (1−1)99=0. By [F9], exp⁡(−100)>0, 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