本文提出 NeuroLog，一个端到端、无需构建环境的漏洞发现流水线，用于 C/C++ 源代码。核心思路是将 LLM、Datalog（Soufflé）和 SMT 求解器（Z3）分层协作：LLM 逐个函数提取类型化的数据流事实；Soufflé 规则网将这些事实组合成跨函数的发现；Z3 后处理过滤不可行路径并为每个幸存路径输出 SAT 模型。为超越纯静态分析，还引入运行时证据：从少量语料种子导出的可能范围不变量以极低成本收紧 SMT 问题。第二个 LLM 智能体读取每个 SAT 模型并编写 Python 程序生成候选崩溃输入，由 AddressSanitizer 验证。实验覆盖 stb、cJSON、libxml2、FFmpeg demuxer 切片和 curl 8.3.0，重新发现了 8 个 CVE 类问题，包括 CVSS 9.8 的 SOCKS5 堆溢出 CVE-2023-38545。在 libarchive HEAD 上发现 5 个内存安全漏洞（4 个先前未报告），其中 cpio use-after-free 在 7 小时内得到确认。提取阶段约 37 秒、成本 $0.005（stb）；崩溃合成将静态发现转化为 102 字节的 stb_vorbis 崩溃（两轮 LLM 交互）。来自三个 Matroska 种子的似然不变性过滤器消除了 FFmpeg demuxer 可行集中的 13.2%。该方法结合了静态缩小 SMT（Saturn, Pinpoint）和 Datalog 与 SMT（Formulog）的先前工作，新贡献在于 LLM 推导的事实库、无构建流水线以及将 SAT 模型作为合成崩溃输入的制品而非简单的是/否判定。适合安全研究人员、漏洞发现工程师和软件质量保障团队阅读。

这篇论文针对高级持续性威胁（APT）场景下的攻击溯源重建问题，提出了一种神经符号框架 HunterAgent。现代安全运营中心（SOC）虽能通过告警筛选减少误报，但面对使用反取证技术（如父进程PID欺骗、日志擦除、无文件执行）的APT攻击时，现有基于溯源图的方法因日志部分损坏或反取证操作导致图分裂为不连通子图，无法重建完整攻击链。此外，无约束的大语言模型（LLM）虽能生成流畅叙事，但会虚构不符合操作系统物理规律的因果链接，导致溯源报告在法律上不可采信。HunterAgent 将溯源重建问题建模为部分可观测条件下的代价有界启发式图搜索。其核心是一个非对称的生成器-验证器流水线：生成器（LLM）在类型化本体中提出语义假设，验证器通过存活的正交遥测数据中的标识符级碰撞来验证每个假设。为连接断裂的痕迹，HunterAgent 使用结合语义差异和操作系统时间势能的校准代价对跳转打分，并硬性剪除违反模式的路径。此外，长度折扣的认知预算防止推理漂移，强制优雅终止。在三个公开基准和一个内部40条痕迹数据集上，采用严格的LOFO交叉验证，HunterAgent 平均F1达到86.1%，比最好的基于智能体的基线高26.7个百分点，比KAIROS高17.1个百分点，同时将路径级幻觉从61.5%降至6.4%。在70%日志擦除情况下，召回率虽下降但精度仍保持≥84%，且95.7%的情况安全终止。所有结果在至少一个正交遥测源存活的实际假设下成立。该方法适合安全分析师、威胁狩猎人员及AI安全研究者关注，为实际环境中的自动化溯源提供了可行的神经符号融合思路。