PaperlayerView exact revision on arXiv

Source-linked AI summary

Proving olympiad geometry theorems on a superconducting quantum processor

Ning Wang, Zheng-Zhi Sun, Zhengyi Cui, Yiren Zou, Aosai Zhang, Fanhao Shen, Jiarun Zhong, Zehang Bao, Zitian Zhu, Han Wang, Jia-Nan Yang, Jiayuan Shen, Gongyu Liu, Yanzhe Wang, Yihang Han, Yiyang He, Jiahua Huang, Sailang Zhou, Xinrong Zhang, Yaozu Wu, Zixuan Song, Jinfeng Deng, Hang Dong, Qi Ye, Weikang Li, Si Jiang, Yixuan Ma, Shuangyue Geng, Zhide Lu, Chao Song, Hekang Li, Pengfei Zhang, Qiujiang Guo, H. Wang, Dong-Ling Deng

arXiv:2609.14533v1quant-phcs.AI

TL;DR

Geometry theorem proving requires precise formal representations and rigorous deduction, while remaining a challenging setting for automated theorem proving. This work implements algebraic and symbolic proof procedures on a superconducting quantum processor, demonstrating proofs of two geometry theorems. The experiments are limited in problem size and symbolic relations, and proof states are measured and re-prepared between reasoning rounds.

  • Problem

    Geometry theorem proving requires precise representations and rigorous chains of deduction, making it an intuitive yet demanding setting for automated theorem proving.

    Source: p. 1

  • Method

    The paper implements Wu’s algebraic method through quantum pseudo-division and a hybrid quantum strategy-guided architecture for full-angle symbolic proof search.

    Source: pp. 1–2

  • Results

    The processor demonstrated an algebraic proof of square-diagonal perpendicularity and a symbolic proof of a 1978 IMO geometry problem.

    Source: pp. 4, 6

  • Takeaways & Limitations

    The experiments provide a first experimental step toward quantum automated theorem proving and quantum symbolic intelligence.

    Source: p. 6

    The experiments cover limited-size polynomial instances and restricted symbolic relations, with proof states measured and re-prepared between reasoning rounds.

    Source: p. 6

Abstract

from arXiv · show

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.

1. QUANTUM ALGEBRAIC THEOREM PROVING

Quantum automated theorem proving encodes hypotheses and proof operations for quantum processing, then checks whether each derivation establishes the target. The reasoning method and termination rule determine how the process proceeds and ends.

1. QUANTUM ALGEBRAIC THEOREM PROVING

  • The QATP workflow formalizes a natural-language problem, encodes its knowledge base for quantum reasoning, then classically updates and re-encodes intermediate results.The chosen proof strategy and termination rule determine when iteration yields a proof; computation may also refute the target, stop for lack of progress, or reach a resource limit.Source: §1 · pp. 11–12, Figure S2 · p. 12
  • Wu’s method iteratively reduces a conclusion polynomial, and a vanishing final pseudo-remainder establishes the conclusion under relevant non-degeneracy conditions.Classical reconstruction and re-encoding connect successive reductions in the described implementation.Source: §1 · p. 12
  • Quantum polynomial identity testing and valid-resolvent identification are search-based validation tasks for which Grover-type algorithms can reduce query complexity quadratically.This comparison applies to search subroutines, not overall theorem-proving cost; broader speedup claims are constrained by no-go results and complexity-theoretic assumptions.Source: §1 · p. 12
  • Small geometric examples suit NISQ devices because their statements are visualizable and coordinate representations directly formalize them.The section reviews Wu’s method before presenting the square example and its quantum implementation.Source: §1 · p. 12

A. Classical Wu’s method

Wu’s method translates geometric relations into polynomial equations and uses ordered pseudo-division to determine whether a conclusion follows from the hypotheses. A zero final pseudo-remainder certifies the conclusion, subject to non-degeneracy conditions.

