Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifiers to ensure output correctness. In this paper, we present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability, being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, our model learns better representations than models trained for classification only, with a much higher data efficiency -- requiring orders of magnitude less training data. NeuRes employs propositional resolution as a proof system to generate proofs of unsatisfiability and to accelerate the process of finding satisfying truth assignments, exploring both possibilities in parallel. To realize this, we propose an attention-based architecture that autoregressively selects pairs of clauses from a dynamic formula embedding to derive new clauses. Furthermore, we employ expert iteration whereby model-generated proofs progressively replace longer teacher proofs as the new ground truth. This enables our model to reduce a dataset of proofs generated by an advanced solver by ~32% after training on it with no extra guidance. This shows that NeuRes is not limited by the optimality of the teacher algorithm owing to its self-improving workflow. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.

翻译：在NP完全问题上训练神经网络通常需要大量训练数据，且常需结合计算成本高昂的符号验证器来确保输出正确性。本文提出NeuRes——一种神经符号方法，针对NP完全问题的典型代表命题可满足性问题同时应对这两项挑战。通过结合证书驱动训练与专家迭代，我们的模型相比仅训练分类任务的模型学习了更优的表示，且数据效率显著提升——所需训练数据量减少数个数量级。NeuRes采用命题归结作为证明系统，并行探索两种可能性：生成不可满足性证明与加速寻找可满足真值指派的过程。为实现这一目标，我们提出一种基于注意力机制的架构，该架构能自回归地从动态公式嵌入中选择子句对以推导新子句。此外，我们采用专家迭代策略，使模型生成的证明逐步替代更长的教师证明作为新的真实标注。这使得我们的模型在无额外指导的情况下，对高级求解器生成的证明数据集训练后能将其长度缩减约32%。这表明NeuRes凭借其自我改进的工作流程不受教师算法最优性的限制。实验证明我们的模型在正确分类实例与可证明实例两方面均远超NeuroSAT的性能表现。