OpenAI研究 GamePad：定理证明的学习环境
在本文中，我们介绍了一个名为 GamePad 的系统，可用于探索机器学习方法在 Coq 证明助手中的定理证明应用。Coq 等交互式定理证明器使用户能够逐步构建机器可检查的证明。因此，它们提供了一个在人工监督下探索定理证明的机会。我们使用 GamePad 来合成一个简单的代数重写问题的证明，并为 Feit-Thompson 定理的形式化训练基线模型。我们处理位置评估（即预测剩余证明步骤的数量）和策略预测（即预测下一个证明步骤）任务，这些任务在基于策略的定理证明中自然出现。
相关文章
近期评论
-
来自： GPT-4V（ision）系统卡
-
来自： GPT-4V（ision）系统卡
-
来自： OpenAI研究 用对抗样本攻击机器学习