面向有效定理推理的图对比预训练
机器学习
2021-08-25 v1
摘要
交互式定理证明是一个具有挑战性且繁琐的过程，需要非平凡的专业知识和人类专家提供的详细低级指令（或策略）。策略预测是实现该过程自动化的一种自然方式。现有方法通过学习基于人类专家所写证明的深度神经网络（DNN）模型，在策略预测上显示出有希望的结果。本文中，我们提出了 NeuroTactic，一种新颖的扩展，特别关注于改进定理证明的表示学习。NeuroTactic 利用图神经网络（GNN）来表示定理和前提，并应用图对比学习进行预训练。我们证明了定理的表示学习对于预测策略至关重要。与其他方法相比，NeuroTactic 在 CoqGym 数据集上达到了最先进的性能。
引用
@article{arxiv.2108.10821,
title = {Graph Contrastive Pre-training for Effective Theorem Reasoning},
author = {Zhaoyu Li and Binghong Chen and Xujie Si},
journal= {arXiv preprint arXiv:2108.10821},
year = {2021}
}