用逻辑编程验证大模型漏洞发现路径是否符合领域知识
EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming
- 通过逻辑编程比对程序调用图与领域知识图，检验推理路径一致性
- 在7个医疗设备二进制上，整体可满足性从78%提升至98%
- 无需针对每个设备调参，适合高安全要求的软件漏洞检测
大型语言模型被用于分析软件漏洞，但其输出可能隐式违反领域知识，影响在医疗设备等高安全场景下的可靠性。现有方法或仅对输出评分，或限制于单一知识图谱中的路径遍历，均无法验证推理是否与独立领域知识一致。本文提出EntailLLM，通过逻辑蕴含验证每个大模型生成的分析路径：路径是二进制函数调用图的遍历，领域知识以独立图表示，验证过程基于带时间标注的逻辑进行对齐。在三个CWE类别、四种大模型、三种提示策略及七个规模从405到12,696个节点的二进制上，领域知识使整体可满足性从78%提升至98%，仅有3%实验出现下降。系统已在真实医疗设备二进制上端到端部署，无需针对设备调参即可达到98%的总体可满足性。系统继承广义标注逻辑的形式保证，提供可解释且语义明确的逻辑验证。
原文摘要 · Abstract (English)
Large language models are increasingly used to reason about software vulnerabilities, but their outputs can silently violate domain knowledge, limiting their reliability in safety-critical settings such as medical devices. Prior work either treats that output as a prediction to be scored or constrains it to walks within a single knowledge graph; neither checks whether reasoning over a binary is consistent with an independent body of domain knowledge. We present EntailLLM, which validates each LLM-proposed analyst path by entailment: the path is a traversal of the binary's function call graph, the domain knowledge is represented in a separate graph, and verification aligns the two under temporal annotated logic. Across three CWE classes, four LLMs, three prompting strategies, and seven binaries varying in size from 405 to 12,696 function call-graph nodes, domain knowledge raises pooled entailment from 78% to 98%, with entailment decreasing in only 3% of the experiments. EntailLLM is deployed end-to-end on real medical-device binaries, reaching 98% pooled entailment without per-device tuning. Our system inherits the formal guarantees of generalized annotated logic, providing logical verification of LLM output that is both explainable and grounded in well-defined semantics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。