从博弈博弈到符号推理：以 Alpha(Go) Zero 风格学习 SAT 求解器启发式
人工智能
2018-02-16 v1
摘要
尽管深度神经网络在图像与语音识别、自然语言处理以及强化学习等多个领域近期取得成效，我们在将数值优化能力引入符号推理方面仍面临巨大挑战。研究者已提出不同路径，例如用于证明合成的神经机器翻译、用于表征符号模式的符号与表达式向量化，以及将用于降维的神经后端与用于决策的符号前端相耦合。然而，这些初步探索仍仅是局部方案，且存在诸如缺乏正确性保证等其他缺陷。本文中，我们提出将符号推理建模为博弈，并直接在符号问题上以 Alpha(Go) Zero 风格运用深度强化学习的力量。以布尔可满足性（SAT）问题为例，我们展示了方法的可行性，以及模块化、高效性与正确性保证方面的优势。
引用
@article{arxiv.1802.05340,
title = {From Gameplay to Symbolic Reasoning: Learning SAT Solver Heuristics in the Style of Alpha(Go) Zero},
author = {Fei Wang and Tiark Rompf},
journal= {arXiv preprint arXiv:1802.05340},
year = {2018}
}