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.
