Communities
Connect sessions
AI calendar
Organizations
Join Slack
Contact Sales
Search
Open menu
Home
Papers
2306.15626
Cited By
v1
v2 (latest)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Neural Information Processing Systems (NeurIPS), 2023
27 June 2023
Kaiyu Yang
Aidan M. Swope
Alex Gu
Rahul Chalamala
Peiyang Song
Shixing Yu
Saad Godil
R. Prenger
Anima Anandkumar
RALM
Re-assign community
ArXiv (abs)
PDF
HTML
HuggingFace (17 upvotes)
Papers citing
"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models"
50 / 192 papers shown
ImProver: Agent-Based Automated Proof Optimization
International Conference on Learning Representations (ICLR), 2024
Riyaz Ahuja
Jeremy Avigad
Prasad Tetali
Sean Welleck
LLMAG
301
4
0
07 Oct 2024
Consistent Autoformalization for Constructing Mathematical Libraries
Conference on Empirical Methods in Natural Language Processing (EMNLP), 2024
Lan Zhang
Xin Quan
André Freitas
AI4CE
214
14
0
05 Oct 2024
Easy2Hard-Bench: Standardized Difficulty Labels for Profiling LLM Performance and Generalization
Neural Information Processing Systems (NeurIPS), 2024
Mucong Ding
Chenghao Deng
Jocelyn Choo
Zichu Wu
Aakriti Agrawal
...
Wanrong Zhu
Tom Goldstein
John Langford
Anima Anandkumar
Furong Huang
354
18
0
27 Sep 2024
In-Context Learning May Not Elicit Trustworthy Reasoning: A-Not-B Errors in Pretrained Language Models
Conference on Empirical Methods in Natural Language Processing (EMNLP), 2024
Pengrui Han
Peiyang Song
Haofei Yu
Jiaxuan You
ReLM
LRM
194
5
0
23 Sep 2024
Retrieval Augmented Generation (RAG) and Beyond: A Comprehensive Survey on How to Make your LLMs use External Data More Wisely
Siyun Zhao
Yuqing Yang
Zilong Wang
Zhiyuan He
Luna Qiu
Lili Qiu
SyDa
RALM
3DV
338
96
0
23 Sep 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
456
28
0
19 Sep 2024
Great Memory, Shallow Reasoning: Limits of
k
k
k
NN-LMs
North American Chapter of the Association for Computational Linguistics (NAACL), 2024
Shangyi Geng
Wenting Zhao
Alexander M. Rush
RALM
ReLM
LRM
246
7
0
21 Aug 2024
KAN 2.0: Kolmogorov-Arnold Networks Meet Science
Ziming Liu
Pingchuan Ma
Yixuan Wang
Wojciech Matusik
Max Tegmark
363
163
0
19 Aug 2024
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
International Conference on Software Engineering (ICSE), 2024
Alex Sanchez-Stern
Abhishek Varghese
Zhanna Kaufman
Dylan Zhang
Talia Ringer
Yuriy Brun
572
4
0
17 Aug 2024
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Huajian Xin
Zhaochun Ren
Junxiao Song
Zhihong Shao
Wanjia Zhao
...
Dejian Yang
Zhibin Gou
Z. F. Wu
Fuli Luo
Chong Ruan
AIMat
LRM
291
138
0
15 Aug 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts
International Conference on Learning Representations (ICLR), 2024
Jiewen Hu
Thomas Zhu
Sean Welleck
AIMat
474
23
0
05 Aug 2024
Mission Impossible: A Statistical Perspective on Jailbreaking LLMs
Neural Information Processing Systems (NeurIPS), 2024
Jingtong Su
Mingyu Lee
SangKeun Lee
217
24
0
02 Aug 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover
Zijian Wu
Jiayu Wang
Dahua Lin
Kai-xiang Chen
307
24
0
24 Jul 2024
Retrieval-Enhanced Machine Learning: Synthesis and Opportunities
To Eun Kim
Alireza Salemi
Andrew Drozdov
Fernando Diaz
Hamed Zamani
376
11
0
17 Jul 2024
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
George Tsoukalas
Jasper Lee
John Jennings
Jimmy Xin
Michelle Ding
Michael Jennings
Amitayush Thakur
Swarat Chaudhuri
LRM
AIMat
271
85
0
15 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving
Haohan Lin
Zhiqing Sun
Yiming Yang
Sean Welleck
ReLM
LRM
752
50
0
14 Jul 2024
Solving General Natural-Language-Description Optimization Problems with Large Language Models
Jihai Zhang
Wei Wang
Siyan Guo
Li Wang
Fangquan Lin
Cheng Yang
Wotao Yin
168
20
0
09 Jul 2024
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent
Mahdi Buali
Robert Hoehndorf
254
0
0
05 Jul 2024
Learning Formal Mathematics From Intrinsic Motivation
Gabriel Poesia
David Broman
Nick Haber
Noah D. Goodman
LRM
317
30
0
30 Jun 2024
Towards Large Language Model Aided Program Refinement
YuFan Cai
Zhe Hou
Xiaokun Luan
David Miguel Sanan Baena
Yun Lin
Jun Sun
Jin Song Dong
179
5
0
26 Jun 2024
From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models
Sean Welleck
Amanda Bertsch
Matthew Finlayson
Hailey Schoelkopf
Alex Xie
Graham Neubig
Ilia Kulikov
Zaid Harchaoui
400
113
0
24 Jun 2024
Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods
George Granberry
Wolfgang Ahrendt
Moa Johansson
286
7
0
21 Jun 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
167
22
0
20 Jun 2024
Proving Olympiad Algebraic Inequalities without Human Demonstrations
Chenrui Wei
Mengzhou Sun
Wei Wang
LRM
246
14
0
20 Jun 2024
miniCodeProps: a Minimal Benchmark for Proving Code Properties
Evan Lohn
Sean Welleck
188
15
0
16 Jun 2024
Reliable Evaluation and Benchmarks for Statement Autoformalization
Auguste Poiroux
Gail Weiss
Viktor Kuncak
Antoine Bosselut
434
10
0
11 Jun 2024
Can I understand what I create? Self-Knowledge Evaluation of Large Language Models
Zhiquan Tan
Lai Wei
Yongfeng Zhang
Xing Xie
Weiran Huang
ELM
LRM
197
6
0
10 Jun 2024
SelfDefend: LLMs Can Defend Themselves against Jailbreaking in a Practical Manner
Xunguang Wang
Daoyuan Wu
Zhenlan Ji
Zongjie Li
Pingchuan Ma
Shuai Wang
Yingjiu Li
Yang Liu
Ning Liu
Juergen Rahmel
AAML
485
35
0
08 Jun 2024
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
Huaiyuan Ying
Zijian Wu
Yihan Geng
Zheng Yuan
Dahua Lin
Kai Chen
518
88
0
06 Jun 2024
RATT: A Thought Structure for Coherent and Correct LLM Reasoning
Jinghan Zhang
Xiting Wang
Weijieying Ren
Lu Jiang
Dongjie Wang
Kunpeng Liu
LRM
462
39
0
04 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
396
35
0
04 Jun 2024
Autoformalizing Euclidean Geometry
Logan Murphy
Kaiyu Yang
Jialiang Sun
Zhaoyu Li
A. Anandkumar
Xujie Si
232
14
0
27 May 2024
Empowering Large Language Models to Set up a Knowledge Retrieval Indexer via Self-Learning
Xun Liang
Pengnian Qi
Zhiyu Li
Sensen Zhang
Chenyang Xi
Ding Chen
Hanyu Wang
Feiyu Xiong
Shichao Song
Chunyu Li
RALM
221
15
0
27 May 2024
Models That Prove Their Own Correctness
Noga Amit
S. Goldwasser
Orr Paradise
G. Rothblum
LRM
469
5
0
24 May 2024
Proving Theorems Recursively
Neural Information Processing Systems (NeurIPS), 2024
Haiming Wang
Huajian Xin
Zhengying Liu
Wenda Li
Yinya Huang
...
Zhicheng YANG
Jing Tang
Jian Yin
Zhenguo Li
Xiaodan Liang
LRM
221
24
0
23 May 2024
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
Huajian Xin
Daya Guo
Zhihong Shao
Zhaochun Ren
Qihao Zhu
Bo Liu
Chong Ruan
Wenda Li
Xiaodan Liang
SyDa
298
159
0
23 May 2024
HoneyBee: A Scalable Modular Framework for Creating Multimodal Oncology Datasets with Foundational Embedding Models
Aakash Tripathi
Asim Waqas
M. Schabath
Yasin Yilmaz
Ghulam Rasool
562
6
0
13 May 2024
ATG: Benchmarking Automated Theorem Generation for Generative Language Models
Xiaohan Lin
Qingxing Cao
Yinya Huang
Zhicheng YANG
Zhengying Liu
Zhenguo Li
Xiaodan Liang
284
9
0
05 May 2024
Generating Probabilistic Scenario Programs from Natural Language
Karim Elmaaroufi
Devan Shankar
Ana Cismaru
Marcell Vazquez-Chanlatte
Alberto L. Sangiovanni-Vincentelli
Matei A. Zaharia
Sanjit A. Seshia
262
15
0
03 May 2024
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
International Conference on Software Engineering (ICSE), 2024
Saikat Chakraborty
Gabriel Ebner
Siddharth Bhat
Sarah Fakhoury
Sakina Fatima
Shuvendu K. Lahiri
Nikhil Swamy
220
23
0
03 May 2024
Towards Green AI: Current status and future research
Christian Clemm
Lutz Stobbe
Kishan Wimalawarne
Jan Druschke
262
8
0
01 May 2024
LLM-SR: Scientific Equation Discovery via Programming with Large Language Models
Parshin Shojaee
Kazem Meidani
Shashank Gupta
A. Farimani
Chandan K. Reddy
585
55
0
29 Apr 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
Peiyang Song
Kaiyu Yang
A. Anandkumar
389
10
0
18 Apr 2024
A Survey on Deep Learning for Theorem Proving
Zhaoyu Li
Jialiang Sun
Logan Murphy
Qidong Su
Zenan Li
Xian Zhang
Kaiyu Yang
Xujie Si
LRM
294
51
0
15 Apr 2024
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
Annual Meeting of the Association for Computational Linguistics (ACL), 2024
Chenyang An
Zhibo Chen
Qihao Ye
Emily First
Letian Peng
Jiayun Zhang
Zihan Wang
Sorin Lerner
Jingbo Shang
LRM
368
11
0
10 Apr 2024
LeanReasoner: Boosting Complex Logical Reasoning with Lean
Dongwei Jiang
Marcio Fonseca
Shay B. Cohen
LRM
243
29
0
20 Mar 2024
StateFlow: Enhancing LLM Task-Solving through State-Driven Workflows
Yiran Wu
Tianwei Yue
Shaokun Zhang
Chi Wang
Qingyun Wu
274
43
0
17 Mar 2024
Learning Guided Automated Reasoning: A Brief Survey
Lasse Blaauwbroek
David M. Cerna
Thibault Gauthier
Jan Jakubruv
C. Kaliszyk
Martin Suda
Josef Urban
LRM
277
7
0
06 Mar 2024
Reliable, Adaptable, and Attributable Language Models with Retrieval
Akari Asai
Zexuan Zhong
Danqi Chen
Pang Wei Koh
Luke Zettlemoyer
Hanna Hajishirzi
Anuj Kumar
KELM
RALM
340
82
0
05 Mar 2024
SynCode: LLM Generation with Grammar Augmentation
Shubham Ugare
Tarun Suresh
Hangoo Kang
Sasa Misailovic
Gagandeep Singh
296
37
0
03 Mar 2024
Previous
1
2
3
4
Next
Page 3 of 4
