SATNet is an award-winning MAXSAT solver that can be used to infer logical rules and integrated as a differentiable layer in a deep neural network. It had been shown to solve Sudoku puzzles visually from examples of puzzle digit images, and was heralded as an impressive achievement towards the longstanding AI goal of combining pattern recognition with logical reasoning. In this paper, we clarify SATNet's capabilities by showing that in the absence of intermediate labels that identify individual Sudoku digit images with their logical representations, SATNet completely fails at visual Sudoku (0% test accuracy). More generally, the failure can be pinpointed to its inability to learn to assign symbols to perceptual phenomena, also known as the symbol grounding problem, which has long been thought to be a prerequisite for intelligent agents to perform real-world logical reasoning. We propose an MNIST based test as an easy instance of the symbol grounding problem that can serve as a sanity check for differentiable symbolic solvers in general. Naive applications of SATNet on this test lead to performance worse than that of models without logical reasoning capabilities. We report on the causes of SATNet's failure and how to prevent them.

SATNet是一个奖-winning的MAXSAT求解器，可以用来推断逻辑规则并作为深度神经网络中的可微分层。本文通过展示，在缺乏标识个别数独数字图像及其逻辑表示的中间标签的情况下，SATNet在视觉数独上彻底失败（0％的测试准确性），澄清了SATNet的能力。一般来说，这个失败可以归因于SATNet无法学会将符号分配给感知现象，也就是所谓的符号基础问题，这被认为是智能代理执行真实世界逻辑推理的先决条件。我们提出了基于MNIST的测试，作为符号基础问题的简单实例，可以作为可微分符号求解器的健全性检查。对于这个测试的SATNet的朴素应用导致性能比没有逻辑推理能力的模型更差。我们报告了SATNet失败的原因以及如何防止它们。

评估SATNet解决符号基础问题的能力