A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912554845995008 |
|---|---|
| author | Bayazıt, Barış Li, Yao Si, Xujie |
| author_facet | Bayazıt, Barış Li, Yao Si, Xujie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_18587 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants Bayazıt, Barış Li, Yao Si, Xujie Programming Languages Artificial Intelligence 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. |
| title | A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants |
| topic | Programming Languages Artificial Intelligence |
| url | https://arxiv.org/abs/2508.18587 |