一句话：将 Datalog 分析概率化，用神经网络把变量名等非形式信息编码为软证据，以改进报警排序。
传统 Datalog 程序分析只利用形式化的规则与事实，忽略变量名、字符串常量等非形式信息，导致报警排序不理想。本文提出一种神经符号式程序分析：将 Datalog 分析转换为概率分析，为规则附加概率；再用神经网络依据非形式信息判断某个分析事实成立的可能性，并将其编码为概率分析中的软证据，即该事实的“噪声传感器”。由此分析输出按概率排序的报警。作者在八个 Java 基准上改进基于变量名的指针分析，在八个 Android 应用上改进考虑组件间通信的污点分析：真报警与假报警的逆序数、真报警平均排名与中位排名分别平均改善 55.4%、44.9%、58%（指针分析）和 67.2%、44.7%、37.6%（污点分析）。此外，他们利用 C 程序执行的动态信息改进污点分析与区间分析，说明了软证据机制的通用性。
We propose a neural-symbolic style of program analysis that systematically incorporates informal information in a Datalog program analysis. The analysis is converted into a probabilistic analysis by attaching probabilities to its rules. And its output becomes a ranking of possible alarms based on their probabilities. We apply a neural network to judge how likely an analysis fact holds based on informal information such as variable names and String constants. This information is encoded as a soft evidence in the probabilistic analysis, which is a “noisy sensor” of the fact. With this information, the probabilistic analysis produces a better ranking of the alarms. We have demonstrated the effectiveness of our approach by improving a pointer analysis based on variable names on eight Java benchmarks, and a taint analysis that considers inter-component communication on eight Android applications. On average, our approach has improved the inversion count between true alarms and false alarms, mean rank of true alarms, and median rank of true alarms by 55.4%, 44.9%, and 58% on the pointer analysis, and 67.2%, 44.7%, and 37.6% on the taint analysis respectively. We also demonstrated the generality of our soft evidence mechanism by improving a taint analysis and an interval analysis for C programs using dynamic information from program executions.
@article{paperbot3166,
title = {Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences},
author = {Tianchi Li and Xin Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720508}
}