A. Classical Wu’s method

  • Wu’s method translates geometric relations into multivariate polynomial equations and tests whether the conclusion polynomial follows from the hypothesis constraints.The method is deterministic and applies to generic geometric configurations.Source: A. Classical Wu’s method · p. 12
  • A fixed variable ordering guides successive pseudo-divisions, reducing the polynomial system to a triangular set with strictly increasing leading variables.The ordering reflects the construction’s point-introduction order and determines each polynomial’s leading variable and coefficient.Source: A. Classical Wu’s method · p. 12
  • Each pseudo-division step cancels the current highest-degree term without dividing by the divisor’s leading coefficient, keeping intermediate polynomials in the original coefficient ring.The resulting pseudo-remainder is zero or has lower degree than the divisor in the elimination variable.Source: A. Classical Wu’s method · p. 13
  • A vanishing final pseudo-remainder establishes the conclusion through the triangular set, up to factors arising from leading coefficients.Those factors impose non-degeneracy conditions; this work assumes them implicitly rather than treating them further.Source: A. Classical Wu’s method · p. 13

B. The square example

The square’s geometric constraints are translated into polynomials and eliminated in sequence using Wu’s method. The final zero pseudo-remainder certifies that the diagonals are perpendicular.

B. The square example

  • The example places A at the origin and AB along the x-axis, then parameterizes the remaining vertices with x1 through x5.This coordinate choice is made without loss of generality.Source: Figure S3 · p. 14, B. The square example · p. 14
  • The square’s constraints and target are encoded as polynomials, then the conclusion is reduced in the variable order x5, x4, x3, x2.Four successive pseudo-remainders implement the elimination sequence.Source: B. The square example · p. 14
  • Successive reductions remove x5, x4, and x3 before the final reduction yields zero.The first step subtracts x3H1 from the target polynomial to eliminate x5.Source: B. The square example · p. 14
  • The final pseudo-remainder is identically zero, certifying that the square’s diagonals are perpendicular under the non-degeneracy assumptions used to obtain the hypotheses.The conclusion polynomial follows from the four hypothesis polynomials.Source: B. The square example · p. 14

C. Quantum implementation of Wu’s method

The quantum implementation represents polynomials through evaluated point-value pairs and performs pseudo-division using pointwise arithmetic. Classical steps prepare coefficients and connect successive reductions.

C. Quantum implementation of Wu’s method

  • A sufficient evaluation set uniquely determines a polynomial, allowing quantum operations on encoded point-value pairs instead of monomial coefficients.Pointwise reversible arithmetic avoids term collection and coefficient comparison, and circuits on a shared evaluation set can be composed for iterative pseudo-division.Source: C. Quantum implementation of Wu’s method · p. 15
  • For pseudo-division, coefficient polynomials are obtained classically, encoded in a circuit controlled by the eliminated variable’s exponent, and combined with arithmetic circuits.The implementation uses classical polynomial-value computation, interpolation, and coefficient reconstruction around the quantum operations.Source: C. Quantum implementation of Wu’s method · p. 15
  • In the square example, each variable elimination requires one pseudo-division step, and the final step yields the zero polynomial.Table S1 lists the remaining variables, elimination variable, dividend, and divisor for each step.Source: C. Quantum implementation of Wu’s method · p. 15, Table S1 · p. 15
  • Evaluation sets are chosen according to maximal degree; steps 2–4 use 0, 1, and −1 when three evaluation values are required.These sets determine the point-value encoding while limiting its overhead; Table S2 lists variable values by reasoning step.Source: C. Quantum implementation of Wu’s method · p. 15, Table S2 · p. 16

2. QUANTUM PROOF SEARCH

Quantum proof search makes inference selection part of the reasoning task: a strategy chooses actions, while formal circuits apply and evaluate them. The framework separates action choice from proof validity, though the experiment measures between reasoning rounds.

2. QUANTUM PROOF SEARCH

  • Proof search addresses the need to explore many possible intermediate statements and reasoning paths even when individual reasoning operations are efficient.Long sequences of low-level symbolic operations may also be difficult to interpret directly.Source: §2 · p. 16
  • At each backward-chaining step, the prover selects an inference and any supporting knowledge-base relations, then uses the resulting state in later rounds.The process starts from the target and reduces the proof state toward the hypotheses.Source: §2 · p. 16
  • The architecture separates strategy-selected inference actions from formally specified transformations, so proofs can be checked independently of how actions were chosen.An evaluation circuit provides information for improving action selection.Source: §2 · p. 16
  • A fully coherent implementation could retain actions, supporting relations, and intermediate formulas in superposition, but this experiment measures each round’s output before preparing the next input.Full-angle reasoning is used as the concrete proof-search realization.Source: §2 · pp. 16–17

A. Preliminaries for the full-angle method

The full-angle method represents geometric relations as algebraic objects and combines a forward-built geometry information base with backward proof reduction. Canonical ranking and control rules constrain transformations toward simpler expressions.

A. Preliminaries for the full-angle method

  • The full-angle method represents geometric relations with full-angles, algebraic objects supporting equality, addition, and sign operations, and constructs proofs using finite inference rules.The method combines forward construction of the geometry information base with backward chaining from the target.Source: A. Preliminaries for the full-angle… · p. 17
  • Full-angle equality, addition, and core rules encode parallelism and perpendicularity as constants, while other rules express line, cyclicity, and angle relations.The stated rules include line membership and parallel substitution, angle splitting, and several geometric inference patterns.Source: A. Preliminaries for the full-angle… · pp. 17–18
  • A total order puts full-angles in canonical form and ranks them lexicographically by their point labels.The ranking provides the basis for controlling rule applications.Source: A. Preliminaries for the full-angle… · p. 18
  • The control strategies allow a transformation only when it lowers rank, and allow line splitting only when both resulting full-angles can be reduced further.Together, these restrictions suppress unproductive transformations and unnecessary proof-search growth.Source: A. Preliminaries for the full-angle… · p. 18
  • The geometry information base stores elementary geometric facts derived from hypotheses for later use in simplifying full-angle inference rules.It is built before the goal-directed proof begins.Source: A. Preliminaries for the full-angle… · pp. 17–19
  • To build the GIB, the prover adds hypotheses, repeatedly applies forward-chaining rules until no new facts arise, and may use auxiliary rules when more geometric information is needed.The stored facts then support backward chaining.Source: A. Preliminaries for the full-angle… · pp. 18–19

B. IMO example

The IMO example tests backward full-angle proof search on a geometry problem, with a classically built geometry information base supplying derived relations. The quantum representation encodes formulas and proof states, while coherent knowledge-base growth remains a representation rather than an explicit classical-output advantage.

B. IMO example

  • The IMO problem asks to prove that the midpoint of FG is the incenter of isosceles triangle ABC, given a circle tangent to its circumcircle and to AB and AC at F and G.The configuration is identified as the 1978 International Mathematical Olympiad geometry problem.Source: B. IMO example · p. 19, Figure S6 · p. 19
  • Before backward proof search, the GIB is built from the hypotheses and derived relations, including cyclicity of A, E, F, G and equality AF = AG.The example also derives relations such as FG ∥ BC and EF ∥ BD, then simplifies equivalent lines to lower-ranked forms.Source: B. IMO example · p. 20

C. State representation of formulas

  • With coherent knowledge-base growth, pairwise reasoning can represent up to M^(2t) formulas after t rounds, or M^t when each step combines the initial base with the current one.In both constructions, composed reasoning-circuit depth grows linearly with t; the latter uses t log2 M index qubits rather than 2t log2 M.Source: C. State representation of formulas · p. 21
  • These counts describe formulas retained in quantum states, not formulas extracted as classical outputs, so they do not establish an exponential quantum advantage for producing the same formulas explicitly.The full-angle experiment constructs its GIB classically before encoding it for quantum reasoning.Source: C. State representation of formulas · p. 21
  • Formula indices use a separate register whose qubit count grows logarithmically with the number of formulas; formula data instead scales with the formula’s variables and value set.For N variables and local value-set cardinality |V|, the stated qubit data-register requirement is N log2 |V|.Source: C. State representation of formulas · pp. 21–22
  • Full-angle formulas are encoded using a sign register and registers for point indices, while the proof state holds the formula or superposition of formulas being processed.A classically specified target can be prepared as a computational-basis product state, and each reasoning operation produces the next proof state.Source: C. State representation of formulas · pp. 21–22

D. Reasoning engine

