Quantum automated theorem proving

TL;DR

The paper addresses the scalability bottleneck of automated theorem proving by proposing Quantum Automated Theorem Proving (QATP), which integrates quantum subroutines into traditional logical and algebraic proof systems. It develops quantum-resolution methods for propositional and first-order logic, achieving a quadratic reduction in query complexity, and extends Wu’s algebraic method for geometric theorem proving into the quantum domain using circuit-based polynomial pseudo-division and Kravchuk-based interpolation. The work provides both state-based and circuit-based formulations, analyzes complexities (including PIT on quantum computers), and demonstrates a concrete end-to-end geometry proof framework for IMO-style problems. This quantum-symbolic approach promises scalable, verifiable reasoning on quantum hardware and establishes a bridge between quantum computation and symbolic AI with potential impact on formal verification and mathematical reasoning.

Abstract

Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast array of applications and the quest for enhanced theorem-proving capabilities remains a prominent pursuit in artificial intelligence. Here, we propose a generic framework for quantum automated theorem proving, where the intrinsic quantum superposition and entanglement features would lead to potential advantages. In particular, we introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks. We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic with quadratically reduced query complexity. In addition, we propose the quantum algebraic proving method for geometric theorems, extending Wu's algebraic approach beyond the classical setting. Through concrete examples, including geometry problems from the International Mathematical Olympiad, we demonstrate how a quantum computer may prove geometric theorems with quadratic better query complexity. Our results establish a primary approach towards building quantum automatic theorem provers, which would be crucial for practical applications of both near-term and future quantum technologies.

Figures (10)

