基于深度强化学习的高阶逻辑函数综合
人工智能
2020-04-27 v3 计算机科学中的逻辑
摘要
本文描述了一种基于证明辅助工具 HOL4 中自监督学习的深度强化学习框架。通过选择树神经网络（TNNs）作为机器学习模型，并在内部使用 HOL4 项来表示 TNN 的树结构，实现了机器学习模块与 HOL4 库之间的紧密交互。当任务被表达为搜索问题时，递归改进是可能的。在这种情况下，由 TNN 引导的蒙特卡洛树搜索（MCTS）算法可用于探索搜索空间并为训练下一个 TNN 生成更好的样本。作为示例，我们指定并学习了关于组合子与丢番图方程的项综合任务。我们在组合子综合问题上取得了 65% 的成功率，优于以其最佳通用策略集运行的最先进 ATP。我们通过解决 78.5% 的生成测试问题，为统计引导的丢番图方程综合开创了先例。
引用
@article{arxiv.1910.11797,
title = {Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic},
author = {Thibault Gauthier},
journal= {arXiv preprint arXiv:1910.11797},
year = {2020}
}