The reasoning engine applies formal inference rules to transform formulas, using inputs from the current proof state, a selected action, and the quantum knowledge base. It can operate coherently on superposed formulas, with circuit depth governed by the rule set and local value set.

D. Reasoning engine

  • The reasoning circuit takes the current formulas, an action specifying the rule and hypotheses, and the quantum-encoded knowledge base as inputs.Its structure reflects the logic system's inference rules, while its implementation depends on the symbolic-formula encoding.Source: D. Reasoning engine · p. 22
  • The reasoning engine acts coherently on formulas in superposition, so inference need not process them one by one.For the examples considered, the corresponding circuits have constant depth or depth that grows mildly with the local value set.Source: D. Reasoning engine · p. 22
  • For rule R9, the circuit writes the conclusion when the input matches the rule premise and otherwise preserves the original input.The circuit compares the input angle with the premise and resets its auxiliary qubits after the operation.Source: D. Reasoning engine · p. 22, Figure S7 · p. 23
  • Reasoning-engine depth scales as O(|R| log |V|); for the full-angle example, |R| = 21 and |V| = 8.Rules are applied sequentially, while the logarithmic dependence on the value set follows from decomposing multi-qubit controlled operations.Source: D. Reasoning engine · p. 23
  • The rule-matching circuit pattern is presented as applicable beyond resolution and the full-angle method to a broad class of rule-based reasoning systems.An inference step checks whether its input matches a rule's applicability pattern before applying the prescribed transformation.Source: D. Reasoning engine · p. 23
  • Validity checks such as whether exactly one variable is resolved are delegated to the strategy engine and value-function evaluation, not the reasoning engine.Those components guide rule and hypothesis selection and enforce the reasoning process's validity.Source: D. Reasoning engine · p. 23

E. Strategy engine and value function

The strategy engine proposes inference actions, while an evaluation circuit assesses resulting proof states and supplies signals for parameter optimization. Two illustrative scenarios show how superposition and interference can shape action selection and evaluation, but the authors do not claim a rigorously established exponential advantage.

E. Strategy engine and value function

  • The variational strategy circuit distributes probability over candidate actions, and evaluation signals are used to optimize its parameters.The authors present heuristic scenarios rather than a comprehensive analysis of expressive power, optimization landscape, or compilation complexity.Source: E. Strategy engine and value function · p. 23
  • More general training schemes, including reinforcement-learning optimization over multi-step proof trajectories, are left for future work.The scenarios are presented as illustrative constructions.Source: E. Strategy engine and value function · pp. 23–24
  • A Hadamard-based strategy suppresses an unproductive action by destructive interference for a superposed input, leaving the action that generates a new formula.For the example, action 1 exchanges F1 and F2, while action 0 generates F3; the same Hadamard gate gives equal action weights for F1 and F2 individually.Source: E. Strategy engine and value function · p. 24
  • A comparison circuit can distinguish a strategy that never changes its inputs from one that produces new outcomes for half of the possible inputs.The authors frame this evaluation as analogous to the Deutsch-Jozsa algorithm.Source: E. Strategy engine and value function · p. 24
  • The scenarios are deliberately constructed and may not reflect typical proof-search learning; they do not establish exponential advantage in a standard classical input-output setting.The authors note that a classical algorithm could solve the tasks efficiently if given direct access to the relevant oracle information.Source: E. Strategy engine and value function · p. 24

1. Circuit of reasoning engine

The reasoning circuit applies action-controlled full-angle updates to proof states, while a value function favors actions that change the state. The compiled implementation retains coherent symbolic reasoning within each round, but measures between rounds.

1. Circuit of reasoning engine

  • The compilation treats each explicit equality between full-angles and a GIB relation as an action, simplifying implementation while increasing action count and circuit depth.The overhead remains acceptable when both the GIB and inference-rule set are small.Source: §1 · pp. 24–25
  • The proof sequence derives ∠[HB, CB] = ∠0 by chaining the listed full-angle relations.The sequence proceeds through ∠[HD, FD], ∠[FD, DB], and −∠[HB, CB].Source: §1 · p. 25
  • The compiled circuit applies action-controlled updates to a copied proof state when the selected action's required input relation matches the current state.The experiment measures the output after each round and uses it to prepare the next round, rather than coherently composing multiple rounds.Source: §1 · pp. 25–26

