论文标题
伊莎贝尔的谜
The Isabelle ENIGMA
论文作者
论文摘要
我们通过将学习和定理以多种方式结合证明，我们可以显着提高E自动定理供款在Isabelle大锤问题上的性能。特别是，我们开发了针对Isabelle问题的Onigma指南的有针对性版本，神经前提选择的有针对性版本以及E的目标策略。这些方法经过了数十万个未效率的未型和键入的一阶问题的培训。我们最终的最佳单策略和前提选择系统在15秒内提高了E前面版本的最佳版本25.3％，也表现出了所有其他以前的ATP和SMT系统。
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.
