Jan Heemstra: Hardware accelerated intelligent theorem proving

Event Details

We present a connection-based tableaux theorem prover that performs inferences entirely on the GPU. Benchmarks on the m40 dataset show it performs worse than other provers in terms of proving power. In terms of inferences per second, however, it is on par with or even surpasses state-of-the-art provers on similarly priced and dated hardware, despite it lacking various important optimizations that are present in the other provers. On top of this prover, we designed and implemented a heuristic neural network-based system that avoids evaluations during the computation of inferences, and instead pre-computes the results of these evaluations.