摘要

在现代人工智能系统中，将逻辑推理整合到深度学习架构内一直是一个主要目标。本文提出了一种新的方向，通过引入一个可微分（平滑）的最大可满足性（MAXSAT）求解器来实现这一目标，该求解器可以嵌入到更大的深度学习系统中。我们的（近似）求解器基于一种快速坐标下降方法，用于解决与MAXSAT问题相关的半定规划（SDP）。我们展示了如何对这个SDP的解进行解析微分，并高效地解决相应的反向传播问题。我们证明了通过将此求解器集成到端到端学习系统中，可以在最少监督的情况下学习复杂问题的逻辑结构。特别是，我们展示了如何仅通过单比特监督（这是传统上对深度网络来说较为困难的任务）来学习奇偶函数，以及如何仅从示例中学会玩9x9数独游戏。此外，我们还解决了“视觉数独”问题，该问题将数独谜题的图像映射到其对应的逻辑解决方案，这通过将我们的MAXSAT求解器与传统的卷积架构相结合来实现。因此，我们的方法在将逻辑结构整合到深度学习中显示出潜力。