EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming
2026-08-03 • Cryptography and Security
Cryptography and SecurityArtificial IntelligenceLogic in Computer ScienceSoftware Engineering
AI summaryⓘ
The authors created a system called EntailLLM that checks if the reasoning from large language models (LLMs) about software vulnerabilities matches established domain knowledge. Instead of just trusting the LLM output or limiting it to one knowledge base, their method compares the LLM’s path through a program's function calls with a separate knowledge graph using logical rules. They tested this on different software types and found that including domain knowledge greatly improved the correctness of the reasoning. EntailLLM works well even on real medical device software without extra customization and provides explainable, logically verified results.
large language modelssoftware vulnerabilitiesfunction call graphdomain knowledgeentailmentknowledge graphannotated logicmedical devicesvulnerability analysis
Authors
Kaustuv Mukherji, Jaikrishna Manojkumar Patil, Colton Payne, Paulo Shakarian, Dana Warmsley, Nigel Stepp, Evelyn Kim
Abstract
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.