Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck pass
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 n=1000 variables and memory length m=10.

Facts & Assumptions

Given: n=1000, m=10, a full n×n BFGS matrix, and the limited-memory state of Limited-memory Bfgs two-loop recursion with curvature filtering.

[F1]

The L-Bfgs two-loop recursion equals the stored inverse updates and costs linear memory work: L-BFGS stores at most m pairs of length-n vectors and uses O(mn) work for the two-loop recursion.

[F3]

Full-memory Bfgs with Wolfe search, descent reset, and Powell damping: this fully explicit implementation maintains both consistent dense matrices Bk and Hk.

[F2]

Limited-memory Bfgs two-loop recursion with curvature filtering: the working vectors have length n and the stored memory is capped at m pairs.

[F4]

Bfgs curvature pairs and Hessian/inverse updates: the direct update is B+=B−BssTB/(sTBs)+yyT/(sTy), and the inverse update is H+=(I−ρsyT)H(I−ρysT)+ρssT, with ρ=(sTy)−1.

Verification

1.1givenF3algebra

Each dense matrix contains n2=10002=1,000,000 real entries. The paired state in [F3] therefore stores 2n2=2,000,000 matrix entries; a one-matrix implementation stores n2=1,000,000.

1.2givenF1F2algebra

The L-BFGS pair list contains at most 2mn=2⋅10⋅1000=20,000 real coordinates, plus O(n+m) temporary vectors and scalars.

2.1givenF1F3F4algebra∎

In exact inverse-matrix mode, computing p=−Hg uses one dense matrix-vector product and costs O(n2) scalar operations. For the direct update, first compute u:=Bs with one dense matrix-vector product; since B is symmetric, BssTB=uuT. Then form B+=B−uuT/(sTu)+yyT/(sTy) using two outer products and an entrywise matrix update, which costs O(n2). For the inverse update, first compute v:=Hy with one dense matrix-vector product and expand [F4] using symmetry of H to obtain H+=H−ρ(svT+vsT)+(ρ+ρ2yTv)ssT. This uses a constant number of outer-product updates and also costs O(n2). Thus the dense direction and the paired BFGS updates use O(n2) work per iteration. By [F1], the two-loop recursion uses O(mn) scalar work. Here mn=10,000 while n2=1,000,000; 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