代理解释：基于 LLM 的程序分析的格结构证据

大语言模型 可以查阅固定静态分析器无法查阅的信息，例如文档、当前安全建议、特定于版本的元数据和非正式 API 合同。这使得 LLM 成为程序分析的一个引人注目的选择，这些程序分析依赖于源程序之外的信息，或者不适合传统静态分析器。然而，直接要求 LLM 进行一次性整个程序分析是很脆弱的，因为它将许多依赖证据的判断压缩成一个不透明的答案，而不是暴露哪些结论得到支持或有争议，并使用中间结果来指导以后更有针对性的搜索。在本文中，我们提出了代理解释，这是一个将基于格的静态分析规则引入到 LLM 驱动的程序推理中的框架。在高层次上，代理解释将高层次分析目标分解为局部声明，并跟踪 LLM 对有限高度格中每个声明的判断。工作列表算法控制着分析过程中索赔及其判断的演变。我们引入了代理解释的正式模型，探索了它打开的设计空间，并通过一个分析依赖于不透明第三方组件的代码的示例来说明该方法。