Fetching the paper…
Reading the bibliography…
Ensuring correctness is a pivotal aspect of software engineering.
Structured programming , volume 8 of A.P.I.C. Studies in data processing
Ole-Johan Dahl, Edsger W. Dijkstra, and Charles Antony Richard Hoare. 1972 · 1972
Earlier work this paper cites.
Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints
Patrick Cousot and Radhia Cousot. 1977 · 1977
Earlier work this paper cites.
Characterizing correctness properties of parallel programs using fixpoints
E. Allen Emerson and Edmund M. Clarke. 1980 · 1980
Earlier work this paper cites.
Specification and verification of concurrent systems in CESAR
Jean-Pierre Queille and Joseph Sifakis. 1982 · 1982
Earlier work this paper cites.
Proof style
John Harrison. 1996 · 1996
Earlier work this paper cites.
Data refinement: model-oriented proof methods and their comparison
W-P De Roever and Kai Engelhardt. 1998 · 1998
Earlier work this paper cites.
Symbolic model checking without bdds
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999 · 1999
Earlier work this paper cites.
Z3: an efficient SMT solver
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008 · 2008
Earlier work this paper cites.
A survey of automated techniques for formal software verification
Vijay Victor D’Silva, Daniel Kroening, and Georg Weissenbacher. 2008 · 2008
Earlier work this paper cites.
The probabilistic relevance framework: BM25 and beyond
Stephen E. Robertson and Hugo Zaragoza. 2009 · 2009
Earlier work this paper cites.
Comprehensive formal verification of an OS microkernel
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014 · 2014
Earlier work this paper cites.
Hammering towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. 2016 · 2016
Earlier work this paper cites.
Controlling linguistic style aspects in neural language generation
Jessica Ficler and Yoav Goldberg. 2017 · 2017
Earlier work this paper cites.
Hierarchical neural story generation
Angela Fan, Mike Lewis, and Yann N. Dauphin. 2018 · 2018
Cited alongside, same era.
Language models are few-shot learners
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. 2020 · 2020
Cited alongside, same era.
Language gans falling short
Massimo Caccia, Lucas Caccia, William Fedus, Hugo Larochelle, Joelle Pineau, and Laurent Charlin. 2020 · 2020
Cited alongside, same era.
The curious case of neural text degeneration
Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. 2020 · 2020
Cited alongside, same era.
Retrieval-augmented generation for knowledge-intensive NLP tasks
Patrick S. H. Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. 2020 · 2020
Cited alongside, same era.
The coq proof assistant
Coq. 2023 · 2023
Later among the works it cites.
The dafny programming and verification language
Dafny. 2023 · 2023
Later among the works it cites.
Baldur: Whole-proof generation and repair with large language models
Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023 · 2023
Later among the works it cites.
The isabelle proof assistant
Isabelle. 2023 · 2023
Later among the works it cites.
Draft, sketch, and prove: Guiding formal theorem provers with informal proofs
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023 · 2023
Later among the works it cites.
The lean project
Lean. 2023 · 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…
Lisa: Language models of isabelle proofs
Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021 · 2021
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óźdź, Piotr Mił oś, Yuhuai Wu, and Mateja Jamnik. 2022 · 2022
Cited alongside, same era.
Reacc: A retrieval-augmented code completion framework
Shuai Lu, Nan Duan, Hojae Han, Daya Guo, Seung-won Hwang, and Alexey Svyatkovskiy. 2022 · 2022
Cited alongside, same era.
minif2f: a cross-system benchmark for formal olympiad-level mathematics
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022 · 2022
Cited alongside, same era.
Self-rag: Learning to retrieve, generate, and critique through self-reflection
Akari Asai, Zeqiu Wu, Yizhong Wang, Avirup Sil, and Hannaneh Hajishirzi. 2023 · 2023
Cited alongside, same era.
Proofnet: Autoformalizing and formally proving undergraduate-level mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023 · 2023
Cited alongside, same era.
Tutorial on locales and locale interpretation
Clemens Ballarin. 2023 · 2023
Cited alongside, same era.
Chuyue Sun, Ying Sheng, Oded Padon, and Clark W. Barrett. 2023 · 2023
Later among the works it cites.
The verus project
Verus. 2023 · 2023
Later among the works it cites.
The isabelle system manual
Makarius Wenzel. 2023 · 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 Prenger, and Anima Anandkumar. 2023 · 2023
Later among the works it cites.
Leveraging large language models for automated proof synthesis in rust
Jianan Yao, Ziqiao Zhou, Weiteng Chen, and Weidong Cui. 2023 · 2023
Later among the works it cites.
Lyra: Orchestrating dual correction in automated theorem proving
Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. 2023 · 2023
Later among the works it cites.