Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911184519692288 |
|---|---|
| author | Mitchell, Jacqueline L. Kim, Brian Hyeongseok Zhou, Chenyu Wang, Chao |
| author_facet | Mitchell, Jacqueline L. Kim, Brian Hyeongseok Zhou, Chenyu Wang, Chao |
| contents | Large language models (LLMs) are increasingly used for program verification, and yet little is known about \emph{how} they reason about program semantics during this process. In this work, we focus on abstract interpretation based-reasoning for invariant generation and introduce two novel prompting strategies that aim to elicit such reasoning from LLMs. We evaluate these strategies across several state-of-the-art LLMs on 22 programs from the SV-COMP benchmark suite widely used in software verification. We analyze both the soundness of the generated invariants and the key thematic patterns in the models' reasoning errors. This work aims to highlight new research opportunities at the intersection of LLMs and program verification for applying LLMs to verification tasks and advancing their reasoning capabilities in this application. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_12686 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters Mitchell, Jacqueline L. Kim, Brian Hyeongseok Zhou, Chenyu Wang, Chao Machine Learning Programming Languages Software Engineering Large language models (LLMs) are increasingly used for program verification, and yet little is known about \emph{how} they reason about program semantics during this process. In this work, we focus on abstract interpretation based-reasoning for invariant generation and introduce two novel prompting strategies that aim to elicit such reasoning from LLMs. We evaluate these strategies across several state-of-the-art LLMs on 22 programs from the SV-COMP benchmark suite widely used in software verification. We analyze both the soundness of the generated invariants and the key thematic patterns in the models' reasoning errors. This work aims to highlight new research opportunities at the intersection of LLMs and program verification for applying LLMs to verification tasks and advancing their reasoning capabilities in this application. |
| title | Understanding Formal Reasoning Failures in LLMs as Abstract Interpreters |
| topic | Machine Learning Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2503.12686 |