Algorithmist 的早期发现 I：大规模可证明算法合成的前景

设计兼具理论保证与实践效果的算法极具挑战。本文提出 Algorithmist，一个基于 GitHub Copilot 的自主研究代理，通过多智能体循环执行想法生成、算法与证明开发、证明引导的实现及审查。在隐私分析与聚类任务中，该系统能生成满足多重约束的可证明且有效的算法，产出类论文报告及审计代码，甚至发现已有工作中的证明漏洞。研究展示了“证明优先”的代码合成新范式，即代码与结构化自然语言证明同步开发并保持对齐。