论文标题
机器学习符合赫布兰德宇宙
Machine Learning Meets The Herbrand Universe
论文作者
论文摘要
强大的基于CDCL的命题（SAT）求解器的出现大大提高了几个自动推理（AR）的领域。因此，AR的方向之一是将SAT求解器应用于诸如一阶逻辑之类的表达形式主义，如今存在大量的一般数学问题语料库。这是由于Herbrand的定理，因此可以通过实例化将一阶问题减少到命题问题。核心挑战是从典型的无限赫尔布兰德宇宙中选择正确的实例。在这项工作中，我们开发了针对此任务的第一个机器学习系统，以解决其组合和不变性属性。特别是，我们基于不变的图神经网络（GNN）开发了GNN2RNN架构，该体系结构从问题及其解决方案中学习，独立于符号名称（解决Skolems的丰度），并结合了一个经常性神经网络（RNN），该神经网络（RNN）提出了每个条款的实例化。然后，对架构进行了数学问题及其基于实例化的证据的培训，并以多种方式评估其性能。我们表明，训练有素的系统在预测正确的实例方面具有很高的准确性，并且能够通过与地面求解器结合使用时通过受过教育的猜测来解决许多问题。据我们所知，这是对机器学习的首次令人信服的用法，用于综合任意赫布兰德宇宙的相关元素。
The appearance of strong CDCL-based propositional (SAT) solvers has greatly advanced several areas of automated reasoning (AR). One of the directions in AR is thus to apply SAT solvers to expressive formalisms such as first-order logic, for which large corpora of general mathematical problems exist today. This is possible due to Herbrand's theorem, which allows reduction of first-order problems to propositional problems by instantiation. The core challenge is choosing the right instances from the typically infinite Herbrand universe. In this work, we develop the first machine learning system targeting this task, addressing its combinatorial and invariance properties. In particular, we develop a GNN2RNN architecture based on an invariant graph neural network (GNN) that learns from problems and their solutions independently of symbol names (addressing the abundance of skolems), combined with a recurrent neural network (RNN) that proposes for each clause its instantiations. The architecture is then trained on a corpus of mathematical problems and their instantiation-based proofs, and its performance is evaluated in several ways. We show that the trained system achieves high accuracy in predicting the right instances, and that it is capable of solving many problems by educated guessing when combined with a ground solver. To our knowledge, this is the first convincing use of machine learning in synthesizing relevant elements from arbitrary Herbrand universes.
