深度网络引导的定理证明搜索
人工智能
2017-05-10 v1 机器学习
计算机科学中的逻辑
摘要
深度学习技术近年来处于多项重大人工智能进展的核心，包括物体识别与检测、图像字幕生成、机器翻译、语音识别与合成，以及围棋博弈。自动化一阶定理证明器有助于数学定理的形式化与验证，并在程序分析、理论推理、安全性、插值以及系统验证中发挥关键作用。本文提出在定理证明器E的证明搜索中采用基于深度学习的引导。我们在现有Mizar语句的ATP证明轨迹上训练并比较了若干深度神经网络模型，并利用它们在证明搜索过程中选择已处理子句。我们给出的实验证据表明，采用混合的两阶段方法，基于深度学习的引导能在增加证明定理数量的同时，显著减少证明搜索的平均步数。利用几种借助深度神经网络的证明引导策略，我们为Mizar数学图书馆定理的一阶逻辑翻译中此前未获得ATP生成证明的定理找到了7.36%的一阶证明。这使得语料库中拥有ATP生成证明的语句比例从56%提升至59%。
引用
@article{arxiv.1701.06972,
title = {Deep Network Guided Proof Search},
author = {Sarah Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk},
journal= {arXiv preprint arXiv:1701.06972},
year = {2017}
}