图神经推理在证明布尔不可满足性时可能失效
机器学习
2019-09-30 v2 计算机科学中的逻辑
符号计算
机器学习
摘要
将图神经网络（GNNs）与逻辑推理的特性相桥接是可行且具实用价值的。尽管在求解布尔可满足性（SAT）问题上已见证大量努力与成功，基于 GNN 的求解器对于更复杂的谓词逻辑公式仍是一个谜。本工作中，我们结合若干证据猜想：一般定义的 GNNs 在证明布尔公式的不可满足性（UNSAT）方面存在若干局限。这意味着，若逻辑推理任务包含证明 UNSAT 这一被大多数谓词逻辑公式作为子问题的内容，GNNs 很可能无法学习此类逻辑推理任务。
引用
@article{arxiv.1909.11588,
title = {Graph Neural Reasoning May Fail in Certifying Boolean Unsatisfiability},
author = {Ziliang Chen and Zhanfu Yang},
journal= {arXiv preprint arXiv:1909.11588},
year = {2019}
}
备注
6 pages