Graph2Tac：形式数学概念的在线表示学习

在证明助手中，两个形式数学概念之间的物理邻近性是其相互相关性的强预测因子。此外，具有紧密邻近性的引理通常表现出相似的证明结构。我们表明，可以通过在线学习技术利用这一局部性，以获得在被要求证明未见数学环境中的定理时远超离线学习器的求解智能体。我们在 Coq 证明助手的 Tactician 平台中广泛基准测试了两个此类在线求解器：首先，Tactician 的在线 $k$-近邻求解器能够从最近的证明中学习，其证明定理数量较离线等价物提升了 $1.72\times$。其次，我们引入了一个图神经网络 Graph2Tac，其采用一种新方法为新定义构建层次表示。Graph2Tac 的在线定义任务在求解定理数量上较离线基线提升了 $1.5\times$。$k$-NN 和 Graph2Tac 求解器依赖正交的在线数据，使其高度互补。它们的组合较其各自性能提升了 $1.27\times$。两个求解器的表现均优于所有其他 Coq 通用证明器，包括 CoqHammer、Proverbot9001 和 transformer 基线至少 $1.48\times$，并可供终端用户实际使用。