Twitch: Learning Abstractions for Equational Theorem Proving

TL;DR

The tool Twitch is presented, which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks, which can produce abstractions from a partial, failed proof of a conjecture or from successful proofs of other theorems in the same domain.

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.

Figures (3)

• Figure 1: Overview of domain abstraction generation via Twitch (Algorithm \ref{['alg:get_domain_abstractions']} and its subroutine Algorithm \ref{['alg:local_abstractions']}).
• Figure 2: Cactus plots of Twee runtimes for TPTP problems. A given point in these plots corresponds to a particular problem $P$ from Table \ref{['tab:tptpv9']}. The y-value of a point indicates the time taken by Twee to find a proof of $P$ (possibly augmented with Twitch domain abstractions), and the corresponding x-value is the index of $P$ when the problems are sorted in increasing order of runtime.
• Figure 3: Cactus plots illustrating the effect of local abstractions. A given point in these plots corresponds to a particular problem $P$ from Table \ref{['tab:tptpv9']}. The y-value of a point corresponds to the time taken by Twee to find a proof of $P$ when augmented with local abstractions, i.e. abstractions derived from an existing proof of $P$ by default Twee. The x-value corresponds to the index of the problem when the problems are sorted by increasing runtime of Twee $P$ augmented with the local abstractions. In other words, the points correspond to runtimes from line \ref{['line:augmented_run']} of Algorithm \ref{['alg:local_abstractions']}.