内容简介：[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 PDFAbstract: 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 .
以上就是本文的全部内容，希望本文的内容对大家的学习或者工作能带来一定的帮助，也希望大家多多支持 码农网
本站部分资源来源于网络，本站转载出于传递更多信息之目的，版权归原作者或者来源机构所有，如转载稿涉及版权问题，请联系我们。
腾讯网UED体验设计之旅
任婕 等 / 电子工业出版社 / 2015-4 / 99.00元
《腾讯网UED体验设计之旅》是腾讯网UED的十年精华输出，涵盖了丰富的案例、极富冲击力的图片，以及来自腾讯网的一手经验，通过还原一系列真实案例的幕后设计故事，从用户研究、创意剖析、绘制方法、项目管理等实体案例出发，带领读者经历一场体验设计之旅。、 全书核心内容涉及网媒用户分析与研究方法、门户网站未来体验设计、H5技术在移动端打开的触控世界、手绘原创设计、改版迭代方法、文字及信息图形化设计、媒......一起来看看 《腾讯网UED体验设计之旅》 这本书的介绍吧!