• Figure 1: An illustration of quantum automated theorem proving. a, The badminton-basketball reasoning task expressed in natural language. The initial knowledge base in this case consists of ten sentences and the target is to infer whether Bob likes both badminton and basketball or not (see Supplementary Information Section II.B for details). b, The IMO 2008 Geometry Problem 1 diagram and statements. c, Left panel: first-order logic representation of the knowledge base for the badminton-basketball reasoning task; Right panel: algebraic expressions of the knowledge base for the IMO 2008 Geometry Problem 1. By using different encoding strategies, these knowledge bases expressed in formal languages are mapped into either quantum states or quantum circuits, depending on the specific task. d, Reasoning on a quantum computer.
• Figure 2: Quantum resolution for propositional logic.a, Schematic overview of the quantum resolution procedure. For a given reasoning task, the knowledge base is expressed in propositional logic as a single sentence in conjunctive normal form, which is a conjunction of $M$ clauses. The quantum resolution process consists of four main steps. First, an appropriate encoding unitary $U_{\text{KB}}$ is constructed to load the classical knowledge base into quantum memory. Applying $U_{\text{KB}}$ to the initial state $|\mathbf{0}\rangle = |0 \cdots 0\rangle$ prepares a many-body quantum state $|\Psi\rangle_{\text{KB}}$ that encodes the entire knowledge base. Second, we apply the quantum resolution unitary $U_\text{R}$ to calculate the resolution results for every propositional variable, and a verification circuit to identify valid resolvents with exactly one resolved variable (see Supplementary Information Section II.A), yielding the state $|\Psi\rangle_\text{R}$. This state is a uniform superposition of $M^2$ components—$s$ of which correspond to valid clauses (state $\left| 1 \right\rangle$ on the last qubit) and the remaining $M^2 - s$ to invalid ones (state $\left| 0 \right\rangle$ on the last qubit). Each clause after resolution is denoted as $L_j$ ($j = 1, \ldots, M^2$). Third, amplitude amplification increases the probability of observing valid components from $s/M^2$ to $\Omega(1)$. Finally, measuring the post-amplification state $|\Psi\rangle_\text{A}$ in the computational basis yields the $s$ valid clauses. If an empty clause is obtained, the reasoning process terminates and the target conclusion is derived. Otherwise, the newly generated clauses are added to the knowledge base, and the procedure is repeated until either an empty clause arises (the theorem is proved) or no new clause can be obtained (the theorem cannot be inferred). b, Quantum circuit implementing the encoding unitary $U_{\text{KB}}$. This circuit consists of $M$ controlled subcircuits. Each subcircuit maps the state from $\left| \bf{0} \right\rangle$ on $N$ ququarts (bottom wire) to the state representing the $m$-th clause, conditioned on the state $\left| m \right\rangle$ on the $k=\log _2 M$ index qubits (top wire). c, Circuit representation of the quantum resolution unitary $U_\text{R}$. This circuit resolves two variables $c_1$ and $c_2$ and outputs the resolution result $\mathcal{R}({c_1}, {c_2})$ on the third ququart. d, Quantum circuit for amplitude amplification. Here, $H$ denotes the Hadamard gate, and $X$ and $Z$ represent the Pauli-$X$ and Pauli-$Z$ operators, respectively. The key idea is to entangle states corresponding to valid (invalid) clauses with state $\left| 1 \right\rangle$ ($\left| 0 \right\rangle$) of the last qubit, and to amplify the amplitude of valid clauses. After $O(M/\sqrt{s})$ iterations, the probability of obtaining valid clauses is increased from $s/M^2$ to $\Omega (1)$.
• Figure 3: The quantum pseudo-division algorithm. We consider a general scenario of dividing a polynomial $\text{S}$ by another polynomial $\text{T}$ with respect to the variable $y$. a, A sketch of ${U_{\text{S},y}}$, which represents the coefficients of $y$ with varying degrees. The qubits that encode the variables $\bf{x}$ are omitted, and the state $\left| {\sum\limits_{\bf{i}}^{\bf{I}} {\text{s}({\bf{i}},d)\prod\limits_k^\text{K} {x_k^{{i_k}}} } } \right\rangle$ is abbreviated as $\left| {\text{s}({\bf{i}},d)} \right\rangle$. b, A sketch of ${U_{\text{R},y}}$ that represents the remainder polynomial for $\text{S}$ divided by $\text{T}$. Here, for simplicity, we write $\left| {\text{r}({\bf{i}},{\bf{j}},d)} \right\rangle$ as the abbreviation of $\left| {\sum\limits_{{\bf{i}}, \bf{j}}^{\bf{I}, \bf{J}} {\text{r}({\bf{i}},{\bf{j}},d)\prod\limits_k^\text{K} {x_k^{{i_k} + {j_k}}} } } \right\rangle$. The number of qubits represented by $\left| \bf{0} \right\rangle$ in the red box is generally greater than the input state $\left| \bf{0} \right\rangle$ for ${U_{\text{R},y}}$ or ${U_{\text{T},y}}$, because these qubits for ${U_{\text{R},y}}$ represent the product of the polynomials for the coefficients of $\text{S}$ and $\text{T}$. The resulting polynomials usually have a higher degree. c, Basic arithmetic circuits used in the construction of ${U_{\text{R},y}}$. The circuits $U_{+}$, $U_{-}$, and $U_{\times}$ are designed to implement addition, subtraction, and multiplication of the input states, respectively. d, The quantum circuit for ${U_{\text{R},y}}$ that represents the remainder polynomial. The states in the red boxes are the input states and those in the green boxes are the output states of ${U_{\text{R},y}}$. The key output $\left| {{\rm{r}}({\bf{i}},{\bf{j}},d)} \right\rangle = \left| {{\rm{s}}({\bf{i}},d){\rm{t}}({\bf{j}},{{\rm{D}}_{\rm{t}}}) - {\rm{t}}({\bf{j}},d + {{\rm{D}}_{\rm{t}}} - {{\rm{D}}_{\rm{s}}}){\rm{s}}({\bf{i}},{{\rm{D}}_{\rm{s}}})} \right\rangle$ is obtained after the portion of the circuit preceding the blue dashed line is executed. The remaining qubits in the purple boxes serve as auxiliary qubits that can be prepared to the desired states (purple boxes) with one layer of single-qubit gates. These auxiliary qubits are reset after the state $\left| {\text{r}({\bf{i}},{\bf{j}},d)} \right\rangle$ is produced.
• Figure 4: An illustration of QATP for an IMO geometry problem.a, The IMO 2008 Geometry Problem 1 in natural language. b, Coordinate assignment and hypothesis algebraic equations for this geometry problem. Without loss of generality, we assign the coordinates of the first point A as (0, 0), and those of the second point B as (0, $x_4$). This choice corresponds to setting $x_1 = x_2 = x_3 = 0$. For simplicity, here we only explicitly show a small portion of the hypothesis algebraic equations. c, The triangular form of the hypothesis equations and one of the conclusion equation $g_1$. d, Successive pseudo-division of the conclusion by the triangulated hypotheses. The variable with the largest subscript in the conclusion is $x_{22}$, which is removed in the first pseudo-division using $h_{16}$. The last pseudo-remainder $R_6$ is zero, proving the validity of the conclusion $g_1$. The number of monomials in the pseudo-remainders determines the computational time and space required for a given proof, potentially being very large for certain cases Wu1978DecisionChou198809introduction. For this particular problem, the largest number is 16172. e, A sketch of the quantum circuit for pseudo-division of the conclusion polynomial $g_1$ by $h_{16}$. This circuit involves two copies of the circuit representing $g_1$ and two copies of the circuit representing $h_{16}$, together with an arithmetic circuit required to perform pseudo-division. f, Quantum gates used in representing polynomials with quantum circuits. g, The quantum circuit for representing $h_{16}$ with seven qubits. This circuit calculates the coefficients of $h_{16}$ in variable $x_{22}$. We first perform quantum Fourier transform on the output qubits, and then use controlled phase gates to add phases determined by the value of the input variables and the degree of the variable being eliminated. The last step is to revert the phase of the quantum state back to the binary representation on the qubits. We use the circuit for $h_{16}$ on seven qubits in this figure as a simple demonstration. The complete circuits of $h_{16}$ employed in the first step of quantum pseudo-division in fact requires more qubits to represent $x_4$, $x_{20}$, the exponent of $x_{22}$, and the output. It involves 28 qubits and has a depth of 89, which is too complicated for clear visualization.
• Figure S1: Quantum circuit implementing the resolution operation for a single propositional variable.