v1v2 (latest)

TacticToe: Learning to Prove with Tactics

2 April 2018

Papers citing "TacticToe: Learning to Prove with Tactics"

35 / 35 papers shown

Title
ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction Murari Ambati LRM 37 0 0 30 May 2025
Formal Mathematical Reasoning: A New Frontier in AI Kaiyu Yang Gabriel Poesia Jingxuan He Wenda Li Kristin Lauter Swarat Chaudhuri Dawn Song LRM AI4CE 157 36 0 20 Dec 2024
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically Kefan Dong Arvind V. Mahankali Tengyu Ma ReLM LRM 102 7 0 04 Nov 2024
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction Liao Zhang David M. Cerna C. Kaliszyk 57 0 0 02 Nov 2024
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 Leni Aniva Chuyue Sun Alycia Lee Clark W. Barrett Sanmi Koyejo 91 6 0 21 Oct 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Zijian Wu Jiayu Wang Dahua Lin Kai-xiang Chen 101 15 0 24 Jul 2024
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent Mahdi Buali Robert Hoehndorf 94 0 0 05 Jul 2024
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts Ruida Wang Jipeng Zhang Yizhen Jia Boyao Wang Shizhe Diao Renjie Pi Tong Zhang LRM 101 23 0 03 Jul 2024
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Saikat Chakraborty Gabriel Ebner Siddharth Bhat Sarah Fakhoury Sakina Fatima Shuvendu K. Lahiri Nikhil Swamy 86 16 0 03 May 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 103 10 0 18 Apr 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 123 32 0 15 Apr 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 93 5 0 06 Mar 2024
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving Sean Lamont Michael Norrish Amir Dezfouli Christian J. Walder Paul Montague 98 3 0 06 Mar 2024
Rigor with Machine Learning from Field Theory to the Poincaré Conjecture Sergei Gukov James Halverson Fabian Ruehle AI4CE 81 16 0 20 Feb 2024
Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry Pedro Quaresma Pierluigi Graziani Stefano M. Nicoletti 18 0 0 22 Jan 2024
A Survey of Reasoning with Foundation Models Jiankai Sun Chuanyang Zheng Enze Xie Zhengying Liu Ruihang Chu ... Xipeng Qiu Yi-Chen Guo Hui Xiong Qun Liu Zhenguo Li ReLM LRM AI4CE 209 85 0 17 Dec 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 150 247 0 27 Jun 2023
MizAR 60 for Mizar 50 Jan Jakubruv Karel Chvalovský Z. Goertzel C. Kaliszyk Mirek Olvsák Bartosz Piotrowski S. Schulz Martin Suda Josef Urban 82 13 0 12 Mar 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 141 107 0 08 Mar 2023
CoProver: A Recommender System for Proof Construction Eric Yeh Briland Hitaj S. Owre Maena Quemener N. Shankar 101 5 0 01 Mar 2023
A Survey of Deep Learning for Mathematical Reasoning Pan Lu Liang Qiu Wenhao Yu Sean Welleck Kai-Wei Chang ReLM LRM 133 150 0 20 Dec 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 157 181 0 21 Oct 2022
Feynman on Artificial Intelligence and Machine Learning, with Updates E. Mjolsness AI4CE 50 0 0 31 Aug 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 293 178 0 25 May 2022
HyperTree Proof Search for Neural Theorem Proving Guillaume Lample Marie-Anne Lachaux Thibaut Lavril Xavier Martinet Amaury Hayat Gabriel Ebner Aurelien Rodriguez Timothée Lacroix AIMat 98 151 0 23 May 2022
The Isabelle ENIGMA Z. Goertzel Jan Jakubruv C. Kaliszyk Miroslav Olvsák Jelle Piepenbrock Josef Urban AIMat 44 13 0 04 May 2022
Generating Symbolic Reasoning Problems with Transformer GANs Jens U. Kreber Christopher Hahn AI4CE 115 6 0 19 Oct 2021
Learning to solve geometric construction problems from images J. Macke J. Sedlar Miroslav Olsák J. Urban Josef Sivic 36 2 0 27 Jun 2021
The Role of Entropy in Guiding a Connection Prover Zsolt Zombori Josef Urban Miroslav Olsák 64 11 0 31 May 2021
Online Machine Learning Techniques for Coq: A Comparison Liao Zhang Lasse Blaauwbroek Bartosz Piotrowski Prokop Cerný C. Kaliszyk Josef Urban OffRL 42 11 0 12 Apr 2021
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning Minchao Wu Michael Norrish Christian J. Walder Amir Dezfouli 61 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 117 127 0 11 Feb 2021
Learning Equational Theorem Proving Jelle Piepenbrock Tom Heskes Mikolávs Janota Josef Urban AIMat LRM 33 4 0 10 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 87 7 0 19 Sep 2020