Large Language Model Powered Symbolic Execution

TL;DR

This paper introduces AutoBug, an LLM-based symbolic execution engine that decomposes program analysis into smaller tasks, improving accuracy and scalability of code analysis on accessible hardware.

Contribution

It proposes a novel path-based decomposition method for LLM symbolic execution, enabling effective analysis with smaller, more accessible models.

Findings

AutoBug improves analysis accuracy over traditional LLM methods.

The approach enables scalable analysis on consumer-grade hardware.

AutoBug is language-agnostic and practical for challenging code analysis.

Abstract

Large Language Models (LLMs) have emerged as a promising alternative to traditional static program analysis methods, such as symbolic execution, offering the ability to reason over code directly without relying on theorem provers or SMT solvers. However, LLMs are also inherently approximate by nature, and therefore face significant challenges in relation to the accuracy and scale of analysis in real-world applications. Such issues often necessitate the use of larger LLMs with higher token limits, but this requires enterprise-grade hardware (GPUs) and thus limits accessibility for many users. In this paper, we propose LLM-based symbolic execution -- a novel approach that enhances LLM inference via a path-based decomposition of the program analysis tasks into smaller (more tractable) subtasks. The core idea is to generalize path constraints using a generic code-based representation that the LLM can directly reason over, and without translation into another (less-expressive) formal language. We implement our approach in the form of AutoBug, an LLM-based symbolic execution engine that is lightweight and language-agnostic, making it a practical tool for analyzing code that is challenging for traditional approaches. We show that AutoBug can improve both the accuracy and scale of LLM-based program analysis, especially for smaller LLMs that can run on consumer-grade hardware.