Fetching the paper…
Reading the bibliography…
Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs).
Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow)
Lawrence C. Paulson · 1994
Earlier work this paper cites.
The coq proof assistant-reference manual
Projet Coq · 1996
Earlier work this paper cites.
A deductive database approach to automated geometry theorem proving and discovering
Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang · 2000
Earlier work this paper cites.
E–a brainiac theorem prover
Stephan Schulz · 2002
Earlier work this paper cites.
leancop: lean connection-based theorem proving
Jens Otten and Wolfgang Bibel · 2003
Earlier work this paper cites.
Proving the correctness of disk paxos
Mauro Jaskelioff and Stephan Merz · 2005
Earlier work this paper cites.
seL4: formal verification of an os kernel
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood · 2009
Earlier work this paper cites.
Ultimate automizer with smtinterpol - (competition contribution)
Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, and Andreas Podelski · 2013
Earlier work this paper cites.
First-order theorem proving and vampire
Laura Kovács and Andrei Voronkov · 2013
Earlier work this paper cites.
CBMC - C bounded model checker - (competition contribution)
Daniel Kroening and Michael Tautschnig · 2014
Earlier work this paper cites.
The lean theorem prover (system description)
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer · 2015
Earlier work this paper cites.
Learning invariants using decision trees
Siddharth Krishna, Christian Puhrsch, and Thomas Wies · 2015
Earlier work this paper cites.
Autocorres tool, 2016
David Greenaway · 2016
Earlier work this paper cites.
C-to-isabelle parser, version 1.13.0, may 2013
Michael Norrish · 2016
Earlier work this paper cites.
ESBMC 5.0: an industrial-strength C model checker
Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, and Denis A. Nicole · 2018
Cited alongside, same era.
Learning loop invariants for program verification
Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song · 2018
Cited alongside, same era.
Metamath: a computer language for mathematical proofs
Norman Megill and David A Wheeler · 2019
Cited alongside, same era.
In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020
The lean mathematical library · 2020
Cited alongside, same era.
Generative language modeling for automated theorem proving
Stanislas Polu and Ilya Sutskever · 2020
Cited alongside, same era.
Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix, and William El Sayed · 2023
Later among the works it cites.
Finding inductive loop invariants using large language models
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma · 2023
Later among the works it cites.
Wizardcoder: Empowering code large language models with evol-instruct
Ziyang Luo, Can Xu, Pu Zhao, Qingfeng Sun, Xiubo Geng, Wenxiang Hu, Chongyang Tao, Jing Ma, Qingwei Lin, and Daxin Jiang · 2023
Later among the works it cites.
OpenAI · 2023
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
CLN2INV: learning loop invariants with continuous logic networks
Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana · 2020
Cited alongside, same era.
Code2inv: A deep learning framework for program verification
Xujie Si, Aaditya Naik, Hanjun Dai, Mayur Naik, and Le Song · 2020
Cited alongside, same era.
Datasheets for datasets
Timnit Gebru, Jamie Morgenstern, Briana Vecchione, Jennifer Wortman Vaughan, Hanna M. Wallach, Hal Daumé III, and Kate Crawford · 2021
Cited alongside, same era.
Lora: Low-rank adaptation of large language models
Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen · 2021
Cited alongside, same era.
Lisa: Language models of isabelle proofs
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu · 2021
Cited alongside, same era.
Proof artifact co-training for theorem proving with language models
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu · 2022
Cited alongside, same era.
Thor: Wielding hammers to integrate language models and automated theorem provers
Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik · 2022
Cited alongside, same era.
Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang · 2023
Later among the works it cites.
Leandojo: Theorem proving with retrieval-augmented language models
Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar · 2023
Later among the works it cites.
Loop invariant inference through SMT solving enhanced reinforcement learning
Shiwen Yu, Ting Wang, and Ji Wang · 2023
Later among the works it cites.
Deepseek-coder: When the large language model meets programming - the rise of code intelligence
Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y. Wu, Y. K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang · 2024
Closest in time.
MUSTARD: Mastering uniform synthesis of theorem and proof data
Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang · 2024
Closest in time.
A survey on deep learning for theorem proving
Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si · 2024
Closest in time.
Process-driven autoformalization in lean 4, 2024
Jianqiao Lu, Zhengying Liu, Yingjia Wan, Yinya Huang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo · 2024
Closest in time.
LEGO-prover: Neural theorem proving with growing libraries
Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang · 2024
Closest in time.
Lemur: Integrating large language models in automated program verification
Haoze Wu, Clark Barrett, and Nina Narodytska · 2024
Closest in time.
Llamafactory: Unified efficient fine-tuning of 100+ language models
Yaowei Zheng, Richong Zhang, Junhao Zhang, Yanhan Ye, Zheyan Luo, and Yongqiang Ma · 2024
Closest in time.