发表机构
Rice University; Johns Hopkins University; Google Inc.; Data Science and AI Institute, Johns Hopkins University（莱斯大学; 约翰斯·霍普金斯大学; 谷歌公司; 约翰斯·霍普金斯大学数据科学与人工智能研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
Peppy是一种AI辅助工作流，通过领域知识和SymPy验证，为优化算法提供严谨的紧收敛性证明，并解决开放问题。
AI 中文摘要
本文介绍了Peppy，一种AI辅助工作流，用于发现一阶优化算法的紧致解析收敛性证明。使用LLM进行数学研究的通用方法针对未指定的广泛问题，有时使用Lean 4证明助手进行形式化。另一方面，Peppy更充分地利用领域特定知识，从而能够以更结构化的方式构建证明，允许通过SymPy进行最小且可访问的验证。我们通过示例实验证明，Peppy为优化中的AI辅助定理合成提供了严谨、实用且可复现的范式。我们进一步强调了其解决一阶优化算法紧收敛性分析中几个开放问题的能力，包括Nesterov的FGM的猜想。总体而言，Peppy旨在将优化算法分析的艺术转变为科学。
英文摘要
This paper presents Peppy, an AI-assisted workflow for discovering tight, analytic convergence proofs for first-order optimization algorithms. Generic approaches to using LLMs to conduct mathematical research target an unspecified, broad spectrum of problems and sometimes use the Lean 4 proof assistant for formalization. On the other hand, Peppy leverages domain-specific knowledge more heavily and is thereby capable of constructing the proofs in a more structured manner, which allow a minimal and accessible verification through SymPy. We experimentally demonstrate through examples that Peppy provides a rigorous, practical, and reproducible paradigm for AI-assisted theorem synthesis in optimization. We further highlight its capability of closing several open problems on tight convergence analysis of first-order optimization algorithms, including conjectures for Nesterov's FGM. Overall, Peppy is designed to turn the art of optimization algorithm analysis into a science.
