Gowtham Kaki

Richard Roberson, Gowtham Kaki, Ashutosh Trivedi

This study investigates various approaches to using Large Language Models (LLMs) for Text-to-SQL program synthesis, focusing on the outcomes and insights derived. Employing the popular Text-to-SQL dataset, spider, the goal was to input a natural language question along with the database schema and output the correct SQL SELECT query. The initial approach was to fine-tune a local and open-source model to generate the SELECT query. After QLoRa fine-tuning WizardLM's WizardCoder-15B model on the spider dataset, the execution accuracy for generated queries rose to a high of 61%. With the second approach, using the fine-tuned gpt-3.5-turbo-16k (Few-shot) + gpt-4-turbo (Zero-shot error correction), the execution accuracy reached a high of 82.1%. Of all the incorrect queries, most can be categorized into a seven different categories of what went wrong: selecting the wrong columns or wrong order of columns, grouping by the wrong column, predicting the wrong values in conditionals, using different aggregates than the ground truth, extra or too few JOIN clauses, inconsistencies in the Spider dataset, and lastly completely incorrect query structure. Most if not all of the queries fall into these categories and it is insightful to understanding where the faults still lie with LLM program synthesis and where they can be improved.

Christian Fontenot, Gowtham Kaki, Bor-Yuh Evan Chang

We consider the problem of automatically proving safety properties of distributed protocols. Distributed protocols have been particularly challenging for automated verification due to their asynchronous and parametric nature. Compared to synchronous systems, asynchronous communication leads to a combinatorial explosion of possible execution histories of message handlers. And because distributed protocols are typically defined parametrically on the number of actors, these definitions lead to an unbounded number of possible execution histories of unbounded length. Existing verification techniques for such distributed protocols typically require global invariants about the entire actor system, which are complex even for simple protocols. In this paper, we present an automated verification technique based on proving unreachability backwards from error states in an actor system. One key insight is that the unboundedness from parametricity can be further classified into \emph{affine} and non-affine protocols, where affine protocols have execution histories of unbounded length in a bounded number of communication rounds. We show how to use novel, goal-directed notions of materialization, causality, and summarization to verify safety properties of affine protocols with an unbounded number of actors in an automated manner. Using our prototype verification tool DissProve, we provide evidence for the feasibility of automated safety verification of asynchronous parametrized systems with affine communication.