ENIGMAWatch: ProofWatch meets ENIGMA

DOI10.1007/978-3-030-29026-9_21MaRDI QIDQ2180529zbMATH OpenOpenAlexFDO

Authors Jan Jakubův, Josef Urban, Zarathustra A. Goertzel

Publication date 14 May 2020

Full work available at URL https://arxiv.org/abs/1905.09565

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: In this work we describe a new learning-based proof guidance -- ENIGMAWatch -- for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the given-clause selection implemented for the E ATP system: ProofWatch and ENIGMA. ProofWatch is motivated by the watchlist (hints) method and based on symbolic matching of multiple related proofs, while ENIGMA is based on statistical machine learning. The two methods are combined by using the evolving information about symbolic proof matching as an additional information that characterizes the saturation-style proof search for the statistical learning methods. The new system is experimentally evaluated on a large set of problems from the Mizar Library. We show that the added proof-matching information is considered important by the statistical machine learners, and that it leads to improvements in E's Performance over ProofWatch and ENIGMA.

Recommendations

• ENIGMA: efficient learning-based inference guiding machine
• ProofWatch: watchlist guidance for large theories in E
• Enhancing ENIGMA given clause guidance
• Machine learning for first-order theorem proving
• Internal guidance for Satallax

Cited in

(11)

• Enhancing ENIGMA given clause guidance
• Improving ENIGMA-style clause selection while learning from history
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• ENIGMA: efficient learning-based inference guiding machine
• Internal guidance for Satallax
• Make E Smart Again (Short Paper)
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Prolog Technology Reinforcement Learning Prover
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Learning guided automated reasoning: a brief survey
• Fast and slow enigmas and parental guidance

Describes a project that uses

Uses Software

• ENIGMA

This page was built for publication: ENIGMAWatch: ProofWatch meets ENIGMA

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2180529)