25 citations · 37 across the 8 of their papers we have counts for
8 papers
Lemmanaid: Neuro-Symbolic Lemma Conjecturing
Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry +4
Mathematicians and computer scientists are increasingly leveraging proof assistants to formalize and check complex proofs, a task that demands substantial expertise. Can we lower t…
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
Kyle Thompson, Nuno Saavedra, Pedro Carrott +6
Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual…
Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun +3
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can auto…
CoqPyt: Proof Navigation in Python in the Era of LLMs
Pedro Carrott, Nuno Saavedra, Kyle Thompson +3
Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most…
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
Chenyang An, Zhibo Chen, Qihao Ye +6
Recent advances in Automated Theorem Proving have shown the effectiveness of leveraging a (large) language model that generates tactics (i.e. proof steps) to search through proof s…
Getting More out of Large Language Models for Proofs
Shizhuo Dylan Zhang, Talia Ringer, Emily First
Large language models have the potential to simplify formal theorem proving and make it more accessible. But how to get the most out of these models is still an open question. To a…
Baldur: Whole-Proof Generation and Repair with Large Language Models
Emily First, Markus N. Rabe, Talia Ringer +1
Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, suc…
Passport: Improving Automated Formal Verification Using Identifiers
Alex Sanchez-Stern, Emily First, Timothy Zhou +3
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive.…