×

zbMATH — the first resource for mathematics

ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). (English) Zbl 07178977
Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer (ISBN 978-3-030-29435-9/pbk; 978-3-030-29436-6/ebook). Lecture Notes in Computer Science 11716. Lecture Notes in Artificial Intelligence, 197-215 (2019).
Summary: We describe an efficient implementation of given clause selection in saturation-based automated theorem provers, extending the previous ENIGMA approach. Unlike in the first ENIGMA implementation where a fast linear classifier is trained and used together with manually engineered features, we have started to experiment with more sophisticated state-of-the-art machine learning methods such as gradient boosted trees and recursive neural networks. In particular, the latter approach poses challenges in terms of efficiency of clause evaluation, however, we show that deep integration of the neural evaluation with the ATP data-structures can largely amortize this cost and lead to competitive real-time results. Both methods are evaluated on a large dataset of theorem proving problems and compared with the previous approaches. The resulting methods improve on the manually designed clause guidance, providing the first practically convincing application of gradient-boosted and neural clause guidance in saturation-style automated theorem provers.
For the entire collection see [Zbl 1428.68018].
MSC:
03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI