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.
Full-memory and limited-memory storage costs
Example
Compare the paired Hessian/inverse state used by the full-memory algorithm with the correction-pair storage in L-BFGS for variables and memory length .
Facts & Assumptions
Given: , , a full BFGS matrix, and the limited-memory state of Limited-memory Bfgs two-loop recursion with curvature filtering.
The L-Bfgs two-loop recursion equals the stored inverse updates and costs linear memory work: L-BFGS stores at most pairs of length- vectors and uses work for the two-loop recursion.
Full-memory Bfgs with Wolfe search, descent reset, and Powell damping: this fully explicit implementation maintains both consistent dense matrices and .
Limited-memory Bfgs two-loop recursion with curvature filtering: the working vectors have length and the stored memory is capped at pairs.
Bfgs curvature pairs and Hessian/inverse updates: the direct update is , and the inverse update is , with .
Verification
Each dense matrix contains real entries. The paired state in [F3] therefore stores matrix entries; a one-matrix implementation stores .
The L-BFGS pair list contains at most real coordinates, plus temporary vectors and scalars.
In exact inverse-matrix mode, computing uses one dense matrix-vector product and costs scalar operations. For the direct update, first compute with one dense matrix-vector product; since is symmetric, . Then form using two outer products and an entrywise matrix update, which costs . For the inverse update, first compute with one dense matrix-vector product and expand [F4] using symmetry of to obtain This uses a constant number of outer-product updates and also costs . Thus the dense direction and the paired BFGS updates use work per iteration. By [F1], the two-loop recursion uses scalar work. Here while ; the paired representation uses 100 times as many matrix entries as correction-pair coordinates, and a one-matrix representation uses 50 times as many. These are storage comparisons, not exact operation totals.
Remarks
The example compares storage and update work only. It does not infer that L-BFGS has the same convergence rate as full BFGS; its convergence result requires separate curvature and scale bounds.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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
- Jorge Nocedal and Stephen J. Wright, Numerical Optimization, 2nd ed. (standard reference, not scraped)
- Dong C. Liu and Jorge Nocedal, On the limited memory BFGS method for large scale optimization (standard reference, not scraped)