AI Proof WatchKeep up with AI contributions

An Improved Last-Iterate Convergence Rate for Anchored Gradient Descent Ascent

Anja Surina, Arun Suggala, George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Francisco J. R. Ruiz, Pushmeet Kohli, Swarat Chaudhuri

For smooth convex-concave objectives with a monotone K-Lipschitz gradient operator and a saddle point, the schedule αₜ=1/(K√(t+γ)), βₜ=γ/(t+γ), γ≥2, gives squared-gradient residual O(1/t) at the last iterate of anchored gradient descent-ascent.

Sources for this record

What was already known

The 2019 analysis obtained O(1/t^(2−2p)) for 1/2<p<1 and left the O(1/t) boundary open under these assumptions.

AI involvement AI-autonomous

The paper and Surina credit AlphaProof Nexus with discovering the schedule and proof. Human authors present the discrete argument; Gemini assisted informalization.

The original paper and Surina's first-person account say the agent discovered the new schedule and proof, with no human-supplied mathematical step beyond setting the task documented.

Importance Notable

Closes that rate gap for anchored GDA.

Limitations

A later Lean theorem proves the asymptotic O(1/t) rate with an unspecified constant and explicit slack. It does not certify the paper’s sharper displayed constant; no complete human proof check is documented.

Technical verification Formal (Lean 4)

The later public AlphaProof Nexus Lean file supplies a proof without sorry of an existential O(1/t) constant under explicit monotonicity, Lipschitz, differentiability and saddle-point hypotheses. Its C includes slack +100, so it certifies the asymptotic rate, not the paper's displayed exact constant. The paper's earlier link points to an older Ryu-paper PR and is not itself the evidence used here. No local Lean rebuild was performed.

Formal checking

Under stated monotone Lipschitz saddle-point assumptions and the agent's schedule, there exists C>0 with squared last-iterate gradient norm at most C/T for every T>=1; Proof term last_iterate_convergence in APNOutputs/AICollaborator/Optimization/LastIterateConvergence.lean, with no sorry in that file

Checker
Lean 4 kernel, reported by the Google DeepMind AlphaProof Nexus authors
Scope
Under stated monotone Lipschitz saddle-point assumptions and the agent's schedule, there exists C>0 with squared last-iterate gradient norm at most C/T for every T>=1
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

Surina and coauthors' natural-language proof explains bounded iterates, the recurrence for consecutive differences and the final residual bound.

Correction and publication history