Getting More out of Large Language Models for Proofs

HOList: An environment for machine learning of higher order logic theorem proving

Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox · 2019

Earlier work this paper cites.

Qed at large: A survey of engineering of formally verified software

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock · 2019

Earlier work this paper cites.

Tactok: Semantics-aware proof synthesis

Emily First, Yuriy Brun, and Arjun Guha · 2020

Earlier work this paper cites.

Generative language modeling for automated theorem proving, 2020

Stanislas Polu and Ilya Sutskever · 2020

Earlier work this paper cites.

Mpnet: Masked and permuted pre-training for language understanding, 2020

Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie-Yan Liu · 2020

Earlier work this paper cites.

Program synthesis with large language models, 2021

Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, and Charles Sutton · 2021

Cited alongside, same era.

Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning, 2021

Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli · 2021

Cited alongside, same era.

Diversity-driven automated formal verification

Emily First and Yuriy Brun · 2022

Cited alongside, same era.

Hypertree proof search for neural theorem proving, 2022

Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix · 2022

Cited alongside, same era.

Compilable neural code generation with compiler feedback, 2022

Xin Wang, Yasheng Wang, Yao Wan, Fei Mi, Yitong Li, Pingyi Zhou, Jin Liu, Hao Wu, Xin Jiang, and Qun Liu · 2022

Later among the works it cites.

Baldur: Whole-proof generation and repair with large language models, 2023

Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun · 2023

Closest in time.

Self-consistency improves chain of thought reasoning in language models, 2023

Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou · 2023

Closest in time.

Conversational automated program repair, 2023

Original

Chunqiu Steven Xia and Lingming Zhang · 2023

Closest in time.