一句话：提出用 LLM 增强静态分析，通过神经-符号混合框架提升缺陷检测的精度与可扩展性。
静态程序分析在软件工程与安全中至关重要，但实用工具长期面临精度与可扩展性之间的权衡。大语言模型（LLM）为程序推理带来新机遇，然而其与形式化分析的整合仍鲜有探索。本提案研究如何用 LLM 增强静态分析，以提升缺陷与漏洞检测的实用性和精度。已完成的两项研究 LLift（OOPSLA'24）和 BugLens（ASE'25）表明，结构化的 LLM 推理能显著降低误报，并在 Linux 内核中发现真实缺陷。在此基础上，正在进行的工作旨在设计混合框架，使 LLM 与静态分析器能够原则性地协作，并刻画基于 LLM 推理的理论极限。最终目标是推动神经-符号程序分析走向实用且可信的软件推理。
Static program analysis plays a fundamental role in software engineering and security, yet practical tools continue to struggle with the long-standing trade-off between precision and scalability. Recent progress in large language models (LLMs) offers new opportunities to enhance program reasoning, but their integration with formal analysis remains largely unexplored. This proposal investigates how LLMs can augment static analysis to improve the practicality and precision of bug and vulnerability detection. Two completed studies, LLift (OOPSLA’24) and BugLens (ASE’25), demonstrate that structured LLM reasoning can significantly reduce false positives and uncover real bugs in the Linux kernel. Building on these results, the ongoing research seeks to design hybrid frameworks that enable principled collaboration between LLMs and static analyzers, and to characterize the theoretical limits of LLM-based reasoning. Ultimately, this work aims to advance neuro-symbolic program analysis toward practical and trustworthy software reasoning.