Alphabeta Math
AlgorithmAlgorithm: Literature-sourcedProof: Not applicablePipeline-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.

Backpropagation through a finite shared-parameter recurrence

Definition

Let p,q≥1, let Θ⊆Rp and H⊆Rq be open, let T≥0 be an integer, and fix θ∈Θ. A map is continuously differentiable here when it is totally differentiable at every point of its open domain and its derivative matrix varies continuously there. A finite shared-parameter recurrence consists of an initial-state map h0:Θ→H, transition maps Φt:Θ×H→H for t=1,…,T, and a scalar loss ℓ:Θ×H→R, all continuously differentiable on open domains containing the evaluated inputs. Put h0=h0(θ), ht=Φt(θ,ht−1), and J(θ)=ℓ(θ,hT). A fixed collection of external inputs, such as the observations at successive time steps, may be built into the maps Φt. The same parameter vector θ is supplied to every transition.

For each map, its registered local derivative is the total derivative with respect to the indicated variable while the other displayed variables are held fixed. Transposes are Euclidean adjoints for the stated coordinate inner products. Evaluate and store h0,h1,…,hT. If a map is undefined, return DOMAIN_ERROR. For piecewise-C1 maps, use only the derivative on a unique strict active branch; if any evaluated input lies on a branch boundary or has ambiguous branch selection, return NONDIFFERENTIABLE and no gradient.

Initialize λT=(Dhℓ(θ,hT))T and g=(Dθℓ(θ,hT))T. For t=T,T−1,…,1, set At=DθΦt(θ,ht−1), Bt=DhΦt(θ,ht−1), then update

g←g+AtTλt,λt−1=BtTλt.

After the reverse sweep, set g←g+(Dh0(θ))Tλ0 and return (J(θ),g). For T=0, the reverse loop is empty and the same initialization and final update apply. All derivative calculations in this procedure are real-arithmetic operations on the specified maps; no floating-point accuracy guarantee is asserted.

The diagram shows the finite unrolling: arrows point from an input value to the operation that uses it. The single θ node feeds each transition and the loss, so the reverse updates add all of those contributions into the same accumulator g; the ht cotangents flow from right to left. The diagram illustrates the algorithm, and no correctness proof relies on it.

µh0(µ)©1h1©2¢¢¢©ThT`(µ;hT)

Remarks

This is a mathematical real-arithmetic procedure. A floating-point implementation may round its primal values and local derivatives; the definition supplies no numerical error estimate.

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources