Content area
Abstract
Theory exploration is an approach to automating the discovery of interesting and useful properties about computer programs and mathematical structures. Such properties can be used to guide automated and interactive reasoning. Coming up with new lemmas is often crucial in proof automation, and can provide vital assistance to a user of an interactive proof system. Generating properties that specify the behavior of a program is beneficial for software verification, testing, and debugging. Automated conjecturing is a challenging endeavor due to the vast search space and the difficulty in identifying the most interesting and useful properties. Developing effective conjecturing techniques is therefore critical for advancing both automated and interactive formal reasoning about programs and proofs.
In this thesis, we present novel symbolic and neuro-symbolic methods for theory exploration, along with the design, development, and evaluation of associated tools. First, we present a coinductive lemma discovery tool, the first system designed to automatically discover and prove lemmas about potentially infinite structures. Then, we integrate theory exploration and automated theorem proving in a state-of-the-art inductive proof system. Next, we introduce template-based theory exploration, which narrows the conjecturing search space and makes theory exploration faster and more targeted. In addition, we provide empirical evidence for the effectiveness of template-based theory exploration in finding interesting and useful lemmas for mathematical formalizations. Finally, we use Large Language Models (LLMs) for lemma conjecturing, both directly and as part of a neuro-symbolic template-based tool. We present the first neuro-symbolic lemma conjecturing tool that can automatically conjecture lemmas across all formalization domains.
