摘要

在本文中，我们展示了如何在存在大量潜在前提知识库的情况下进行自动定理证明，而无需从人类证明中学习。我们提出了一种探索机制，该机制在深度强化学习场景中通过基于tf-idf（词频-逆文档频率）的查找来混合选择额外的前提。这有助于探索和学习哪些前提是证明新定理所必需的。实验结果表明，采用这种探索机制训练的定理证明器优于仅基于人类证明训练的证明器，其性能接近于结合模仿学习和强化学习训练的证明器。我们进行了多次实验，以了解使我们的探索方法有效的基本假设的重要性，从而解释了我们的设计选择。