BriefGPT.xyz
Feb, 2021
利用语言模型进行定理证明的证明工件协同训练
Proof Artifact Co-training for Theorem Proving with Language Models
HTML
PDF
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu
TL;DR
本文介绍了 PACT 的一般方法，通过自我监督学习从内核级证明术语中提取丰富的数据，以协同常规战术预测目标，以提高定理证明的成功率。
Abstract
Labeled data for
imitation learning
of
theorem proving
in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is parti
→