Abstract
Large language model agents are increasingly used to analyze potential 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 entailed by an independent body of domain knowledge. We present EntailLLM, a framework that includes a specialized LLM agent and a validation mechanism. The agent proposes a traversal path of the function call graph for a vulnerability, which is checked against a separate knowledge graph and a logic program by an entailment procedure under annotated logic. We evaluate EntailLLM by examining six specialized agents across three CWE classes, and eight binaries varying in size from 405 to 12,696 functions. The agents improve pooled entailment from 77% to 98%, with entailment decreasing in only 3 of 118 configurations. We found that the best-performing agent combines self-refinement and a priori domain knowledge. EntailLLM is deployed end-to-end on real medical-device binaries, reaching 98% pooled entailment without per-device tuning. Our framework inherits the formal guarantees of generalized annotated logic, providing logical verification of agent output that is both explainable and grounded in well-defined semantics.
Abstract (translated)
URL
https://arxiv.org/abs/2608.01763
