Session 4A

Chair: Geoff Sutcliffe

• 16:45: Jan Jakubuv, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, Josef Urban. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description).     See abstract ...
  ABSTRACT. We describe an implementation of gradient boosted and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems. For the gradient-boosted guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks and their embedding of the terms and clauses. The two methods are efficiently implemented in the E prover and its ENIGMA learning-guided framework and evaluated on the MPTP large-theory benchmark. Both methods are shown to achieve comparable real-time performance to state-of-the-art symbol-based methods.
• 17:00: Zsolt Zombori, Josef Urban. Prolog Technology Reinforcement Learning Prover (system description).     See abstract ...
  ABSTRACT. We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte Carlo Tree Search as done in the rlCoP system. Other components include a Python interface between plCoP and machine learners, and an external proof checker that verifies the validity of the plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) the learned guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We show that the code size compares favorably to rlCoP and argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.
• 17:15: Bernhard Gleiss, Martin Suda. Layered Clause Selection for Theory Reasoning (short paper).     See abstract ...
  ABSTRACT. Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of the search space where the chance to find a proof is low. In this paper we describe a new strategy for controlling the amount of reasoning with explicit theory axioms. The strategy refines a recently proposed two-layer-queue clause selection and combines it with a heuristical measure of the amount of theory reasoning in the derivation of a clause. We implemented the new strategy in the automatic theorem prover Vampire and present an evaluation showing that our work dramatically improves the state-of-the-art clause-selection strategy in the presence of theory axioms.
• 17:30: Zarathustra Goertzel. Make E Smart Again (short paper).     See abstract ...
  ABSTRACT. In this work in progress we demonstrate a new use-case for the ENIGMA system. The ENIGMA system using the XGBoost implementation of gradient boosted decision trees has shown high capability to learn to guide the E theorem prover's inferences in real time.
  In this work we strip E to the barebones: we replace the KBO6 term ordering with an identity relation as the minimal possible ordering, disable literal selection, and replace evolved strategies with the simple combination of the clause weight and FIFO (first in first out) evaluatino functions.
  We experimentally demonstrate that ENIGMA can learn to guide E as well as the smart, evolved strategies even without these staple automated theorem prover functionalities. To do this we need to experiment with XGBoost's meta-parameters over a dozen loops.