A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

TL;DR

This case study evaluates the effectiveness of large language models in automating proofs within proof assistants, revealing their strengths and limitations across different verification projects and proof sizes.

Contribution

It provides a comprehensive analysis of LLMs in proof generation, highlighting factors that influence their performance and showcasing their capabilities and errors in verification tasks.

Findings

LLMs benefit from external dependencies and context.

They perform well on small proofs and can handle large proofs.

Performance varies across different verification projects.

Abstract

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.