FMitF: Track I: Symbolic Reasoning with Graph Networks

尽管深度神经网络在图像识别、语音识别和机器翻译方面取得了成功，但在将深度学习技术应用于需要符号形式推理的应用程序--特别是证明各种逻辑中的定理--方面仍然存在巨大挑战。主要的挑战是代表性问题。在图像识别中，进步在很大程度上是由卷积神经网络推动的，卷积神经网络是深度学习的变种，它利用像素网格中固有的邻域关系。事实证明，这种表示法对二维游戏板也很有效：与强化学习相结合，卷积神经网络的变体被著名的游戏系统采用，包括DeepMind最初的Atari引擎，以及最近的AlphaGo和AlphaZero。然而，这些技术并不适用于通常用于表示逻辑推理的符号术语和公式，因为这些结构缺乏相同的数据丰富的结构和邻域关系。尽管在游戏动作和这样的公式之间进行类比是很有诱惑力的，但在确定如何在游戏领域取得的进展的基础上将其扩展到符号推理问题方面仍然存在重大挑战。该项目通过神经术语图的新概念来解决这一表示挑战，以表示强化学习框架内的公式和符号公式操作的中间状态。该项目将对受游戏启发的机器学习方法进行基础研究，以解决符号推理问题，包括布尔可满足性(SAT)、量化布尔公式(QBF)和一阶逻辑(FOL)。该项目将进一步将这些符号推理领域与统计关系学习联系起来，并探索它们在可解释人工智能和对抗性推理领域的应用。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Despite the success of deep neural networks in image recognition, speech recognition, and machine translation, big challenges remain in applying deep-learning techniques to applications that require symbolic forms of reasoning -- in particular, proving theorems in various kinds of logics. The main challenge is one of representation. In image recognition, advances are driven to a large extent by convolutional neural networks, a variation of deep learning, which exploit neighborhood relations inherent in a pixel grid. This representation has also turned out to work very well for two-dimensional game boards: combined with reinforcement-learning, variants of convolutional neural networks are employed by famous gameplay systems, including DeepMind's original Atari engine and more recently AlphaGo and AlphaZero. These techniques do not apply as well to symbolic terms and formulae often used to represent logical reasoning, however, because these constructs lack the same data-rich structure and neighborhood relations. Although it is tempting to draw analogies between game moves and such formulae, significant challenges remain in determining how to build upon the advances made in the domains of gameplay and extend them to symbolic-reasoning problems.The project addresses this representation challenge through a novel notion of neural term-graphs to represent formulae and intermediate states of symbolic formula manipulation within a reinforcement-learning framework. The project will conduct a fundamental study of gameplay-inspired machine-learning approaches to symbolic-reasoning problems, including boolean satisfiability (SAT), quantified boolean formulae (QBF), and first-order logic (FOL). The project will further connect these symbolic reasoning domains with statistical relational learning, and explore their application in the domains of explainable AI and adversarial inference.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.