BriefGPT.xyz
May, 2022
Isabelle密码机
The Isabelle ENIGMA
HTML
PDF
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock...
TL;DR
该研究结合学习与定理证明的多种方式显著提高了E自动定理证明器在Isabelle Sledgehammer问题上的性能，特别是在ENIGMA指导，神经前提选择和E的有针对性策略的开发方法上。最终的ENIGMA和前提选择系统在15秒内比E的最佳先前版本提高了25.3％，也优于所有其他先前的ATP和SMT系统。该方法可在从Isabelle提取的数十万个一阶未分类和已分类问题的几次迭代训练中进行训练。
Abstract
We significantly improve the performance of the E
automated theorem prover
on the
isabelle
Sledgehammer problems by combining
learning
and
→