Can Large Language Models Reason about Program Invariants?

Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, Pengcheng Yin
Proceedings of the 40th International Conference on Machine Learning, PMLR 202:27496-27520, 2023.

Abstract

Identifying invariants is an important program analysis task with applications towards program understanding, bug finding, vulnerability analysis, and formal verification. Existing tools for identifying program invariants rely on dynamic analysis, requiring traces collected from multiple executions in order to produce reliable invariants. We study the application of large language models to invariant prediction, finding that models trained on source code and fine-tuned for invariant generation can perform invariant prediction as static rather than dynamic analysis. Using a scratchpad approach where invariants are predicted sequentially through a program gives the best performance, finding invariants statically of quality comparable to those obtained by a dynamic analysis tool with access to five program traces.

Cite this Paper

BibTeX
@InProceedings{pmlr-v202-pei23a, title = {Can Large Language Models Reason about Program Invariants?}, author = {Pei, Kexin and Bieber, David and Shi, Kensen and Sutton, Charles and Yin, Pengcheng}, booktitle = {Proceedings of the 40th International Conference on Machine Learning}, pages = {27496--27520}, year = {2023}, editor = {Krause, Andreas and Brunskill, Emma and Cho, Kyunghyun and Engelhardt, Barbara and Sabato, Sivan and Scarlett, Jonathan}, volume = {202}, series = {Proceedings of Machine Learning Research}, month = {23--29 Jul}, publisher = {PMLR}, pdf = {https://proceedings.mlr.press/v202/pei23a/pei23a.pdf}, url = {https://proceedings.mlr.press/v202/pei23a.html}, abstract = {Identifying invariants is an important program analysis task with applications towards program understanding, bug finding, vulnerability analysis, and formal verification. Existing tools for identifying program invariants rely on dynamic analysis, requiring traces collected from multiple executions in order to produce reliable invariants. We study the application of large language models to invariant prediction, finding that models trained on source code and fine-tuned for invariant generation can perform invariant prediction as static rather than dynamic analysis. Using a scratchpad approach where invariants are predicted sequentially through a program gives the best performance, finding invariants statically of quality comparable to those obtained by a dynamic analysis tool with access to five program traces.} }
Endnote
%0 Conference Paper %T Can Large Language Models Reason about Program Invariants? %A Kexin Pei %A David Bieber %A Kensen Shi %A Charles Sutton %A Pengcheng Yin %B Proceedings of the 40th International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2023 %E Andreas Krause %E Emma Brunskill %E Kyunghyun Cho %E Barbara Engelhardt %E Sivan Sabato %E Jonathan Scarlett %F pmlr-v202-pei23a %I PMLR %P 27496--27520 %U https://proceedings.mlr.press/v202/pei23a.html %V 202 %X Identifying invariants is an important program analysis task with applications towards program understanding, bug finding, vulnerability analysis, and formal verification. Existing tools for identifying program invariants rely on dynamic analysis, requiring traces collected from multiple executions in order to produce reliable invariants. We study the application of large language models to invariant prediction, finding that models trained on source code and fine-tuned for invariant generation can perform invariant prediction as static rather than dynamic analysis. Using a scratchpad approach where invariants are predicted sequentially through a program gives the best performance, finding invariants statically of quality comparable to those obtained by a dynamic analysis tool with access to five program traces.
APA
Pei, K., Bieber, D., Shi, K., Sutton, C. & Yin, P.. (2023). Can Large Language Models Reason about Program Invariants?. Proceedings of the 40th International Conference on Machine Learning, in Proceedings of Machine Learning Research 202:27496-27520 Available from https://proceedings.mlr.press/v202/pei23a.html.

Related Material