一句话：提出基于路径分解的 LLM 符号执行方法，用代码表示泛化路径约束让 LLM 直接推理，并实现轻量、语言无关的 AutoBug 引擎。
该文针对 LLM 直接用于程序分析时固有的近似性所带来的准确性与规模瓶颈展开研究：此类问题通常需要更大规模的模型与更高 token 上限，进而依赖企业级 GPU，限制了可用性。作者提出基于 LLM 的符号执行，其核心是按路径对程序分析任务进行分解，把整体分析拆成更小、更易处理的子任务；同时用一个通用的、基于代码的表示来泛化路径约束，使 LLM 可以直接在该表示上推理，而无需将其翻译为表达力更弱的形式语言。作者以 AutoBug 的形式实现了该思路，这是一个轻量且语言无关的 LLM 符号执行引擎，可分析传统方法难以处理的代码。实验表明，AutoBug 能同时提升基于 LLM 的程序分析的准确性与规模，尤其适用于可在消费级硬件上运行的小型 LLM。
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.
@article{paperbot3023,
title = {Large Language Model Powered Symbolic Execution},
author = {Yihe Li and Ruijie Meng and Gregory J. Duck},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763163}
}