量智信息中心_量科网

该研究报道了一个在量子优化领域悬而未决超过十年的问题的机器验证解答：Farhi、Goldstone和Gutmann（FGG）猜想，即深度为\(p\)的量子近似优化算法（QAOA）在分歧环上精确达到近似比\((2p+1)/(2p+2)\)。该团队借助大型语言模型Claude Fable 5找到了证明，并通过Lean 4证明助手端到端验证了其正确性。该工作的研究方法包括若干要素：在已有的量子信息Lean库基础上，该团队形式化了QAOA组件及问题的已知部分，并将猜想归约为一个单独的公开数学命题。随后，该模型被赋予该库及该团队的工具包，并承担起通过构建Lean证明来填补这一空缺的任务。最终形成的过程是一个循环反馈：模型进行自然语言推理，而Lean进行机械验证，两者收敛至一个机器验证的证明。人类验证仅需针对结构性框架——即形式化表述是否忠实编码了预定的论断——而证明本身由模型提供并由Lean机械认证。然而，该证明令人瞩目——模型揭示了问题中隐藏的动态对称性并加以利用，借用相邻领域的工具和机制，将一个困难的存性问题转化为显式构造。该工作为攻克量子信息科学及其他领域的公开猜想铺平了道路。