ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

24 February 2023

Papers citing "ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics"

29 / 29 papers shown

Title
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation Junyu Lai Jiakun Zhang Shuo Xu Taolue Chen Zihang Wang Yao Yang Jiarui Zhang Chun Cao Jingwei Xu 96 0 0 17 May 2025
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques Sangjun Han Taeil Hur Youngmi Hur Kathy Sangkyung Lee Myungyoon Lee Hyojae Lim 468 0 0 20 Feb 2025
Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions Lan Zhang Marco Valentino André Freitas 108 1 0 17 Feb 2025
One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs Hai-Tao Zheng Jiayi Kuang Haojing Huang Zhikun Xu Xinnian Liang ... Jue Chen Chao Qu Ying Shen Hai-Tao Zheng Philip S. Yu LRM 127 2 0 12 Feb 2025
Examining False Positives under Inference Scaling for Mathematical Reasoning Yu Guang Wang Nan Yang Liang Wang Furu Wei LRM 128 4 0 10 Feb 2025
Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning Yanfang Zhang Yiliu Sun Yibing Zhan Dapeng Tao Dacheng Tao Chen Gong LRM AI4CE LLMAG 157 2 0 28 Jan 2025
Mathematical Language Models: A Survey Wen Liu Hanglei Hu Jie Zhou Yuyang Ding Junsong Li ... Mengliang He Qin Chen Bo Jiang Aimin Zhou Liang He LRM 213 14 0 03 Jan 2025
MIND: Math Informed syNthetic Dialogues for Pretraining LLMs Syeda Nahida Akter Shrimai Prabhumoye John Kamalu S. Satheesh Eric Nyberg M. Patwary Mohammad Shoeybi Bryan Catanzaro LRM SyDa ReLM 161 2 0 15 Oct 2024
Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks Rushang Karia Daniel Bramblett D. Dobhal Siddharth Srivastava ELM LRM 107 0 0 11 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 165 8 0 09 Oct 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 140 10 0 05 Aug 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 141 29 0 14 Jul 2024
Improving Autoformalization using Type Checking Auguste Poiroux Gail Weiss Viktor Kunčak Antoine Bosselut 108 4 0 11 Jun 2024
Large Language Models Michael R Douglas LLMAG LM&MA 140 644 0 11 Jul 2023
The unreasonable effectiveness of few-shot learning for machine translation Xavier Garcia Yamini Bansal Colin Cherry George F. Foster M. Krikun Fan Feng Melvin Johnson Orhan Firat 104 108 0 02 Feb 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 132 180 0 21 Oct 2022
Solving Quantitative Reasoning Problems with Language Models Aitor Lewkowycz Anders Andreassen David Dohan Ethan Dyer Henryk Michalewski ... Theo Gutman-Solo Yuhuai Wu Behnam Neyshabur Guy Gur-Ari Vedant Misra ReLM ELM LRM 181 859 0 29 Jun 2022
NaturalProver: Grounded Mathematical Proof Generation with Language Models Sean Welleck Jiacheng Liu Ximing Lu Hannaneh Hajishirzi Yejin Choi AIMat LRM 75 73 0 25 May 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 291 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 82 151 0 23 May 2022
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers Albert Q. Jiang Wenda Li Szymon Tworkowski K. Czechowski Tomasz Odrzygó'zd'z Piotr Milo's Yuhuai Wu M. Jamnik AIMat LRM 87 103 0 22 May 2022
Memorizing Transformers Yuhuai Wu M. Rabe DeLesley S. Hutchins Christian Szegedy RALM 100 178 0 16 Mar 2022
Unsupervised Neural Machine Translation with Generative Language Models Only Jesse Michael Han Igor Babuschkin Harrison Edwards Arvind Neelakantan Tao Xu ... Alex Ray Pranav Shyam Aditya A. Ramesh Alec Radford Ilya Sutskever 105 37 0 11 Oct 2021
Evaluating Large Language Models Trained on Code Mark Chen Jerry Tworek Heewoo Jun Qiming Yuan Henrique Pondé ... Bob McGrew Dario Amodei Sam McCandlish Ilya Sutskever Wojciech Zaremba ELM ALM 238 5,675 0 07 Jul 2021
NaturalProofs: Mathematical Theorem Proving in Natural Language Sean Welleck Jiacheng Liu Ronan Le Bras Hannaneh Hajishirzi Yejin Choi Kyunghyun Cho AIMat 72 69 0 24 Mar 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 103 126 0 11 Feb 2021
Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm David Silver Thomas Hubert Julian Schrittwieser Ioannis Antonoglou Matthew Lai ... D. Kumaran T. Graepel Timothy Lillicrap Karen Simonyan Demis Hassabis 159 1,785 0 05 Dec 2017
Unsupervised Machine Translation Using Monolingual Corpora Only Guillaume Lample Alexis Conneau Ludovic Denoyer MarcÁurelio Ranzato SSL 153 1,098 0 31 Oct 2017
DeepMath - Deep Sequence Models for Premise Selection Alexander A. Alemi François Chollet N. Eén G. Irving Christian Szegedy Josef Urban LRM AIMat 86 230 0 14 Jun 2016