BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving

Abstract

Artificial Intelligence for Theorem Proving has given rise to a plethora of benchmarks and methodologies, particularly in Interactive Theorem Proving (ITP). Research in the area is fragmented, with a diverse set of approaches being spread across several ITP systems. This presents a significant challenge to the comparison of methods, which are often complex and difficult to replicate. Addressing this, we present BAIT, a framework for fair and streamlined comparison of learning approaches in ITP. We demonstrate BAIT's capabilities with an in-depth comparison, across several ITP benchmarks, of state-of-the-art architectures applied to the problem of formula embedding. We find that Structure Aware Transformers perform particularly well, improving on techniques associated with the original problem sets. BAIT also allows us to assess the end-to-end proving performance of systems built on interactive environments. This unified perspective reveals a novel end-to-end system that improves on prior work. We also provide a qualitative analysis, illustrating that improved performance is associated with more semantically-aware embeddings. By streamlining the implementation and comparison of Machine Learning algorithms in the ITP context, we anticipate BAIT will be a springboard for future research.

References in corpus (19)

• GamePad: A Learning Environment for Theorem Proving
• Structure-Aware Transformer for Graph Representation Learning
• TacticToe: Learning to Prove with Tactics
• Generative Language Modeling for Automated Theorem Proving
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
• HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
• Premise Selection for Theorem Proving by Deep Graph Embedding
• HyperTree Proof Search for Neural Theorem Proving
• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• Holophrasm: a neural Automated Theorem Prover for higher-order logic
• Formal Mathematics Statement Curriculum Learning
• Learning to Prove Theorems via Interacting with Proof Assistants
• Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
• MWPToolkit: An Open-Source Framework for Deep Learning-Based Math Word Problem Solvers
• Learning to Reason in Large Theories without Imitation
• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
• Proof Artifact Co-training for Theorem Proving with Language Models
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• Transformers over Directed Acyclic Graphs