A Survey on Deep Learning for Theorem Proving

15 April 2024

Papers citing "A Survey on Deep Learning for Theorem Proving"

22 / 22 papers shown

Title
Knowledge Augmented Complex Problem Solving with Large Language Models: A Survey Da Zheng Lun Du Junwei Su Yuchen Tian Yuqi Zhu Jintian Zhang Lanning Wei Ningyu Zhang H. Chen LRM 39 0 0 06 May 2025
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 31 0 0 21 Oct 2024
AutoVerus: Automated Proof Generation for Rust Code Chenyuan Yang Xuheng Li Md Rakib Hossain Misu Jianan Yao Weidong Cui ... Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou Shan Lu 23 7 0 19 Sep 2024
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving Xiaohan Lin Qingxing Cao Yinya Huang Haiming Wang Jianqiao Lu Zhengying Liu Linqi Song Xiaodan Liang LRM 28 4 0 20 Jun 2024
Proving Olympiad Algebraic Inequalities without Human Demonstrations Chenrui Wei Mengzhou Sun Wei Wang LRM 34 6 0 20 Jun 2024
Process-Driven Autoformalization in Lean 4 Jianqiao Lu Zhengying Liu Yingjia Wan Yinya Huang Haiming Wang Zhicheng YANG Jing Tang Zhijiang Guo AI4CE 29 14 0 04 Jun 2024
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving Chenyang An Zhibo Chen Qihao Ye Emily First Letian Peng Jiayun Zhang Zihan Wang Sorin Lerner Jingbo Shang LRM 26 6 0 10 Apr 2024
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving Sean Lamont Michael Norrish Amir Dezfouli Christian J. Walder Paul Montague 28 1 0 06 Mar 2024
REFACTOR: Learning to Extract Theorems from Proofs Jin Peng Zhou Yuhuai Wu Qiyang Li Roger C. Grosse AIMat 26 1 0 26 Feb 2024
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 30 20 0 01 Oct 2023
gym-saturation: Gymnasium environments for saturation provers (System description) Boris Shminke 21 1 0 16 Sep 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 53 90 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 32 41 0 08 Mar 2023
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 58 154 0 21 Oct 2022
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought Abulhair Saparov He He ELM LRM ReLM 116 270 0 03 Oct 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 108 107 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 55 115 0 03 Feb 2022
Fast and Slow Enigmas and Parental Guidance Z. Goertzel Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban 36 11 0 14 Jul 2021
Explaining Answers with Entailment Trees Bhavana Dalvi Peter Alexander Jansen Oyvind Tafjord Zhengnan Xie Hannah Smith Leighanna Pipatanangkura Peter Clark ReLM FAtt LRM 235 184 0 17 Apr 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 58 51 0 15 Jan 2021
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling M. Crouse Ibrahim Abdelaziz Cristina Cornelio Veronika Thost Lingfei Wu Kenneth D. Forbus Achille Fokoue NAI AI4CE GNN 93 36 0 15 Nov 2019
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 48 131 0 10 Oct 2013