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

基于摘要分析。本文研究 Coq 证明助手在未见数学环境中的自动定理证明，利用形式化数学概念在组织位置上的邻近性与相关性、证明结构相似性之间的联系，通过在线学习适应新环境。核心贡献是 Graph2Tac：一种为新定义构建层次化表示的图神经网络，并与能够吸收近期证明的在线 k-nearest neighbor（k-NN）求解器进行对照和组合。 两种求解器均在 Tactician 平台实现。在线 k-NN 从近期证明中学习，Graph2Tac 则通过在线定义任务更新概念表示；摘要称二者依赖不同且互补的在线数据，但未给出具体图构造、训练目标、更新流程及资源开销。 作者报告，在其未见数学环境的评估中，在线 k-NN 证明的定理数量为对应离线版本的 1.72 倍，Graph2Tac 为离线基线的 1.5 倍；二者组合相对于单独使用的表现提升至 1.27 倍，具体比较口径尚待全文核对。作者还报告，两种求解器相较 CoqHammer、Proverbot9001 和 transformer 基线等通用 Coq 证明器，表现至少达到 1.48 倍。上述数字对应定理求解表现，不能解读为 Accuracy 或百分点变化；测试库、划分、搜索预算、消融及统计信息尚未验证。摘要称求解器已可供实际使用，但具体复现入口与运行条件需进一步核对。 平台推测（待验证）：可借鉴的是对两类在线信息来源分别建模、再检验互补性的思路，而非直接将形式化数学概念图迁移至 EEG。其原机制依赖可组织为层次关系的定义及可获得的近期证明，EEG 是否具有对应结构与监督信号尚不明确；因此不据此推断跨被试或跨会话收益。相关 EEG 工作尚未检索确认。