专栏首页arxiv.org翻译专栏Coq Proof Assistant的策略学习与证明(CS AI)
原创

Coq Proof Assistant的策略学习与证明(CS AI)

我们提出了一种利用机器学习在Coq Proof Assistant中进行战术证明搜索的系统。 与HOL4的Tactic Toe项目类似,我们的系统预测适当的战术,并以战术脚本的形式找到证据。 为了做到这一点,它学习了以前的战术脚本,以及它们如何应用于证明状态。 系统性能在Coq标准库上进行评估.. 目前,我们的预测器可以识别应用于23.4%的证明状态的正确策略。 我们的证明搜索器可以完全自动证明39.3%的引理。 当与CoqHammer系统相结合时,这两个系统共同证明了56.7%的库的引理。

原文题目:Tactic Learning and Proving for the Coq Proof Assistant

原文:We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs in the form of tactic scripts. To do this, it learns from previous tactic scripts and how they are applied to proof states. The performance of the system is evaluated on the Coq Standard Library. Currently, our predictor can identify the correct tactic to be applied to a proof state 23.4% of the time. Our proof searcher can fully automatically prove 39.3% of the lemmas. When combined with the CoqHammer system, the two systems together prove 56.7% of the library's lemmas.

原文作者:Lasse Blaauwbroek,Josef Urban,Herman Geuvers

原文地址:https://arxiv.org/abs/2003.09140

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 推和拖:水果收获机器人的主动障碍物分离方法(CS RO)

    选择性地采摘被障碍物包围的目标水果是水果收获机器人的主要挑战之一。与传统的避障方法不同,本文提出了一种结合了推和拖动作的主动式障碍物分离策略。分离运动和轨迹是基...

    时代在召唤
  • 在室内环境中使用二次曲面和对称属性的面向对象SLAM(CS RO)

    针对室内移动机器人的应用环境,提出了一种基于RGB-D摄像机的稀疏对象级SLAM算法。二次表示用作界标以紧凑地建模对象,包括对象的位置,方向和占用的空间。现有的...

    时代在召唤
  • 耳面部外科应用的RCM新机制(CS RO)

    由于中耳或鼻窦腔的插入区域非常狭窄,内窥镜的活动性降低为围绕虚拟点旋转和平移以插入相机。本文首先介绍了从三维扫描中获得的这些区域的解剖结构,然后介绍了一种基于敏...

    时代在召唤
  • 基于注意力的基于神经网络的远程监督情感态度提取(CS CL)

    在情感态度提取任务中,目标是识别文本中实体之间的情感关系。本文提供了一种在情感态度提取任务中基于注意力的上下文编码器的研究。基于此任务,采用两种类型的注意力上下...

    用户7454091
  • gcc命令

    在Linux底下搞开发,不可避免的要使用到gcc,gcc选项众多,下面记录下常见的一些选项,网上好多博客也说这个但是很多的都是不对的,我的博客记录参见man g...

    GavinZhou
  • 在SAP WebClient UI里使用AJAX进行异步数据读取

    For POC purpose I need to implement the AJAX functionality in Webclient UI compo...

    Jerry Wang
  • Face_Recognition_v3a

    In this assignment, you will build a face recognition system. Many of the ideas ...

    列夫托尔斯昊
  • LSTM生成尼采风格文章

    github地址 使用循环神经网络生成序列文本数据。循环神经网络可以用来生成音乐、图像作品、语音、对话系统对话等等。

    用户1631856
  • gcc x64 asm 内联汇编尝试

    asm volatile(assembler template : output : input : clobber);

    战神伽罗
  • PAT 1011 World Cup Betting (20分) 比较大小难度级别

    With the 2010 FIFA World Cup running, football fans the world over were becoming...

    vivi

扫码关注云+社区

领取腾讯云代金券