Quantum automated theorem proving

TL;DR

This paper introduces a quantum framework for automated theorem proving, leveraging quantum superposition and entanglement to improve reasoning efficiency and extend capabilities to geometric theorems, with promising results demonstrated on Olympiad geometry problems.

Contribution

It presents a novel quantum-based framework for automated theorem proving, including quantum representations, reasoning algorithms, and applications to geometric theorems with improved query complexity.

Findings

Quantum resolution reduces query complexity quadratically.

Quantum algebraic proving extends classical methods to geometry.

Demonstrated proof of geometric theorems using quantum algorithms.

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.