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

arXiv:2403.03401v1 Announce Type: cross
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 …

abstract architectures artificial artificial intelligence arxiv benchmarking benchmarks challenge comparison cs.ai cs.lg cs.lo diverse embedding intelligence interactive research set systems theorem type