ResearchTrend.AI
  • Papers
  • Communities
  • Events
  • Blog
  • Pricing
Papers
Communities
Social Events
Terms and Conditions
Pricing
Parameter LabParameter LabTwitterGitHubLinkedInBlueskyYoutube

© 2025 ResearchTrend.AI, All rights reserved.

  1. Home
  2. Papers
  3. 2412.14063
  4. Cited By
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
v1v2v3 (latest)

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

18 December 2024
Kyle Thompson
Nuno Saavedra
Pedro Carrott
Kevin Fisher
Alex Sanchez-Stern
Yuriy Brun
J. Ferreira
Sorin Lerner
E. First
    LRM
ArXiv (abs)PDFHTML

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

38 / 38 papers shown
Title
VERINA: Benchmarking Verifiable Code Generation
VERINA: Benchmarking Verifiable Code Generation
Zhe Ye
Zhengxu Yan
Jingxuan He
Timothe Kasriel
Kaiyu Yang
Dawn Song
31
0
0
29 May 2025
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
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
Assured Automatic Programming via Large Language Models
Martin Mirchev
Andreea Costea
Abhishek Kr Singh
Abhik Roychoudhury
90
1
0
24 Oct 2024
QEDCartographer: Automating Formal Verification Using Reward-Free
  Reinforcement Learning
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Alex Sanchez-Stern
Abhishek Varghese
Zhanna Kaufman
Dylan Zhang
Talia Ringer
Yuriy Brun
137
2
0
17 Aug 2024
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale
  Synthetic Data
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
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty
Gabriel Ebner
Siddharth Bhat
Sarah Fakhoury
Sakina Fatima
Shuvendu K. Lahiri
Nikhil Swamy
88
16
0
03 May 2024
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for
  Intuitionistic Propositional Logic Proving
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
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
149
813
0
25 Jan 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts
Graph2Tac: Online Representation Learning of Formal Math Concepts
Lasse Blaauwbroek
Miroslav Olšák
Jason Rute
F. I. S. Massolo
Jelle Piepenbrock
Vasily Pestun
96
11
0
05 Jan 2024
Llemma: An Open Language Model For Mathematics
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
130
303
0
16 Oct 2023
Can Large Language Models Transform Natural Language Intent into Formal
  Method Postconditions?
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
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
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
Benchmarking Large Language Models in Retrieval-Augmented Generation
Jiawei Chen
Hongyu Lin
Xianpei Han
Le Sun
3DVRALM
126
312
0
04 Sep 2023
EditSum: A Retrieve-and-Edit Framework for Source Code Summarization
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
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
AI4MHALM
574
12,138
0
18 Jul 2023
GPT-4 Technical Report
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
LLMAGMLLM
1.7K
14,870
0
15 Mar 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models
Baldur: Whole-Proof Generation and Repair with Large Language Models
E. First
M. Rabe
Talia Ringer
Yuriy Brun
144
107
0
08 Mar 2023
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
  Proofs
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
160
181
0
21 Oct 2022
Autoformalization with Large Language Models
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
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
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
AIMatLRM
94
103
0
22 May 2022
Formal Mathematics Statement Curriculum Learning
Formal Mathematics Statement Curriculum Learning
Stanislas Polu
Jesse Michael Han
Kunhao Zheng
Mantas Baksys
Igor Babuschkin
Ilya Sutskever
AIMat
158
127
0
03 Feb 2022
Retrieval Augmented Code Generation and Summarization
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
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
OffRLAI4TSAI4CEALMAIMat
846
10,659
0
17 Jun 2021
A Syntax-Guided Edit Decoder for Neural Program Repair
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
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Minchao Wu
Michael Norrish
Christian J. Walder
Amir Dezfouli
73
42
0
19 Feb 2021
Proof Artifact Co-training for Theorem Proving with Language Models
Proof Artifact Co-training for Theorem Proving with Language Models
Jesse Michael Han
Jason M. Rute
Yuhuai Wu
Edward W. Ayers
Stanislas Polu
AIMat
119
127
0
11 Feb 2021
The Tactician (extended version): A Seamless, Interactive Tactic Learner
  and Prover for Coq
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
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
256
3,816
0
10 Apr 2020
CodeBERT: A Pre-Trained Model for Programming and Natural Languages
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
240
2,727
0
19 Feb 2020
Learning to Reason in Large Theories without Imitation
Learning to Reason in Large Theories without Imitation
Kshitij Bansal
Christian Szegedy
M. Rabe
Sarah M. Loos
Viktor Toman
NAILRM
118
42
0
25 May 2019
Graph Representations for Higher-Order Logic and Theorem Proving
Graph Representations for Higher-Order Logic and Theorem Proving
Aditya Sanjay Paliwal
Sarah M. Loos
M. Rabe
Kshitij Bansal
Christian Szegedy
AI4CENoLa
206
98
0
24 May 2019
Learning to Prove Theorems via Interacting with Proof Assistants
Learning to Prove Theorems via Interacting with Proof Assistants
Kaiyu Yang
Jia Deng
AIMatLRM
127
147
0
21 May 2019
GamePad: A Learning Environment for Theorem Proving
GamePad: A Learning Environment for Theorem Proving
Daniel Huang
Prafulla Dhariwal
Basel Alomair
Ilya Sutskever
110
111
0
02 Jun 2018
Learning to Reason with HOL4 tactics
Learning to Reason with HOL4 tactics
Thibault Gauthier
C. Kaliszyk
Josef Urban
94
77
0
02 Apr 2018
Fairness Testing: Testing Software for Discrimination
Fairness Testing: Testing Software for Discrimination
Sainyam Galhotra
Yuriy Brun
A. Meliou
89
383
0
11 Sep 2017
1