Learning to Prove Theorems via Interacting with Proof Assistants

栏目: IT技术 · 发布时间: 4年前

内容简介:[Submitted on 21 May 2019]

[Submitted on 21 May 2019]

Title: Learning to Prove Theorems via Interacting with Proof Assistants

Authors: Kaiyu Yang , Jia Deng

Download PDF

Abstract: Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts have to construct proofs manually by entering tactics into the proof assistant. In this paper, we study the problem of using machine learning to automate the interaction with proof assistants. We construct CoqGym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. We develop ASTactic, a deep learning-based model that generates tactics as programs in the form of abstract syntax trees (ASTs). Experiments show that ASTactic trained on CoqGym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. Code is available at this https URL .


以上就是本文的全部内容,希望本文的内容对大家的学习或者工作能带来一定的帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

史玉柱自述

史玉柱自述

优米网 / 同心出版社 / 2013-6-1 / 42.00元

史玉柱迄今为止唯一公开著作。 亲口讲述24年创业历程与营销心得。 中国商业思想史里程碑之作! 24年跌宕起伏,功成身退,史玉柱向您娓娓道来,历经时间沉淀的商业智慧和人生感悟。 在书中,史玉柱毫无保留地回顾了创业以来的经历和各阶段的思考。全书没有深奥的理论,铅华洗尽、朴实无华,往往在轻描淡写之间,一语道破营销的本质。 关于产品开发、营销传播、广告投放、团队管理、创业投资......一起来看看 《史玉柱自述》 这本书的介绍吧!

HTML 编码/解码
HTML 编码/解码

HTML 编码/解码

XML 在线格式化
XML 在线格式化

在线 XML 格式化压缩工具

UNIX 时间戳转换
UNIX 时间戳转换

UNIX 时间戳转换