算法学家 I：大规模可证算法综合的承诺

设计既可证明且在实际中表现良好的算法仍然困难，需要数学推理与严谨实现。已有的将最坏情况理论与实证性能相结合的方法，如超最坏情况分析和数据驱动算法选择，通常假设先验分布知识或仅关注固定算法池。近期进展表明，LLM 可能开启一种全新的可能：即时可证算法综合。为此，我们构建了 Algorithmist——一个基于 GitHub Copilot 的自主研究代理，运行多智能体研究-审查循环，包括创意生成、算法与证明开发、证明导向实现以及证明、代码及其一致性审查。我们在私有数据分析和聚类等研究水平任务上评估了 Algorithmist。当被要求设计满足隐私、近似和可解释性要求的实用方法时，它产生了可证明正确且实证有效的算法，伴随研究风格的撰写和审计后的实现。它在某些情境下还发现了改进算法，解释了其他情境下的原则性障碍，并发现了先前已发表工作中的细微证明错误。更广泛地说，我们的结果表明一种新范式正在形成：LLM 系统为每个数据集和部署情境生成研究论文质量的算法制品。它们还指向一种以证明为先的代码综合范式，即在结构化自然语言证明中间表示中开发代码，并在综合过程中保持其与证明的一致性。