BAIT：交互式定理证明（嵌入）架构基准测试
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
AI总结：
针对交互式定理证明（ITP）研究分散、方法难比较的问题，提出BAIT框架，通过比较公式嵌入的先进架构、评估端到端证明性能，为ITP学习方法提供公平简化的比较基准，助力未来研究。
摘要：
定理证明人工智能已催生大量基准和方法，尤其在交互式定理证明（ITP）领域。该领域研究较为分散，多种方法分布在多个ITP系统中，这给方法比较带来重大挑战——这些方法通常复杂且难以复现。为解决此问题，我们提出BAIT框架，用于ITP中学习方法的公平且简化的比较。我们通过在多个ITP基准上深入比较应用于公式嵌入问题的最先进架构，展示了BAIT的能力。我们发现结构感知Transformer表现尤为出色，优于原始问题集相关技术。BAIT还允许我们评估在交互式环境中构建的系统的端到端证明性能。这种统一视角揭示了一个改进先前工作的新型端到端系统。我们还提供了定性分析，表明改进的性能与语义感知更强的嵌入相关。通过简化ITP背景下机器学习算法的实现和比较，我们预计BAIT将成为未来研究的跳板。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
