ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

Gradient descent can stay at a non-global stationary point

Example

For the scalar objective $J (θ) = (θ^{2} - 1)^{2}$ , the global minimum value is $0$ and is attained at $θ = \pm 1$ , while $θ = 0$ is stationary with $J (0) = 1$ . Gradient descent $θ_{k + 1} = θ_{k} - η J^{'} (θ_{k})$ initialized at $θ_{0} = 0$ remains at $0$ for every step size $η > 0$ . Thus a theorem about global minimizers does not by itself imply that a gradient-based training procedure finds one.

Example references

Shin et al., Introduction: the analysis idealizes global minimizers and does not prove optimizer convergence

Shin et al., Introduction: no general optimizer guarantee is asserted

Facts & Assumptions

Given: The polynomial objective and gradient-descent update in the Example.

[F1]

$J^{'} (θ) = 4 θ (θ^{2} - 1)$ by polynomial differentiation.

Verification

Proof strategy: compare objective values and evaluate the update at zero.

1.1givenalgebra

Since $J (θ)$ is a square, $J (θ) \geq 0$ , with equality exactly when $θ^{2} = 1$ . Also $J (0) = 1$ . Hence $0$ is not a global minimizer.

2.1givenF1algebrainduction∎

By [F1], $J^{'} (0) = 0$ . If $θ_{k} = 0$ , the update gives $θ_{k + 1} = 0 - η J^{'} (0) = 0$ ; induction from $θ_{0} = 0$ yields $θ_{k} = 0$ for all $k$ . The iterates therefore never reach either global minimizer.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

Shin, Darbon, and Karniadakis, On the Convergence of Physics-Informed Neural Networks for Linear Second-Order Elliptic and Parabolic Type PDEs (standard reference, not scraped)