熵在引导连接证明器中的作用
人工智能
2021-07-19 v2 机器学习
计算机科学中的逻辑
摘要
在这项工作中，我们研究如何学习良好的算法以在定理证明中选择推理步骤。我们在 leanCoP 实现的连接表aux 演算中探索此问题，其中部分表aux 为可应用有限数目推理的干净紧凑的状态概念。我们首先将一个最先进的学习算法——图神经网络（GNN）——整合进 plCoP 定理证明器中。然后我们利用它在强化学习设定中观察系统行为，即从许多问题的成功蒙特卡洛树搜索中学习推理引导。尽管具有更好的模式匹配能力，GNN 初始表现不如先前使用的更简单的学习算法。我们观察到较简单算法的置信度更低，即其推荐具有更高熵。这引导我们探索通过神经网络实现的推理选择的熵如何影响证明搜索。这与人类不确定性下决策研究相关，特别是概率匹配理论。我们的主要结果表明适当的熵正则化，即训练 GNN 不要过度自信，极大提升了 plCoP 在大型数学语料库上的性能。
引用
@article{arxiv.2105.14706,
title = {The Role of Entropy in Guiding a Connection Prover},
author = {Zsolt Zombori and Josef Urban and Miroslav Olšák},
journal= {arXiv preprint arXiv:2105.14706},
year = {2021}
}