-
Finding Inductive Loop Invariants using Large Language Models
Authors:
Adharsh Kamath,
Aditya Senthilnathan,
Saikat Chakraborty,
Pantazis Deligiannis,
Shuvendu K. Lahiri,
Akash Lal,
Aseem Rastogi,
Subhajit Roy,
Rahul Sharma
Abstract:
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting t…
▽ More
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification.
△ Less
Submitted 14 November, 2023;
originally announced November 2023.
-
Ranking LLM-Generated Loop Invariants for Program Verification
Authors:
Saikat Chakraborty,
Shuvendu K. Lahiri,
Sarah Fakhoury,
Madanlal Musuvathi,
Akash Lal,
Aseem Rastogi,
Aditya Senthilnathan,
Rahul Sharma,
Nikhil Swamy
Abstract:
Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an…
▽ More
Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}.
△ Less
Submitted 12 February, 2024; v1 submitted 13 October, 2023;
originally announced October 2023.
-
Fission-fusion dynamics and group-size dependent composition in heterogeneous populations
Authors:
Gokul G. Nair,
Athmanathan Senthilnathan,
Srikanth K. Iyer,
Vishwesha Guttal
Abstract:
Many animal groups are heterogeneous and may even consist of individuals of different species, called mixed-species flocks. Mathematical and computational models of collective animal movement behaviour, however, typically assume that groups and populations consist of identical individuals. In this paper, using the mathematical framework of the coagulation-fragmentation process, we develop and anal…
▽ More
Many animal groups are heterogeneous and may even consist of individuals of different species, called mixed-species flocks. Mathematical and computational models of collective animal movement behaviour, however, typically assume that groups and populations consist of identical individuals. In this paper, using the mathematical framework of the coagulation-fragmentation process, we develop and analyse a model of merge and split group dynamics, also called fission-fusion dynamics, for heterogeneous populations that contain two types (or species) of individuals. We assume that more heterogeneous groups experience higher split rates than homogeneous groups, forming two daughter groups whose compositions are drawn uniformly from all possible partitions. We analytically derive a master equation for group size and compositions and find mean-field steady-state solutions. We predict that there is a critical group size below which groups are more likely to be homogeneous and contain the abundant type/species. Despite the propensity of heterogeneous groups to split at higher rates, we find that groups are more likely to be heterogeneous but only above the critical group size. Monte-Carlo simulation of the model show excellent agreement with these analytical model results. Thus, our model makes a testable prediction that composition of flocks are group-size dependent and do not merely reflect the population level heterogeneity. We discuss the implications of our results to empirical studies on flocking systems.
△ Less
Submitted 18 March, 2019; v1 submitted 18 November, 2017;
originally announced November 2017.
