Autoformalization with Large Language Models

25 May 2022

Albert Q. Jiang

Papers citing "Autoformalization with Large Language Models"

46 / 46 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 61 0 0 17 May 2025
Autograding Mathematical Induction Proofs with Natural Language Processing Chenyan Zhao Mariana Silva Seth Poulsen AIMat 103 2 0 20 Feb 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 163 14 0 03 Jan 2025
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 155 4 0 18 Dec 2024
ZIP-FIT: Embedding-Free Data Selection via Compression-Based Alignment Elyas Obbad Iddah Mlauzi Brando Miranda Rylan Schaeffer Kamal Obbad Suhana Bedi Sanmi Koyejo CVBM 89 0 0 23 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Yeyun Gong Nan Duan Ping Wei AIMat 62 0 0 21 Oct 2024
Beyond Autoregression: Discrete Diffusion for Complex Reasoning and Planning Jiacheng Ye Jiahui Gao Shansan Gong Lin Zheng Xin Jiang Zhiyu Li Dianbo Sui DiffM LRM 124 23 0 18 Oct 2024
Planning Anything with Rigor: General-Purpose Zero-Shot Planning with LLM-based Formalized Programming Yilun Hao Yang Zhang Chuchu Fan LLMAG 102 17 0 15 Oct 2024
FLARE: Faithful Logic-Aided Reasoning and Exploration Erik Arakelyan Pasquale Minervini Pat Verga Patrick Lewis Isabelle Augenstein ReLM LRM 121 2 0 14 Oct 2024
Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks Rushang Karia Daniel Bramblett D. Dobhal Siddharth Srivastava ELM LRM 73 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 136 6 0 09 Oct 2024
Can Transformers Do Enumerative Geometry? Baran Hashemi Roderic G. Corominas Alessandro Giacchetto 487 3 0 27 Aug 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 117 29 0 14 Jul 2024
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 70 100 0 22 May 2022
PaLM: Scaling Language Modeling with Pathways Aakanksha Chowdhery Sharan Narang Jacob Devlin Maarten Bosma Gaurav Mishra ... Kathy Meier-Hellstern Douglas Eck J. Dean Slav Petrov Noah Fiedel PILM LRM 433 6,222 0 05 Apr 2022
Training Compute-Optimal Large Language Models Jordan Hoffmann Sebastian Borgeaud A. Mensch Elena Buchatskaya Trevor Cai ... Karen Simonyan Erich Elsen Jack W. Rae Oriol Vinyals Laurent Sifre AI4TS 180 1,941 0 29 Mar 2022
Memorizing Transformers Yuhuai Wu M. Rabe DeLesley S. Hutchins Christian Szegedy RALM 68 177 0 16 Mar 2022
Competition-Level Code Generation with AlphaCode Yujia Li David Choi Junyoung Chung Nate Kushman Julian Schrittwieser ... Esme Sutherland Robson Pushmeet Kohli Nando de Koray Kavukcuoglu Oriol Vinyals 83 1,372 0 08 Feb 2022
Proving Theorems using Incremental Learning and Hindsight Experience Replay Eser Aygun Laurent Orseau Ankit Anand Xavier Glorot Vlad Firoiu Lei M. Zhang Doina Precup Shibl Mourad CLL LRM 63 18 0 20 Dec 2021
Training Verifiers to Solve Math Word Problems K. Cobbe V. Kosaraju Mohammad Bavarian Mark Chen Heewoo Jun ... Jerry Tworek Jacob Hilton Reiichiro Nakano Christopher Hesse John Schulman ReLM OffRL LRM 227 4,392 0 27 Oct 2021
Generating Symbolic Reasoning Problems with Transformer GANs Jens U. Kreber Christopher Hahn AI4CE 61 6 0 19 Oct 2021
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 75 37 0 11 Oct 2021
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics Kunhao Zheng Jesse Michael Han Stanislas Polu AIMat 83 172 0 31 Aug 2021
Neural Circuit Synthesis from Specification Patterns Frederik Schmitt Christopher Hahn M. Rabe Bernd Finkbeiner 56 19 0 25 Jul 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 205 5,513 0 07 Jul 2021
Measuring Mathematical Problem Solving With the MATH Dataset Dan Hendrycks Collin Burns Saurav Kadavath Akul Arora Steven Basart Eric Tang D. Song Jacob Steinhardt ReLM FaML 147 2,249 0 05 Mar 2021
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning Minchao Wu Michael Norrish Christian J. Walder Amir Dezfouli 36 41 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 93 125 0 11 Feb 2021
The Pile: An 800GB Dataset of Diverse Text for Language Modeling Leo Gao Stella Biderman Sid Black Laurence Golding Travis Hoppe ... Horace He Anish Thite Noa Nabeshima Shawn Presser Connor Leahy AIMat 434 2,091 0 31 Dec 2020
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving Yuhuai Wu Albert Qiaochu Jiang Jimmy Ba Roger C. Grosse AIMat 84 55 0 06 Jul 2020
Language Models are Few-Shot Learners Tom B. Brown Benjamin Mann Nick Ryder Melanie Subbiah Jared Kaplan ... Christopher Berner Sam McCandlish Alec Radford Ilya Sutskever Dario Amodei BDL 706 41,736 0 28 May 2020
Teaching Temporal Logics to Neural Networks Christopher Hahn Frederik Schmitt Jens U. Kreber M. Rabe Bernd Finkbeiner NAI 86 66 0 06 Mar 2020
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar Qingxiang Wang C. Brown C. Kaliszyk Josef Urban AIMat AI4CE 109 51 0 05 Dec 2019
Learning to Reason in Large Theories without Imitation Kshitij Bansal Christian Szegedy M. Rabe Sarah M. Loos Viktor Toman NAI LRM 68 42 0 25 May 2019
Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning Gil Lederman M. Rabe Edward A. Lee Sanjit A. Seshia 53 38 0 20 Jul 2018
First Experiments with Neural Translation of Informal to Formal Mathematics Qingxiang Wang C. Kaliszyk Josef Urban AI4CE 61 60 0 10 May 2018
TacticToe: Learning to Prove with Tactics Thibault Gauthier C. Kaliszyk Josef Urban Ramana Kumar Michael Norrish 53 54 0 02 Apr 2018
Unsupervised Machine Translation Using Monolingual Corpora Only Guillaume Lample Alexis Conneau Ludovic Denoyer MarcÁurelio Ranzato SSL 110 1,096 0 31 Oct 2017
Hindsight Experience Replay Marcin Andrychowicz Dwight Crow Alex Ray Jonas Schneider Rachel Fong Peter Welinder Bob McGrew Joshua Tobin Pieter Abbeel Wojciech Zaremba OffRL 245 2,326 0 05 Jul 2017
Attention Is All You Need Ashish Vaswani Noam M. Shazeer Niki Parmar Jakob Uszkoreit Llion Jones Aidan Gomez Lukasz Kaiser Illia Polosukhin 3DV 656 131,414 0 12 Jun 2017
Accurate, Large Minibatch SGD: Training ImageNet in 1 Hour Priya Goyal Piotr Dollár Ross B. Girshick P. Noordhuis Lukasz Wesolowski Aapo Kyrola Andrew Tulloch Yangqing Jia Kaiming He 3DH 120 3,675 0 08 Jun 2017
Thinking Fast and Slow with Deep Learning and Tree Search Thomas W. Anthony Zheng Tian David Barber 93 395 0 23 May 2017
Deep Network Guided Proof Search Sarah M. Loos G. Irving Christian Szegedy C. Kaliszyk AIMat 68 159 0 24 Jan 2017
SGDR: Stochastic Gradient Descent with Warm Restarts I. Loshchilov Frank Hutter ODL 288 8,091 0 13 Aug 2016
DeepMath - Deep Sequence Models for Premise Selection Alexander A. Alemi François Chollet N. Eén G. Irving Christian Szegedy Josef Urban LRM AIMat 52 229 0 14 Jun 2016
Improving Neural Machine Translation Models with Monolingual Data Rico Sennrich Barry Haddow Alexandra Birch 241 2,716 0 20 Nov 2015