Meghana Sistla, Gogul Balakrishnan, Pat Rondon, José P. Cambronero, Michele Tufano, and Satish Chandra
(University of Texas at Austin, USA; Google DeepMind, USA; Google, USA; Meta Platforms, USA)
While LLM-based agents are able to tackle a wide variety of code reasoning questions, the answers are not always correct. As a result of this lack of trustworthiness, the agent's answers need to be manually verified before they can be trusted, which requires substantial effort and can result in lower developer productivity. We describe a method to automatically validate the answers provided by a code reasoning agent by extracting a formal representation of the agent's response, and using formal verification and program analysis tools to verify the reasoning steps. We applied this approach to a set of 20 program equivalence queries and found that the formal verification step successfully caught 6/8 incorrect agent judgments. This work lays the foundation for what may become a new class of high-precision, verifiable code agents, paving the way for their reliable use in critical software engineering workflows.
Article Search
Article: pldiws26pagemain-p4-p