4 papers
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…
Stop treating `AGI' as the north-star goal of AI research
Borhane Blili-Hamelin, Christopher Graziul, Leif Hancox-Li +13
The AI research community plays a vital role in shaping the scientific, engineering, and societal goals of AI research. In this position paper, we argue that focusing on the highly…
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
Jilin Hu, Jianyu Zhang, Yongwang Zhao +1
Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs…
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman +3
Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recen…