대규모 언어 모델(Large language models, LLM)은 소프트웨어 취약점에 대해 추론하는 데 점점 더 많이 사용되고 있지만, 모델의 출력값이 도메인 지식(domain knowledge)을 조용히 위반할 수 있어 의료 기기와 같은 안전 필수 환경(safety-critical settings)에서의 신뢰성을 제한합니다. 기존 연구들은 출력을 점수를 매겨야 할 예측값으로 취급하거나, 단일 지식 그래프(knowledge graph) 내의 워크(walks)로 제한하는 방식을 취했습니다. 하지만 이 중 어느 것도 바이너리(binary)에 대한 추론이 독립적인 도메인 지식 체계와 일치하는지 확인하지는 않습니다. 우리는 함의(entailment)를 통해 LLM이 제안한 각 분석가 경로(analyst path)를 검증하는 EntailLLM을 제시합니다. 여기서 경로는 바이너리의 함수 호출 그래프(function call graph)를 순회하는 것이며, 도메인 지식은 별도의 그래프로 표현됩니다. 검증 과정은 시간 주석이 달린 논리(temporal annotated logic) 하에 이 두 가지를 정렬합니다. 세 가지 CWE 클래스, 네 가지 LLM, 세 가지 프롬프팅 전략(prompting strategies), 그리고 405개에서 12,696개의 함수 호출 그래프 노드 크기를 가진 일곱 개의 바이너리에 걸쳐 실험한 결과, 도메인 지식은 통합 함의(pooled entailment)를 78%에서 98%로 높였으며, 함의가 감소한 경우는 실험의 3%에 불과했습니다. EntailLLM은 실제 의료 기기 바이너리에 엔드 투 엔드(end-to-end)로 배포되어, 기기별 튜닝 없이도 98%의 통합 함의에 도달했습니다. 우리 시스템은 일반화된 주석 논리(generalized annotated logic)의 형식적 보증(formal guarantees)을 계승하여, 설명 가능하고 잘 정의된 의미론(semantics)에 기반한 LLM 출력의 논리적 검증을 제공합니다.