Learning to Prove Theorems via Interacting with Proof Assistants

21 May 2019

ArXiv (abs)PDF HTML Github (403★)

Papers citing "Learning to Prove Theorems via Interacting with Proof Assistants"

43 / 93 papers shown

Title
LEGO-Prover: Neural Theorem Proving with Growing Libraries Haiming Wang Huajian Xin Chuanyang Zheng Lin Li Zhengying Liu ... Enze Xie Jian Yin Zhenguo Li Heng Liao Xiaodan Liang LRM 127 74 0 01 Oct 2023
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Kaiyu Yang Aidan M. Swope Alex Gu Rahul Chalamala Peiyang Song Shixing Yu Saad Godil R. Prenger Anima Anandkumar RALM 155 247 0 27 Jun 2023
Can Transformers Learn to Solve Problems Recursively? Shizhuo Zhang Curt Tigges Stella Biderman Maxim Raginsky Talia Ringer 54 17 0 24 May 2023
Transformer Models for Type Inference in the Simply Typed Lambda Calculus: A Case Study in Deep Learning for Code Alycia Lee Avraham Shinnar V. Pestun B. Trager 42 3 0 15 Mar 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 144 107 0 08 Mar 2023
Magnushammer: A Transformer-Based Approach to Premise Selection Maciej Mikuła Szymon Tworkowski Szymon Antoniak Bartosz Piotrowski Albert Qiaochu Jiang Jinyi Zhou Christian Szegedy Lukasz Kuciñski Piotr Milo's Yuhuai Wu 161 46 0 08 Mar 2023
CoProver: A Recommender System for Proof Construction Eric Yeh Briland Hitaj S. Owre Maena Quemener N. Shankar 111 5 0 01 Mar 2023
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics Zhangir Azerbayev Bartosz Piotrowski Hailey Schoelkopf Edward W. Ayers Dragomir R. Radev J. Avigad AIMat 83 84 0 24 Feb 2023
A Survey of Deep Learning for Mathematical Reasoning Pan Lu Liang Qiu Wenhao Yu Sean Welleck Kai-Wei Chang ReLM LRM 135 150 0 20 Dec 2022
Genetic Algorithm for Program Synthesis Yutaka Nagashima 76 1 0 22 Nov 2022
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Albert Q. Jiang Sean Welleck Jin Peng Zhou Wenda Li Jiacheng Liu M. Jamnik Timothée Lacroix Yuhuai Wu Guillaume Lample AIMat 160 181 0 21 Oct 2022
Project proposal: A modular reinforcement learning based automated theorem prover Boris Shminke 66 1 0 06 Sep 2022
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis Jonathan Laurent André Platzer 109 9 0 27 May 2022
Generating Natural Language Proofs with Verifier-Guided Search Kaiyu Yang Jia Deng Danqi Chen LRM 132 72 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 158 127 0 03 Feb 2022
Learning Symbolic Rules for Reasoning in Quasi-Natural Language Kaiyu Yang Jia Deng NAI ReLM LRM 61 13 0 23 Nov 2021
Generating Symbolic Reasoning Problems with Transformer GANs Jens U. Kreber Christopher Hahn AI4CE 115 6 0 19 Oct 2021
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics Kunhao Zheng Jesse Michael Han Stanislas Polu AIMat 154 178 0 31 Aug 2021
Graph Contrastive Pre-training for Effective Theorem Reasoning Zhaoyu Li Binghong Chen X. Si 61 5 0 24 Aug 2021
Contrastive Reinforcement Learning of Symbolic Reasoning Domains Gabriel Poesia Wenxin Dong Noah D. Goodman 180 19 0 16 Jun 2021
The Role of Entropy in Guiding a Connection Prover Zsolt Zombori Josef Urban Miroslav Olsák 64 11 0 31 May 2021
NaturalProofs: Mathematical Theorem Proving in Natural Language Sean Welleck Jiacheng Liu Ronan Le Bras Hannaneh Hajishirzi Yejin Choi Kyunghyun Cho AIMat 98 69 0 24 Mar 2021
Blindspots in Python and Java APIs Result in Vulnerable Code Yuriy Brun Tian Lin J. Somerville Elisha M Myers Natalie C. Ebner 63 7 0 10 Mar 2021
Training a First-Order Theorem Prover from Synthetic Data Vlad Firoiu Eser Aygun Ankit Anand Zafarali Ahmed Xavier Glorot Laurent Orseau Lei Zhang Doina Precup Shibl Mourad NAI 87 14 0 05 Mar 2021
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning Minchao Wu Michael Norrish Christian J. Walder Amir Dezfouli 73 42 0 19 Feb 2021
Proof Artifact Co-training for Theorem Proving with Language Models Jesse Michael Han Jason M. Rute Yuhuai Wu Edward W. Ayers Stanislas Polu AIMat 119 127 0 11 Feb 2021
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning Yuhuai Wu M. Rabe Wenda Li Jimmy Ba Roger C. Grosse Christian Szegedy AIMat LRM 144 57 0 15 Jan 2021
Faster Smarter Induction in Isabelle/HOL Yutaka Nagashima 93 7 0 19 Sep 2020
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq Lasse Blaauwbroek Josef Urban H. Geuvers 62 24 0 31 Jul 2020
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving Yuhuai Wu Albert Qiaochu Jiang Jimmy Ba Roger C. Grosse AIMat 115 55 0 06 Jul 2020
Retro: Learning Retrosynthetic Planning with Neural Guided A Search Binghong Chen Chengtao Li H. Dai Le Song 83 109 0 29 Jun 2020
Learning to Prove from Synthetic Theorems Eser Aygun Zafarali Ahmed Ankit Anand Vlad Firoiu Xavier Glorot Laurent Orseau Doina Precup Shibl Mourad NAI 70 20 0 19 Jun 2020
IsarStep: a Benchmark for High-level Mathematical Reasoning Wenda Li Lei Yu Yuhuai Wu Lawrence Charles Paulson AIMat LRM 77 10 0 13 Jun 2020
A framework for step-wise explaining how to solve constraint satisfaction problems B. Bogaerts Emilio Gamba Tias Guns LRM 32 17 0 11 Jun 2020
Mathematical Reasoning via Self-supervised Skip-tree Training M. Rabe Dennis Lee Kshitij Bansal Christian Szegedy ReLM LRM 47 2 0 08 Jun 2020
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek Josef Urban H. Geuvers 119 24 0 20 Mar 2020
Learning Compositional Rules via Neural Program Synthesis Maxwell Nye Armando Solar-Lezama J. Tenenbaum Brenden M. Lake NAI LRM 83 118 0 12 Mar 2020
Teaching Temporal Logics to Neural Networks Christopher Hahn Frederik Schmitt Jens U. Kreber M. Rabe Bernd Finkbeiner NAI 109 67 0 06 Mar 2020
Learning to Prove Theorems by Learning to Generate Theorems Mingzhe Wang Jia Deng NAI 135 50 0 17 Feb 2020
From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group) Zied Bouraoui Antoine Cornuéjols Thierry Denoeux Sebastien Destercke Didier Dubois ... Jérôme Mengin H. Prade Steven Schockaert M. Serrurier Christel Vrain 128 14 0 13 Dec 2019
Learning to Reason in Large Theories without Imitation Kshitij Bansal Christian Szegedy M. Rabe Sarah M. Loos Viktor Toman NAI LRM 118 42 0 25 May 2019
Graph Representations for Higher-Order Logic and Theorem Proving Aditya Sanjay Paliwal Sarah M. Loos M. Rabe Kshitij Bansal Christian Szegedy AI4CE NoLa 206 98 0 24 May 2019
Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning Gil Lederman M. Rabe Edward A. Lee Sanjit A. Seshia 89 38 0 20 Jul 2018