Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

3 May 2024

Saikat Chakraborty

Shuvendu K. Lahiri

Papers citing "Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming"

14 / 14 papers shown

Title
Can LLMs Enable Verification in Mainstream Programming? Aleksandr Shefer Igor Engel Stanislav Alekseev Daniil Berezun Ekaterina Verbitskaia Anton Podkopaev 58 0 0 18 Mar 2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity Dylan Zhang Justin Wang Tianran Sun 36 0 0 17 Feb 2025
RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation Sicheng Zhong Jiading Zhu Yifang Tian Xujie Si 49 0 0 07 Feb 2025
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 98 1 0 18 Dec 2024
Cobblestone: Iterative Automation for Formal Verification Saketh Ram Kasibatla Arpan Agarwal Yuriy Brun Sorin Lerner Talia Ringer Emily First 23 0 0 25 Oct 2024
Automated Proof Generation for Rust Code via Self-Evolution Tianyu Chen Shuai Lu Shan Lu Y. Gong Chenyuan Yang ... Peng Cheng Fan Yang Shuvendu Lahiri Tao Xie Lidong Zhou 37 6 0 21 Oct 2024
AutoVerus: Automated Proof Generation for Rust Code Chenyuan Yang Xuheng Li Md Rakib Hossain Misu Jianan Yao Weidong Cui ... Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou Shan Lu 27 7 0 19 Sep 2024
Statically Contextualizing Large Language Models with Typed Holes Andrew Blinn Xiang Li June Hyung Kim Cyrus Omar 25 1 0 02 Sep 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 42 21 0 15 Apr 2024
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 39 61 0 01 Oct 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 53 90 0 08 Mar 2023
Magnushammer: A Transformer-Based Approach to Premise Selection Maciej Mikuła Szymon Tworkowski Szymon Antoniak Bartosz Piotrowski Albert Qiaochu Jiang Jinyi Zhou Christian Szegedy Lukasz Kuciñski Piotr Milo's Yuhuai Wu 37 41 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 58 154 0 21 Oct 2022
Text and Code Embeddings by Contrastive Pre-Training Arvind Neelakantan Tao Xu Raul Puri Alec Radford Jesse Michael Han ... Tabarak Khan Toki Sherbakov Joanne Jang Peter Welinder Lilian Weng SSL AI4TS 201 412 0 24 Jan 2022