v1v2v3 (latest)

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

18 December 2024

Papers citing "Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification"

38 / 38 papers shown

Title
VERINA: Benchmarking Verifiable Code Generation Zhe Ye Zhengxu Yan Jingxuan He Timothe Kasriel Kaiyu Yang Dawn Song 29 0 0 29 May 2025
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation Nikita Khramov Andrei Kozyrev Gleb Solovev Anton Podkopaev 66 0 0 28 May 2025
A cross-regional review of AI safety regulations in the commercial aviation Penny A. Barr Sohel M. Imroz 108 0 0 12 Feb 2025
Assured Automatic Programming via Large Language Models Martin Mirchev Andreea Costea Abhishek Kr Singh Abhik Roychoudhury 87 1 0 24 Oct 2024
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning Alex Sanchez-Stern Abhishek Varghese Zhanna Kaufman Dylan Zhang Talia Ringer Yuriy Brun 133 2 0 17 Aug 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 116 91 0 23 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 86 16 0 03 May 2024
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving Chenyang An Zhibo Chen Qihao Ye Emily First Letian Peng Jiayun Zhang Zihan Wang Sorin Lerner Jingbo Shang LRM 161 8 0 10 Apr 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 142 813 0 25 Jan 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts Lasse Blaauwbroek Miroslav Olšák Jason Rute F. I. S. Massolo Jelle Piepenbrock Vasily Pestun 94 11 0 05 Jan 2024
Llemma: An Open Language Model For Mathematics Zhangir Azerbayev Hailey Schoelkopf Keiran Paster Marco Dos Santos Stephen Marcus McAleer Albert Q. Jiang Jia Deng Stella Biderman Sean Welleck CLL 128 303 0 16 Oct 2023
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Madeline Endres Sarah Fakhoury Saikat Chakraborty Shuvendu K. Lahiri 80 26 0 03 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 127 74 0 01 Oct 2023
RAP-Gen: Retrieval-Augmented Patch Generation with CodeT5 for Automatic Program Repair Weishi Wang Yue Wang Shafiq Joty Steven C. H. Hoi 76 68 0 12 Sep 2023
Benchmarking Large Language Models in Retrieval-Augmented Generation Jiawei Chen Hongyu Lin Xianpei Han Le Sun 3DV RALM 121 312 0 04 Sep 2023
EditSum: A Retrieve-and-Edit Framework for Source Code Summarization Jia Li Yongming Li Ge Li Xing Hu Xin Xia Zhi Jin 116 68 0 26 Aug 2023
Llama 2: Open Foundation and Fine-Tuned Chat Models Hugo Touvron Louis Martin Kevin R. Stone Peter Albert Amjad Almahairi ... Sharan Narang Aurelien Rodriguez Robert Stojnic Sergey Edunov Thomas Scialom AI4MH ALM 548 12,137 0 18 Jul 2023
GPT-4 Technical Report OpenAI OpenAI OpenAI Josh Achiam Steven Adler Sandhini Agarwal Lama Ahmad ... Shengjia Zhao Tianhao Zheng Juntang Zhuang William Zhuk Barret Zoph LLMAG MLLM 1.6K 14,869 0 15 Mar 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 141 107 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 157 181 0 21 Oct 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 293 178 0 25 May 2022
HyperTree Proof Search for Neural Theorem Proving Guillaume Lample Marie-Anne Lachaux Thibaut Lavril Xavier Martinet Amaury Hayat Gabriel Ebner Aurelien Rodriguez Timothée Lacroix AIMat 98 151 0 23 May 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 94 103 0 22 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 156 127 0 03 Feb 2022
Retrieval Augmented Code Generation and Summarization Md. Rizwan Parvez W. Ahmad Saikat Chakraborty Baishakhi Ray Kai-Wei Chang 70 192 0 26 Aug 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 801 10,658 0 17 Jun 2021
A Syntax-Guided Edit Decoder for Neural Program Repair Qihao Zhu Zeyu Sun Yuan-an Xiao Wenjie Zhang Kang Yuan Y. Xiong Lu Zhang KELM 119 227 0 15 Jun 2021
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning Minchao Wu Michael Norrish Christian J. Walder Amir Dezfouli 61 42 0 19 Feb 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 117 127 0 11 Feb 2021
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq Lasse Blaauwbroek Josef Urban H. Geuvers 62 24 0 31 Jul 2020
Dense Passage Retrieval for Open-Domain Question Answering Vladimir Karpukhin Barlas Oğuz Sewon Min Patrick Lewis Ledell Yu Wu Sergey Edunov Danqi Chen Wen-tau Yih RALM 251 3,816 0 10 Apr 2020
CodeBERT: A Pre-Trained Model for Programming and Natural Languages Zhangyin Feng Daya Guo Duyu Tang Nan Duan Xiaocheng Feng ... Linjun Shou Bing Qin Ting Liu Daxin Jiang Ming Zhou 230 2,727 0 19 Feb 2020
Learning to Reason in Large Theories without Imitation Kshitij Bansal Christian Szegedy M. Rabe Sarah M. Loos Viktor Toman NAI LRM 107 42 0 25 May 2019
Graph Representations for Higher-Order Logic and Theorem Proving Aditya Sanjay Paliwal Sarah M. Loos M. Rabe Kshitij Bansal Christian Szegedy AI4CE NoLa 206 98 0 24 May 2019
Learning to Prove Theorems via Interacting with Proof Assistants Kaiyu Yang Jia Deng AIMat LRM 114 147 0 21 May 2019
GamePad: A Learning Environment for Theorem Proving Daniel Huang Prafulla Dhariwal Basel Alomair Ilya Sutskever 103 111 0 02 Jun 2018
Learning to Reason with HOL4 tactics Thibault Gauthier C. Kaliszyk Josef Urban 94 77 0 02 Apr 2018
Fairness Testing: Testing Software for Discrimination Sainyam Galhotra Yuriy Brun A. Meliou 87 383 0 11 Sep 2017