LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

27 June 2023

Papers citing "LeanDojo: Theorem Proving with Retrieval-Augmented Language Models"

50 / 150 papers shown

Title
Reliable, Adaptable, and Attributable Language Models with Retrieval Akari Asai Zexuan Zhong Danqi Chen Pang Wei Koh Luke Zettlemoyer Hanna Hajishirzi Wen-tau Yih KELM RALM 49 55 0 05 Mar 2024
SynCode: LLM Generation with Grammar Augmentation Shubham Ugare Tarun Suresh Hangoo Kang Sasa Misailovic Gagandeep Singh 40 12 0 03 Mar 2024
Retrieval-Augmented Generation for AI-Generated Content: A Survey Penghao Zhao Hailin Zhang Qinhan Yu Zhengren Wang Yunteng Geng Fangcheng Fu Ling Yang Wentao Zhang Jie Jiang Bin Cui 3DV 132 235 0 29 Feb 2024
ArCHer: Training Language Model Agents via Hierarchical Multi-Turn RL Yifei Zhou Andrea Zanette Jiayi Pan Sergey Levine Aviral Kumar 65 51 0 29 Feb 2024
Securing Reliability: A Brief Overview on Enhancing In-Context Learning for Foundation Models Yunpeng Huang Yaonan Gu Jingwei Xu Zhihong Zhu Zhaorun Chen Xiaoxing Ma 43 3 0 27 Feb 2024
REFACTOR: Learning to Extract Theorems from Proofs Jin Peng Zhou Yuhuai Wu Qiyang Li Roger C. Grosse AIMat 45 7 0 26 Feb 2024
How Can LLM Guide RL? A Value-Based Approach Shenao Zhang Sirui Zheng Shuqi Ke Zhihan Liu Wanxin Jin Jianbo Yuan Yingxiang Yang Hongxia Yang Zhaoran Wang 35 8 0 25 Feb 2024
Stepwise Self-Consistent Mathematical Reasoning with Large Language Models Zilong Zhao Yao Rong Dongyang Guo Emek Gözlüklü Emir Gülboy Enkelejda Kasneci LRM 44 3 0 24 Feb 2024
LLMs Can Defend Themselves Against Jailbreaking in a Practical Manner: A Vision Paper Daoyuan Wu Shuaibao Wang Yang Liu Ning Liu AAML 39 7 0 24 Feb 2024
Hint-before-Solving Prompting: Guiding LLMs to Effectively Utilize Encoded Knowledge Jinlan Fu Shenzhen Huangfu Hang Yan See-Kiong Ng Xipeng Qiu LRM 50 7 0 22 Feb 2024
ChartX & ChartVLM: A Versatile Benchmark and Foundation Model for Complicated Chart Reasoning Renqiu Xia Bo-Wen Zhang Hancheng Ye Xiangchao Yan Qi Liu ... Min Dou Botian Shi Junchi Yan Junchi Yan Yu Qiao LRM 63 56 0 19 Feb 2024
FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems Yiming He Jia Zou Xiaokai Zhang Na Zhu Tuo Leng LRM 37 1 0 14 Feb 2024
VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search David Brandfonbrener Simon Henniger Sibi Raja Tarun Prasad Chloe Loughridge ... Sabrina Ruixin Hu Jianang Yang William E. Byrd Robert Zinkov Nada Amin LRM 59 6 0 13 Feb 2024
EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Johnathan Mercer 41 0 0 12 Feb 2024
InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning Huaiyuan Ying Shuo Zhang Linyang Li Zhejian Zhou Yunfan Shao ... Hang Yan Xipeng Qiu Jiayu Wang Kai-xiang Chen Dahua Lin ReLM LRM 34 71 0 09 Feb 2024
Understanding Reasoning Ability of Language Models From the Perspective of Reasoning Paths Aggregation Xinyi Wang Alfonso Amayuelas Kexun Zhang Liangming Pan Wenhu Chen Wei Wang LRM 40 12 0 05 Feb 2024
Learning Structure-Aware Representations of Dependent Types Konstantinos Kogkalidis Orestis Melkonian Jean-Philippe Bernardy NAI 34 1 0 03 Feb 2024
From RAG to QA-RAG: Integrating Generative AI for Pharmaceutical Regulatory Compliance Process Jaewoong Kim Moohong Min 49 0 0 26 Jan 2024
The Tactician's Web of Large-Scale Formal Knowledge Lasse Blaauwbroek 16 4 0 05 Jan 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts Lasse Blaauwbroek Miroslav Olšák Jason Rute F. I. S. Massolo Jelle Piepenbrock Vasily Pestun 17 10 0 05 Jan 2024
Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challenges Qingyao Li Lingyue Fu Weiming Zhang Xianyu Chen Jingwei Yu Wei Xia Weinan Zhang Ruiming Tang Yong Yu AI4Ed ELM 46 18 0 27 Dec 2023
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method Rahul Vishwakarma Subhankar Mishra AIMat 27 1 0 20 Dec 2023
A Survey of Reasoning with Foundation Models Jiankai Sun Chuanyang Zheng E. Xie Zhengying Liu Ruihang Chu ... Xipeng Qiu Yi-Chen Guo Hui Xiong Qun Liu Zhenguo Li ReLM LRM AI4CE 30 77 0 17 Dec 2023
Modeling Complex Mathematical Reasoning via Large Language Model based MathAgent Haoran Liao Qinyi Du Shaohua Hu Hao He Yanyan Xu Jidong Tian Yaohui Jin LRM AI4CE 40 1 0 14 Dec 2023
Large Language Models for Mathematicians Simon Frieder Julius Berner P. Petersen Thomas Lukasiewicz 13 4 0 07 Dec 2023
Inherent limitations of LLMs regarding spatial information He Yan Xinyao Hu Xiangpeng Wan Chengyu Huang Kai Zou Shiqi Xu LRM 36 2 0 05 Dec 2023
Meta Prompting for AI Systems Yifan Zhang Yang Yuan Andrew Chi-Chih Yao LLMAG LRM 29 5 0 20 Nov 2023
Multilingual Mathematical Autoformalization Albert Q. Jiang Wenda Li M. Jamnik AI4CE 37 19 0 07 Nov 2023
LLMSTEP: LLM proofstep suggestions in Lean Sean Welleck Rahul Saha 14 24 0 27 Oct 2023
Llemma: An Open Language Model For Mathematics Zhangir Azerbayev Hailey Schoelkopf Keiran Paster Marco Dos Santos Stephen Marcus McAleer Albert Q. Jiang Jia Deng Stella Biderman Sean Welleck CLL 40 275 0 16 Oct 2023
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models Jing Xiong Jianhao Shen Ye Yuan Haiming Wang Yichun Yin ... Yinya Huang Chuanyang Zheng Xiaodan Liang Ming Zhang Qun Liu AIMat LRM 24 15 0 16 Oct 2023
Let's reward step by step: Step-Level reward model as the Navigators for Reasoning Qianli Ma Haotian Zhou Tingkai Liu Jianbo Yuan Pengfei Liu Yang You Hongxia Yang LRM 35 43 0 16 Oct 2023
A New Approach Towards Autoformalization Nilay Patel Rahul Saha Jeffrey Flanigan AI4CE AIMat 26 3 0 12 Oct 2023
An In-Context Learning Agent for Formal Theorem-Proving Amitayush Thakur George Tsoukalas Yeming Wen Jimmy Xin Swarat Chaudhuri LLMAG 33 26 0 06 Oct 2023
Retrieval-augmented Generation to Improve Math Question-Answering: Trade-offs Between Groundedness and Human Preference Zachary Levonian Chenglu Li Wangda Zhu Anoushka Gade Owen Henkel Millie-Ellen Postle Wanli Xing AI4Ed RALM 23 32 0 04 Oct 2023
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 41 65 0 01 Oct 2023
MINT: Evaluating LLMs in Multi-turn Interaction with Tools and Language Feedback Xingyao Wang Zihan Wang Jiateng Liu Yangyi Chen Lifan Yuan Hao Peng Heng Ji LRM 133 142 0 19 Sep 2023
Security and Privacy on Generative Data in AIGC: A Survey Tao Wang Yushu Zhang Shuren Qi Ruoyu Zhao Zhihua Xia Jian Weng 64 44 0 18 Sep 2023
Large Language Models on Wikipedia-Style Survey Generation: an Evaluation in NLP Concepts Fan Gao Hang Jiang Rui Yang Qingcheng Zeng Jinghui Lu Moritz Blum Dairui Liu Tianwei She Yuang Jiang Irene Z Li ELM ALM LM&MA 35 8 0 21 Aug 2023
Cumulative Reasoning with Large Language Models Yifan Zhang Jingqin Yang Yang Yuan Andrew Chi-Chih Yao ReLM ELM LRM AI4CE 42 69 0 08 Aug 2023
A Comprehensive Overview of Large Language Models Humza Naveed Asad Ullah Khan Shi Qiu Muhammad Saqib Saeed Anwar Muhammad Usman Naveed Akhtar Nick Barnes Ajmal Mian OffRL 70 538 0 12 Jul 2023
Math Agents: Computational Infrastructure, Mathematical Embedding, and Genomics M. Swan Takashi Kido Eric Roland R. P. D. Santos AI4CE 29 10 0 04 Jul 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 67 95 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 52 44 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 75 159 0 21 Oct 2022
Training Language Models with Memory Augmentation Zexuan Zhong Tao Lei Danqi Chen RALM 249 128 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 112 158 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 91 118 0 03 Feb 2022
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning Yuhuai Wu M. Rabe Wenda Li Jimmy Ba Roger C. Grosse Christian Szegedy AIMat LRM 75 52 0 15 Jan 2021
Retrieval-Based Neural Code Generation Shirley Anugrah Hayati R. Olivier Pravalika Avvaru Pengcheng Yin A. Tomasic Graham Neubig 134 110 0 29 Aug 2018