Peppy: An AI-Assisted Workflow for Tight Convergence Analysis of Optimization Algorithms

Motivation

• Known: PEP는 first-order optimization method의 tight한 수치적 수렴 bound(numerical certificate)를 찾는 데 유용한 computer-assisted proof framework로 널리 활용되어 왔으며, 이를 지원하는 여러 소프트웨어 패키지(PESTO, PEPit 등)가 존재한다.
• Gap: 그러나 PEP가 산출하는 수치적 certificate를 iteration number N에 무관한 analytic Lyapunov 증명으로 변환하는 작업은 여전히 인간 전문가의 수작업(research-level task)에 의존하며, 이를 자동화하는 체계적 도구는 부재했다.
• Why: 이 변환 과정을 자동화하면 최적화 이론 연구자들이 새로운 알고리즘의 tight한 수렴률 정리를 훨씬 빠르고 재현 가능하게 도출할 수 있어, 최적화 이론 연구의 생산성과 엄밀성을 동시에 높일 수 있다.
• Approach: PEP 관련 계산을 PEPFlow로 black-box화하여 AI coding agent가 다루기 쉽게 만들고, 5단계(구현-수치해-Lyapunov skeleton 정의-summation-free 표현 도출-analytic 정리 생성)로 구성된 구조화된 markdown 커맨드 시퀀스를 통해 AI 에이전트가 numerical certificate로부터 analytic Lyapunov 증명을 합성하도록 하는 workflow를 제안한다.

Achievement

Figure 1. A schematic description of Peppy’s 5-stage workflow.

1. 5단계 워크플로우 설계: PEP 구현, PEP 해결 및 certificate 추출, Lyapunov 함수 정의, summation-free 표현 도출, 최종 analytic 정리 및 증명 생성을 하나의 파이프라인으로 통합했다.
2. lyapunov_utils.py 컴포넌트 개발: Lyapunov 함수 Vk를 low-rank quadratic form으로 변환하는 비자명한 선형대수 기법을 PEPFlow 위에 패키지화하여, 기존에 인간 전문가만 수행 가능했던 research-level 작업을 자동화했다.
3. 재현 가능한 증명 검증 체계: Lean 스타일의 비용이 큰 formalization 없이도 PEP의 수치적 feasibility 확인과 symbolic matrix identity 검증을 통해 최종 증명을 검증 가능하게 만들었다.
4. GD 사례 시연: gradient descent에 대해 N-독립적인 f(xN)-f(x*) ≤ LR/(4N+2) 형태의 정리와 그 증명을 Peppy가 성공적으로 산출함을 보였다.

How

Figure 1. A schematic description of Peppy’s 5-stage workflow.

• 사용자가 문제 클래스(예: L-smooth convex function), 알고리즘 update rule, performance metric, initial condition을 coding agent에 입력
• /pep-implement 커맨드로 PEPFlow 코드를 작성해 PEP를 구성
• /pep-full-proof 커맨드로 고정된 N에서 PEP를 수치적으로 풀어 certificate(λ, d, s)를 추출하고 closed-form을 추정
• /lyap-define 커맨드로 partial sum 형태의 Lyapunov 함수 Vk 후보를 구성 (Yoon et al. 2026 절차 기반)
• 내부 선형대수 기법으로 Vk를 summation-free한 low-rank quadratic form으로 변환 (lyapunov_utils.py)
• Vk+1 ≤ Vk를 symbolic 계산으로 검증하고, 최종 정리 및 증명을 LaTeX로 생성

Originality

• PEP라는 도메인 특화 프레임워크를 AI 에이전트가 다룰 수 있도록 PEPFlow로 black-box화하여, 범용 LLM+정형검증 기반 AI4Math 접근과 차별화되는 최적화 이론 특화 AI 보조 워크플로우를 제시
• Lean 스타일 formalization 없이도 PEP 자체의 verification-friendly한 성질(수치적 feasibility 체크, symbolic matrix identity 검증)을 활용해 증명을 검증하는 경량 검증 체계 고안
• 기존에 수작업으로만 가능했던 Vk의 summation-free/low-rank quadratic form 변환을 자동화하는 lyapunov_utils.py 도입
• 구조화된 markdown 커맨드 시퀀스로 워크플로우를 모듈화하여 재현성과 검증 가능성을 확보

Limitation & Further Study

• 본문 발췌에는 GD라는 단일 사례 연구만 상세히 제시되어, 보다 복잡한 알고리즘(momentum, 가속 방법, 비볼록 문제 등)에 대한 일반화 가능성 및 성공률에 대한 정량적 평가가 부족함
• Vk를 summation-free form으로 변환하는 "nontrivial linear algebraic tricks"의 구체적 알고리즘과 그 실패 사례(에이전트가 실패하는 경우)에 대한 분석이 본문 발췌에서 충분히 드러나지 않음
• AI 에이전트의 개입 정도("varying degrees of human intervention")가 사례마다 다르다고 언급되나, 완전 자동화 대비 인간 개입이 필요한 비율이나 실패 시 복구 전략에 대한 상세한 논의가 필요
• 후속 연구로 더 넓은 범위의 알고리즘 클래스(확률적 방법, 분산 최적화 등)로의 확장 및 실패 케이스에 대한 체계적 벤치마크 구축이 필요해 보임

Evaluation

총평: PEP 기반 수렴 분석의 자동화라는 명확하고 실용적인 문제를 domain-specific한 AI 보조 워크플로우로 풀어낸 참신하고 실용적인 연구이나, 발췌된 내용만으로는 다양한 알고리즘에 대한 일반화 성능과 실패 사례에 대한 정량적 근거가 다소 제한적이다.