Title
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 12 0 0 09 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 26 0 0 27 Apr 2025
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries Huajian Xin Luming Li Xiaoran Jin Jacques Fleuriot Wenda Li AIMat 48 0 0 27 Apr 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 58 0 0 20 Feb 2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity Dylan Zhang Justin Wang Tianran Sun 36 0 0 17 Feb 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 96 1 0 18 Dec 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 31 0 0 21 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 37 3 0 09 Oct 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 25 7 0 19 Sep 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 61 22 0 14 Jul 2024
GenArtist: Multimodal LLM as an Agent for Unified Image Generation and Editing Zhenyu Wang Aoxue Li Zhenguo Li Xihui Liu MLLM DiffM 28 25 0 08 Jul 2024
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 6 15 0 16 Oct 2023
Generative Agents: Interactive Simulacra of Human Behavior J. Park Joseph C. O'Brien Carrie J. Cai Meredith Ringel Morris Percy Liang Michael S. Bernstein LM&Ro AI4CE 204 1,701 0 07 Apr 2023
Sparks of Artificial General Intelligence: Early experiments with GPT-4 Sébastien Bubeck Varun Chandrasekaran Ronen Eldan J. Gehrke Eric Horvitz ... Scott M. Lundberg Harsha Nori Hamid Palangi Marco Tulio Ribeiro Yi Zhang ELM AI4MH AI4CE ALM 197 2,232 0 22 Mar 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 53 90 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 34 41 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 58 154 0 21 Oct 2022
Discovering the Hidden Vocabulary of DALLE-2 Giannis Daras A. Dimakis 97 53 0 01 Jun 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 108 107 0 25 May 2022
Large Language Models are Zero-Shot Reasoners Takeshi Kojima S. Gu Machel Reid Yutaka Matsuo Yusuke Iwasawa ReLM LRM 291 2,712 0 24 May 2022
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 236 1,508 0 31 Dec 2020