Coq 的在线机器学习技术：一项对比研究
计算机科学中的逻辑
2021-06-08 v2 人工智能
摘要
我们针对 Coq 证明助手中的策略学习与证明，呈现若干在线机器学习技术的对比。本工作构建于 Tactician 之上，Tactician 是 Coq 的一个插件，可从用户书写的证明中学习以综合新证明。学习以在线方式进行，意味着 Tactician 的机器学习模型在用户每次于交互式证明中执行一步时立即更新。与更多被研究的离线学习系统相比，这具有重要优势：（1）它为用户提供无缝的交互式 Tactician 体验；（2）它利用证明相似性的局部性，即与当前证明相似的证明很可能邻近出现。我们实现了两种在线方法，即基于局部敏感哈希森林的近似 k 近邻和随机决策森林。此外，我们使用 XGBoost 在离线设置下对梯度提升树进行实验。我们在 Coq 标准库上比较了 Tactician 使用这三种学习方法的相对性能。
引用
@article{arxiv.2104.05207,
title = {Online Machine Learning Techniques for Coq: A Comparison},
author = {Liao Zhang and Lasse Blaauwbroek and Bartosz Piotrowski and Prokop Černý and Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:2104.05207},
year = {2021}
}
备注
Intelligent Computer Mathematics 14th International Conference, CICM 2021