2. Circuit for the value function

  • The evaluation circuit compares proof states at consecutive rounds, favoring actions that make a nontrivial update and suppressing the unused action state.The stated criterion does not evaluate longer reasoning trajectories.Source: §2 · p. 26

3. Circuit of strategy engine

A variational circuit selects each reasoning action from the current proof state, and the experimental processor executes the strategy and reasoning circuits using superconducting-qubit gates and readout.

3. Circuit of strategy engine

  • The action-selection circuit determines each action from the proof state, coupling action-register qubits to the state qubits encoding relevant geometric content.Single-qubit rotations accompany entangling gates to increase the ansatz's expressive power.Source: §3 · pp. 26–27, Figure S10 · p. 27
  • The processor uses an 11×11 array of frequency-tunable transmon qubits, 220 nearest-neighbor couplers, and 121 readout resonators.The circuits use single-qubit, two-qubit, and measurement gates.Source: §3 · p. 27
  • The experiments use controlled-phase (CP) gates as their two-qubit gate; the CP process completes in 44 ns, and measurement gates use custom-envelope microwave pulses with optimized power, length, and qubit frequency.To enhance readout fidelity, an additional microwave pulse drives the |1⟩↔|2⟩ transition before the readout pulse.Source: §3 · p. 27

B. Circuit and layout

  • Executing theoretical circuits on the processor involves multi-qubit gate optimization and quantum circuit compilation.The section identifies these as two preprocessing procedures.Source: B. Circuit and layout · p. 29

1. Multi-qubit gate optimization

The paper reduces the overhead of multi-qubit gates and compiles theoretical circuits for the processor's nearest-neighbor connectivity and native gates.

2. Quantum circuit compilation

  • SABRE maps logical qubits to physical qubits and inserts SWAP gates when nearest-neighbor connectivity prevents a required two-qubit interaction.In the illustrated example, a SWAP repositions Q2 and Q3 for the third CP gate.Source: §2 · p. 30, Figure S15 · p. 31
  • After mapping and routing, circuits are transpiled to the native {U, CP} gate set, with gate fusion and scheduling used to shorten depth and limit crosstalk and idle time.Fusion merges consecutive single-qubit gates on the same qubit.Source: §2 · p. 30

1. Multi-qubit gate optimization

  • Approximately 50% reduction in both quantum gate count and circuit depth is achieved with optimized CCX and CCCX implementations relative to the original implementations.The optimized decompositions preserve circuit validity up to a relative phase.Source: §1 · p. 29, Figure S14 · p. 31

3. Experimental circuits

For algebraic theorem proving, the experimental circuits use Pauli twirling and are compiled into a physical circuit with a specified qubit and gate count.

3. Experimental circuits

  • Pauli twirling is applied to four algebraic theorem-proving circuits to suppress gate-dependent errors while leaving the overall function invariant.The CP(π) gates are sandwiched with random Pauli gate combinations.Source: §3 · p. 31, Figure S16 · p. 31
  • The experimental circuit corresponding to the theoretical circuit in Fig. S13 uses 28 physical qubits.The physical qubits are identified by their coordinates in the processor layout.Source: §3 · p. 31, Figure S17 · p. 32
  • The 28-qubit experimental circuit contains 202 single-qubit gates, 116 CP gates, six Z-basis measurement gates, and has depth 80.Source: §3 · pp. 31, 33

C. Additional results

Figure S18 reports the experimental point-value correspondence for steps 2 and 3, with outcomes organized by exponent sector and encoded point-register states.

C. Additional results

  • In step 2, the point register encodes x1, x2, and x3 using 1, 2, and 1 qubits, respectively.The two-qubit value register represents coefficient values.Source: C. Additional results · p. 33
  • In step 3, the point register encodes x1 and x2 using two qubits each.The two-qubit value register represents coefficient values.Source: C. Additional results · p. 33
  • Figure S18 shows measurement outcomes for steps 2 and 3, with colors indicating probabilities across joint point-register states.The results are classified into sectors according to d.Source: Figure S18 · p. 33, C. Additional results · p. 33
Loading 2609.14533v1…