Finding Simple Proofs for First-Order Optimization

Motivation

• Known: PEP framework는 first-order optimization method의 worst-case convergence rate를 SDP로 정식화하고, 그 Lagrangian dual solution을 통해 수치적 증명 certificate를 자동으로 발견할 수 있음이 알려져 있다.
• Gap: 그러나 이렇게 얻어진 dual certificate는 numerical, parameter-specific, dense하며 유일하지 않아, 어떤 inequality와 residual term이 실제로 증명을 이끄는지 파악하기 어렵고 인간이 해석·재사용·formalization하기 힘들다는 문제가 있다.
• Why: LLM 및 solver 기반 agentic workflow가 수학 연구에 활용되려면, dense한 machine-generated proof를 사람이 이해·검증·재사용 가능한 compact 구조로 자동 정제하는 절차가 필요하며, 이는 AI-assisted mathematical discovery를 더 체계적이고 검증 가능하게 만드는 핵심 단계이다.
• Approach: 이 논문은 증명 단순화를 dual certificate 위에서의 2단계 optimization 문제로 재정의하고, active hypothesis 수와 residual 구조 등 complexity 척도를 도입한 뒤, (weighted) ℓ1-heuristics와 intermediate lemma 탐색을 위한 SDP 기반 절차를 개발한다.

Achievement

Figure 2. Fitted interpolation curvatures identified from singleton candidate lemmas for the one-step gradient descent c

1. Certificate-complexity criteria 정의: 표준 interpolation 기반 PEP의 SDP 정식화를 바탕으로 active inequalities와 residual term을 이용한 증명 복잡도 척도를 제안했다.
2. Sparsification 절차 개발: 소규모 인스턴스에 대한 exhaustive search부터 대규모 문제를 위한 weighted ℓ1-type surrogate까지 exact/heuristic sparsification 기법을 개발했다.
3. Intermediate lemma 탐색: 기존 PEP formulation에 있는 부등식들로부터 새로운 valid inequality(candidate intermediate lemma)를 도출하는 SDP 탐색법을 제안했다.
4. 다양한 알고리즘에 적용: gradient descent(GD), fast-gradient methods(FGM), proximal methods에 대해 실험하여, redundant inequality 자동 제거, 3-hypothesis GD proof, compact FGM multiplier pattern, proximal point residual bound 및 accelerated proximal point saddle-gap estimate에 대한 Lyapunov function 기반 compact proof 등을 복원했다.

How

Figure 3. FGM hypothesis complexity across horizon lengths: all methods on the left, and the competitive continuous spar

• PEP를 함수 f, trajectory, performance metric Pf, initialization measure If를 이용한 infinite-dimensional worst-case maximization 문제로 정식화하고, exact finite-dimensional SDP reformulation의 Lagrangian dual certificate를 출발점으로 삼음
• 동일한 target bound를 증명하는 대안적(더 단순한) dual certificate를 찾는 2단계 search로 simplification을 정의
• Active hypothesis 개수와 residual decomposition 구조를 복잡도 지표로 사용
• (weighted) ℓ1-heuristic을 이용해 multiplier를 sparsify하고, 소규모 문제에는 exhaustive search 적용
• 기존 PEP formulation의 부등식들로부터 새로운 valid inequality를 도출하는 SDP 기반 candidate lemma 탐색 formulation 제안
• GD, FGM, proximal methods(및 accelerated proximal point)에 대한 구체적 사례로 검증

Originality

• PEP의 Lagrangian dual certificate를 "증명 자체"로 보고, 이를 sparse optimization/statistical learning 관점에서 후처리(post-processing)하는 새로운 문제 설정을 제시
• 증명 단순화를 별도의 2단계 optimization 문제로 정식화하여, active hypothesis 및 residual 구조 기반의 정량적 complexity 척도를 도입
• Weighted ℓ1-heuristics를 dual certificate sparsification에 적용하고, intermediate lemma를 자동으로 발견하는 SDP 탐색을 결합한 독창적 workflow 제안
• LLM 및 formal proof assistant(Lean 등)와 결합 가능한 pre-processing 단계로서 solver-guided proof simplification을 agentic workflow 관점에서 위치시킴

Limitation & Further Study

• 실험이 GD, FGM, proximal methods 등 비교적 단순하고 잘 알려진 알고리즘/함수 클래스에 국한되어 있어, 더 복잡한 composite/constrained 설정이나 stochastic 알고리즘으로의 일반화가 검증되지 않음
• "simplicity"의 정의가 여전히 operational하고 다소 임의적(active hypothesis 수, residual 구조 등)이어서, 다른 복잡도 척도나 사람의 직관적 단순성과의 정합성에 대한 추가 검토가 필요함
• Intermediate lemma 탐색이 미리 정해진 후보 부등식 공간 내에서 이루어지므로, 완전히 새로운 lemma나 proof pattern을 발견하는 능력에는 한계가 있을 수 있음
• 후속 연구로 실제 LLM 기반 agentic workflow와의 통합 실험, Lean 등 formal proof system으로의 자동 translation 검증이 필요함

Evaluation

총평: PEP 기반 dual certificate를 증명 단순화 관점에서 체계적으로 후처리하는 새로운 workflow를 제시하여, AI 보조 수학 연구를 더 검증 가능하고 재사용 가능하게 만드는 실질적 기여를 한다. 다만 적용 범위가 제한적이고 simplicity 척도의 일반성에 대한 추가 검증이 필요하다.