arXiv:2603.22363cs.SEcs.AI2026-03

用大模型自动设计可证明有效的实用算法,还能发现旧论文的漏洞。

Early Discoveries of Algorithmist I: Promise of Provable Algorithm Synthesis at Scale

  • 构建多智能体系统,边写证明边生成代码,实现算法与证明同步演化。
  • 在隐私分析和聚类任务中产出既可证明又高效的新算法,部分优于已有方法。
  • 适合研究者探索新算法或验证理论正确性,推动代码生成向可验证方向演进。

设计兼具理论保证与实际性能的算法依然困难,需结合数学推理与精细实现。现有方法如超越最坏情况分析或数据驱动算法选择,通常依赖先验分布知识或固定算法池。大语言模型的进展带来新可能:即时生成可证明的算法。为此,我们构建了Algorithmist——基于GitHub Copilot的自主研究代理,采用多智能体研究-评审循环,包含创意生成、算法与证明开发、证明引导的实现以及对证明、代码及其一致性审查等阶段。我们在私有数据分析和聚类等研究级任务上评估Algorithmist。当要求设计同时满足隐私、近似性和可解释性要求的方法时,它生成了可证明有效且实证高效的算法,附带研究风格写作与审计后的实现。它还发现了某些场景下的改进算法,解释了其他场景中的根本限制,并揭露了先前已发表工作中的一处微妙证明错误。结果表明,这一范式可让大模型系统为每个数据集和部署环境生成高质量算法成果。同时提示一种‘以证明为先’的代码合成路径,即代码与结构化自然语言证明中间表示同步生成并保持一致。

原文摘要 · Abstract (English)

Designing algorithms with provable guarantees that also work well in practice remains difficult, requiring both mathematical reasoning and careful implementation. Existing approaches that bridge worst-case theory and empirical performance, such as beyond-worst-case analysis and data-driven algorithm selection, typically assume prior distributional knowledge or restrict attention to a fixed pool of algorithms. Recent progress in LLMs suggests a new possibility: provable algorithm synthesis on the fly. To study this, we built Algorithmist, an autonomous researcher agent on top of GitHub Copilot that runs a multi-agent research-and-review loop, with separate stages for idea generation, algorithm and proof development, proof-guided implementation, and review of proofs, code, and their alignment. We evaluate Algorithmist on research-level tasks in private data analysis and clustering. When asked to design practical methods that jointly satisfy privacy, approximation, and interpretability requirements, it produced provably sound and empirically effective algorithms, together with research-style writeups and audited implementations. It also found improved algorithms in some settings, explained principled barriers in others, and uncovered a subtle proof bug in prior published work. More broadly, our results suggest a new paradigm in which LLM systems generate research-paper-quality algorithmic artifacts tailored to each dataset and deployment setting. They also point to a proof-first code-synthesis paradigm, in which code is developed alongside a structured natural-language proof intermediate representation and kept aligned with it throughout synthesis.

算法合成大模型科研可证明性代码生成

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。