AutoCodeSherpa: Symbolic Explanations in AI Coding Agents

Large Language Model (LLM) agents autonomously use external tools on top of one or more LLMs to accomplish specific tasks. Lately LLM agents for software engineering tasks have become popular. These agents can benefit from the use of program analysis tools working on program representations. This is demonstrated by existing agentic AI solutions such as AutoCodeRover or SpecRover which perform automated program repair. Specifically the goal of these works is to use program analysis to improve the patch quality. These agents are currently being used to automatically fix static analysis issues from the widely used SonarQube static analyzer. Nevertheless, for the agents to be deployed in a production environment, agents need to suggest software artifacts, such as patches, with evidence and with high confidence. In this work, we provide a workflow where an agent provides explanations of the bug in the form of symbolic formulae. The explanations are in the form of input conditions, infection conditions and output conditions, implemented as property based tests (PBT) and program-internal symbolic expressions. These can help in human developer cognition of the agent outputs as well as in achieving completely automated agentic workflows for software. The human developer can benefit from the input condition, represented as a PBT, to generate various concrete inputs showing a given issue. Furthermore, since the PBTs are executable, our explanations are executable as well. We can thus also use the explanations in a completely automated issue resolution environment for accepting or rejecting the patches that are suggested by patching agents such as AutoCodeRover. Finally, as agentic AI approaches continue to develop, the program analysis driven explanations can be provided to other LLM-based repair techniques such as Agentless to improve their output.