v1v2 (latest)

Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity

17 February 2025

Dylan Zhang

Justin Wang

Tianran Sun

ArXiv (abs)PDF HTML HuggingFace (6 upvotes)

Papers citing "Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity"

36 / 36 papers shown

Title
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction Suozhi Huang Peiyang Song Robert Joseph George Julius Berner AI4TS LRM 196 3 0 25 Feb 2025
CoqPilot, a plugin for LLM-based generation of proofs Andrei Kozyrev Gleb Solovev Nikita Khramov Anton Podkopaev 78 8 0 25 Oct 2024
DafnyBench: A Benchmark for Formal Software Verification Chloe Loughridge Qinyi Sun Seth Ahrenbach Federico Cassano Chuyue Sun Ying Sheng Anish Mudide Md Rakib Hossain Misu Nada Amin Max Tegmark ALM AI4CE 139 21 0 12 Jun 2024
Magpie: Alignment Data Synthesis from Scratch by Prompting Aligned LLMs with Nothing Zhangchen Xu Fengqing Jiang Luyao Niu Yuntian Deng Radha Poovendran Yejin Choi Bill Yuchen Lin SyDa 167 213 0 12 Jun 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 130 123 0 23 May 2024
OpenRLHF: An Easy-to-use, Scalable and High-performance RLHF Framework Jian Hu Xibin Wu Wei Shen OpenLLMAI Team Dehao Zhang ... Weikai Fang Xianyu Yu Cao Haotian Xu Yiming Liu VLM AI4CE 260 0 0 20 May 2024
DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model DeepSeek-AI Aixin Liu Bei Feng Bin Wang Bingxuan Wang ... Zhuoshu Li Zihan Wang Zihui Gu Zilin Li Ziwei Xie MoE 276 700 0 07 May 2024
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Saikat Chakraborty Gabriel Ebner Siddharth Bhat Sarah Fakhoury Sakina Fatima Shuvendu K. Lahiri Nikhil Swamy 123 20 0 03 May 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 170 28 0 18 Apr 2024
CodecLM: Aligning Language Models with Tailored Synthetic Data Zifeng Wang Chun-Liang Li Vincent Perot Long T. Le Jin Miao Zizhao Zhang Chen-Yu Lee Tomas Pfister SyDa ALM 101 27 0 08 Apr 2024
StarCoder 2 and The Stack v2: The Next Generation Anton Lozhkov Raymond Li Loubna Ben Allal Federico Cassano J. Lamy-Poirier ... Sean M. Hughes Thomas Wolf Arjun Guha Leandro von Werra H. D. Vries OSLM ELM 131 451 0 29 Feb 2024
DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence Daya Guo Qihao Zhu Dejian Yang Zhenda Xie Kai Dong ... Yu-Huan Wu Yiming Li Fuli Luo Yingfei Xiong W. Liang ELM 184 1,053 0 25 Jan 2024
Magicoder: Empowering Code Generation with OSS-Instruct Yuxiang Wei Zhe Wang Jiawei Liu Yifeng Ding Lingming Zhang SyDa 159 160 0 04 Dec 2023
SWE-bench: Can Language Models Resolve Real-World GitHub Issues? Carlos E. Jimenez John Yang Alexander Wettig Shunyu Yao Kexin Pei Ofir Press Karthik Narasimhan ELM 228 947 0 10 Oct 2023
How Abilities in Large Language Models are Affected by Supervised Fine-tuning Data Composition Guanting Dong Hongyi Yuan Keming Lu Chengpeng Li Mingfeng Xue Dayiheng Liu Wei Wang Zheng Yuan Chang Zhou Jingren Zhou LRM CLL 150 189 0 09 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 236 93 0 01 Oct 2023
LMSYS-Chat-1M: A Large-Scale Real-World LLM Conversation Dataset Lianmin Zheng Wei-Lin Chiang Ying Sheng Tianle Li Siyuan Zhuang ... Zi Lin Eric P. Xing Joseph E. Gonzalez Ion Stoica Haotong Zhang 204 283 0 21 Sep 2023
Code Llama: Open Foundation Models for Code Baptiste Rozière Jonas Gehring Fabian Gloeckle Sten Sootla Itai Gat ... Hugo Touvron Louis Martin Nicolas Usunier Thomas Scialom Gabriel Synnaeve ELM ALM 250 2,414 0 24 Aug 2023
Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs Federico Cassano John Gouwar Francesca Lucchetti Claire Schlesinger Anders Freeman Carolyn Jane Anderson Molly Q. Feldman Michael Greenberg Abhinav Jangda Arjun Guha 243 49 0 19 Aug 2023
Large Language Model as Attributed Training Data Generator: A Tale of Diversity and Bias Yue Yu Yuchen Zhuang Jieyu Zhang Yu Meng Alexander Ratner Ranjay Krishna Jiaming Shen Chao Zhang ALM 199 275 0 28 Jun 2023
WizardCoder: Empowering Code Large Language Models with Evol-Instruct Ziyang Luo Can Xu Lu Wang Qingfeng Sun Xiubo Geng Wenxiang Hu Chongyang Tao Jing Ma Qingwei Lin Daxin Jiang ELM SyDa ALM 413 767 0 14 Jun 2023
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving Xueliang Zhao Wenda Li Lingpeng Kong 108 36 0 25 May 2023
LIMA: Less Is More for Alignment Chunting Zhou Pengfei Liu Puxin Xu Srini Iyer Jiao Sun ... Susan Zhang Gargi Ghosh M. Lewis Luke Zettlemoyer Omer Levy ALM 216 993 0 18 May 2023
OpenAssistant Conversations -- Democratizing Large Language Model Alignment Andreas Kopf Yannic Kilcher Dimitri von Rutte Sotiris Anagnostidis Zhi Rui Tam ... Arnav Dantuluri Andrew Maguire Christoph Schuhmann Huu Nguyen A. Mattick ALM LM&MA 228 711 0 14 Apr 2023
Teaching Large Language Models to Self-Debug Xinyun Chen Maxwell Lin Nathanael Scharli Denny Zhou LRM 313 801 0 11 Apr 2023
Self-Instruct: Aligning Language Models with Self-Generated Instructions Yizhong Wang Yeganeh Kordi Swaroop Mishra Alisa Liu Noah A. Smith Daniel Khashabi Hannaneh Hajishirzi ALM SyDa LRM 417 2,542 0 20 Dec 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 153 112 0 22 May 2022
Training a Helpful and Harmless Assistant with Reinforcement Learning from Human Feedback Yuntao Bai Andy Jones Kamal Ndousse Amanda Askell Anna Chen ... Jack Clark Sam McCandlish C. Olah Benjamin Mann Jared Kaplan 513 3,067 0 12 Apr 2022
CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis Erik Nijkamp Bo Pang Hiroaki Hayashi Lifu Tu Haiquan Wang Yingbo Zhou Silvio Savarese Caiming Xiong ELM 310 1,184 0 25 Mar 2022
Training language models to follow instructions with human feedback Long Ouyang Jeff Wu Xu Jiang Diogo Almeida Carroll L. Wainwright ... Amanda Askell Peter Welinder Paul Christiano Jan Leike Ryan J. Lowe OSLM ALM 1.6K 15,250 0 04 Mar 2022
Finetuned Language Models Are Zero-Shot Learners Jason W. Wei Maarten Bosma Vincent Zhao Kelvin Guu Adams Wei Yu Brian Lester Nan Du Andrew M. Dai Quoc V. Le ALM UQCV 620 4,172 0 03 Sep 2021
Program Synthesis with Large Language Models Jacob Austin Augustus Odena Maxwell Nye Maarten Bosma Henryk Michalewski ... Ellen Jiang Carrie J. Cai Michael Terry Quoc V. Le Charles Sutton ELM AIMat ReCod ALM 272 2,442 0 16 Aug 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 413 6,658 0 07 Jul 2021
LoRA: Low-Rank Adaptation of Large Language Models J. E. Hu Yelong Shen Phillip Wallis Zeyuan Allen-Zhu Yuanzhi Li Shean Wang Lu Wang Weizhu Chen OffRL AI4TS AI4CE ALM AIMat 1.2K 12,811 0 17 Jun 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 175 135 0 11 Feb 2021
Learning to Prove Theorems by Learning to Generate Theorems Mingzhe Wang Jia Deng NAI 177 53 0 17 Feb 2020