该论文针对大语言模型（LLM）在软件漏洞推理中可能静默违反领域知识、导致安全关键场景（如医疗设备）可靠性不足的问题，提出了一种基于逻辑编程的验证框架 EntailLLM。现有方法要么将 LLM 输出仅作为待评分的预测，要么将其限制在单张知识图谱的路径遍历中，均未检查对二进制程序的推理是否与独立领域知识保持一致。EntailLLM 的核心思路是将每条 LLM 提出的分析师路径视为对二进制函数调用图的遍历，并将领域知识表示为另一张独立图谱，然后在时序注释逻辑（temporal annotated logic）下将两者对齐，通过蕴含（entailment）验证每条路径的合理性。实验覆盖三个 CWE 类别、四种 LLM、三种提示策略，以及七个规模从 405 到 12,696 个函数调用图节点的二进制程序。结果显示，加入领域知识后，池化蕴含率从 78% 提升至 98%，仅有 3% 的实验出现蕴含率下降。该系统已端到端部署于真实医疗设备二进制程序，无需针对具体设备调整即可达到 98% 的池化蕴含率。EntailLLM 继承了广义注释逻辑的形式化保证，为 LLM 输出提供可解释且基于明确语义的逻辑验证。本文适合安全分析自动化、LLM 在静态分析中的应用、以及形式化验证与 AI 结合方向的研究者和工程师阅读。