标题： GamePad：定理证明的学习环境 显示英文标题

标题： GamePad: A Learning Environment for Theorem Proving

摘要： 在本文中，我们引入了一个名为GamePad的系统，该系统可用于探索机器学习方法在Coq证明助手中的定理证明应用。 交互式定理证明器如Coq允许用户以逐步的方式构建可被机器检查的证明。 因此，它们提供了一个在人类监督下探索定理证明的机会。 我们使用GamePad为一个简单的代数重写问题合成证明，并为Feit-Thompson定理的形式化训练基线模型。 我们解决了位置评估（即，预测剩余的证明步骤数）和策略预测（即，预测下一步的证明步骤）任务，这些任务在基于策略的定理证明中自然出现。 显示英文摘要

摘要： In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct machine-checkable proofs in a step-by-step manner. Hence, they provide an opportunity to explore theorem proving with human supervision. We use GamePad to synthesize proofs for a simple algebraic rewrite problem and train baseline models for a formalization of the Feit-Thompson theorem. We address position evaluation (i.e., predict the number of proof steps left) and tactic prediction (i.e., predict the next proof step) tasks, which arise naturally in tactic-based theorem proving.