内容简介：[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 .
以上就是本文的全部内容，希望本文的内容对大家的学习或者工作能带来一定的帮助，也希望大家多多支持 码农网
猜你喜欢:
本站部分资源来源于网络，本站转载出于传递更多信息之目的，版权归原作者或者来源机构所有，如转载稿涉及版权问题，请联系我们。
你也能看得懂的Python算法书
王硕，董文馨，张舒行，张洁 著 / 电子工业出版社 / 2018-11-1 / 59.00
编程的核心是算法，学习算法不仅能教会你解决问题的方法，而且还能为你今后的发展提供一种可能。 《你也能看得懂的Python算法书》面向算法初学者，首先介绍当下流程的编程语言Python，详细讲解Python语言中的变量和循序、分支、循环三大结构，以及列表和函数的使用，为之后学习算法打好基础。然后以通俗易懂的语言讲解双指针、哈希、深度优先、广度优先、回溯、贪心、动态规划和至短路径等经典算法。 ......一起来看看 《你也能看得懂的Python算法书》 这本书的介绍吧!
