Twitch: Learning Abstractions for Equational Theorem Proving

TL;DR

This paper introduces Twitch, a tool that automatically discovers recurring term patterns called abstractions to improve equational theorem proving, demonstrating significant speed-ups and success on benchmark problems.

Contribution

Twitch is a novel tool that automatically finds useful abstractions from proofs to enhance theorem proving efficiency.

Findings

Proved 12 rating-1 problems using abstractions.

Achieved significant speed-ups on multiple problems.

Extended Twee prover to incorporate discovered abstractions.

Abstract

Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems.