arXiv Artificial Intelligence· Sergey Shirobokov, Ben Jaderberg, Katerina Hristova, George Tsoukalas, Johannes Bausch, Eric Wieser, Francisco J. H. Heras, Nicholas C. Rubin, Guang Hao Low, S\'ebastien Racani\`ere, Nenad Toma\v{s}ev, Lei M. Zhang, James Watson, Tanuj Khattar, Aws Albarghouthi, Stavan Jain, Harun Khan, Leopoldo Sarra, Andrew W. Senior, Michael Broughton, Hussain Masoom, Sergio Boixo, Ryan Babbush, Swarat Chaudhuri, Pushmeet Kohli·· 13 小时前AI 评分58
AI 智能体在 Lean 中自动发现并形式化验证量子程序
Discovering formally verified quantum programs with AI
AI 导读
研究团队在 Lean 定理证明器中构建量子程序库，让大语言模型智能体按形式化问题规格合成新程序并验证其正确性与代价。智能体团队通过 wiki 共享结果、在组织的会议中讨论想法，在并行搜索上取得最高 1.4x、量子算术 290x 的提升，聚变、光化学和药物代谢相关模拟分别提升 11x、8x 和 2.5x。作者称在数学证明的严格性下结合人与 AI，可设计出当今经典与量子计算机都无法测试的算法。
推荐理由模型分析
量子算法难以在经典计算机上完整验证，该工作用 Lean 形式化规格让 LLM 智能体合成并证明程序正确性与代价，给出可比较的加速基线。
来源：arXiv Artificial Intelligence · arxiv.org