# EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming

arXiv: https://arxiv.org/abs/2608.01763 · HTML: https://mlsanity.com/paper/2608.01763/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 26 references that are in the map.
- First posted on arXiv 3 Aug 2026.

## Builds on (most cited first, 6 of 6)

- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [LLMs Cannot Reliably Identify and Reason About Security Vulnerabilities (Yet?): A Comprehensive Evaluation, Framework, and Benchmarks](https://mlsanity.com/paper/2312.12575/) (2023)
- [LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights](https://mlsanity.com/paper/2502.07049/) (2025)
- [An Observational Investigation of Reverse Engineers' Processes](https://mlsanity.com/paper/1912.00317/) (2019)
- [Harnessing the Power of LLM to Support Binary Taint Analysis](https://mlsanity.com/paper/2310.08275/) (2023)
- [Extensions to Generalized Annotated Logic and an Equivalent Neural Architecture](https://mlsanity.com/paper/2302.12195/) (2023)

## Built on by (most cited first, 1 of 1)

- [Automating Attack Graph Construction for Agentic Pentesting. Towards Neuro-Symbolic Vulnerability Hunting](https://mlsanity.com/paper/2609.15523/) (2026)

## Abstract (arXiv)

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.