A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this paper, we perform a case study based on two mature Rocq projects: the hs-to-coq tool and Verdi. We evaluate the effectiveness of LLMs in generating proofs by both quantitative and qualitative analysis. Our study finds that: (1) external dependencies and context in the same source file can significantly help proof generation; (2) LLMs perform great on small proofs but can also generate large proofs; (3) LLMs perform differently on different verification projects; and (4) LLMs can generate concise and smart proofs, apply classical techniques to new definitions, but can also make odd mistakes.
Wed 15 OctDisplayed time zone: Perth change
16:00 - 17:40 | LLMs for Program Analysis and Verification IILMPL at Orchid East Chair(s): Zhuo Zhang Columbia University | ||
16:00 15mTalk | Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis LMPL | ||
16:15 20mTalk | Toward Repository-Level Program Verification with Large Language Models LMPL DOI Pre-print | ||
16:35 15mTalk | Preguss: It Analyzes, It Specifies, It Verifies LMPL Zhongyi Wang Zhejiang University, China, Tengjie Lin Zhejiang University, Mingshuai Chen Zhejiang University, Mingqi Yang Zhejiang University, Haokun Li Peking University, Xiao Yi The Chinese University of Hong Kong, Shengchao Qin Xidian University, Jianwei Yin Zhejiang University | ||
16:50 20mTalk | A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants LMPL Barış Bayazıt University of Toronto, Yao Li Portland State University, Xujie Si University of Toronto DOI Pre-print | ||
17:10 20mTalk | Understanding Formal Reasoning Failures in LLMs as Abstract Interpretersremote LMPL Jacqueline Mitchell University of Southern California, Brian Hyeongseok Kim University of Southern California, Chenyu Zhou University of Southern California, Chao Wang University of Southern California | ||