发表机构
Zhejiang University; Tsinghua University; Hefei National Laboratory; Shanghai Qi Zhi Institute（浙江大学; 清华大学; 合肥国家实验室; 上海期智研究院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究在超导量子处理器上实验实现了自动几何定理证明，开发了基于量子伪除法和全角方法的两个框架，成功证明正方形对角线垂直及一道1978年IMO几何题，展示了量子增强符号智能的可行性。
AI 中文摘要
自动定理证明旨在利用计算系统证明或证伪数学和逻辑命题[1, 2]。它支撑着广泛的应用，提升定理证明能力仍是人工智能的核心目标[3]。尽管近期神经符号系统取得了显著进展[4-7]，其运行最终受限于经典计算架构。相比之下，量子计算[8]能够实现超越经典极限的信息编码和相干并行[9-14]，为加速结构化符号演绎[15]提供了可能。在此，我们报告了在完全可编程的超导量子处理器上实现自动几何定理证明的实验成果。我们开发了两个互补的量子证明框架。第一个框架利用量子伪除法实现吴氏代数消元法，将多元多项式表示为叠加态，从而实现量子代数定理证明。第二个框架通过混合量子策略引导架构，将全角方法实现为反向符号推理，展示了通往量子符号证明搜索的一般路径。作为示例，我们在超导量子处理器上证明了两条定理：正方形对角线垂直性以及一道1978年国际数学奥林匹克几何问题。我们的结果在实验层面确立了自动逻辑推理作为近期量子处理器的可行任务，并为量子增强的符号智能提供了具体路径。
英文摘要
Automated theorem proving seeks to use computational systems to prove or disprove mathematical and logical statements [1, 2]. It underpins a wide range of applications, and enhancing theorem-proving capabilities remains a central objective in artificial intelligence [3]. Although recent neuro-symbolic systems have achieved remarkable progress [4-7], their operation is ultimately constrained by classical computational architectures. Quantum computing [8], by contrast, enables information encoding and coherent parallelism beyond classical limits [9-14], raising the possibility of accelerating structured symbolic deduction [15]. Here we report the experimental realization of automated geometry theorem proving on a fully programmable superconducting quantum processor. We develop two complementary quantum proving frameworks. The first implements Wu's algebraic elimination method using quantum pseudo-division, with multivariate polynomials represented in superposition states, enabling quantum algebraic theorem proving. The second implements the full-angle method as backward symbolic reasoning through a hybrid quantum strategy-guided architecture, demonstrating a general route toward quantum symbolic proof search. As illustrative examples, we prove two theorems on a superconducting quantum processor: the perpendicularity of the diagonals of a square and a 1978 International Mathematical Olympiad geometry problem. Our results establish, at the experimental level, automated logical reasoning as a viable task for near-term quantum processors and provide a concrete pathway toward quantum-enhanced symbolic intelligence.
