대규모 언어 모델(LLM)은 실제 프로그램의 버그를 찾는 데 점점 더 많이 사용되고 있지만, 개발자의 시간을 낭비하는 수많은 오탐(false alarms)도 생성합니다. 우리는 LLM이 보고된 버그가 실제로 존재한다는 것을 증명하는 기계 검증된 증거(machine-checked proof)를 각 버그 보고서에 첨부하도록 요구함으로써 이러한 오탐을 방지하는 방법을 제안합니다. 우리는 부정확성 논리(incorrectness logics)의 접근 방식을 따르는데, 이 논리는 근사 추론(under-approximate reasoning)을 통해 주장된 동작이 실제로 도달 가능한지, 따라서 참 양성(true positive)인지를 확립합니다. 그러나 우리의 경우, 해당 논리는 현실적인 프로그래밍 언어를 모델링해야 하고, 증명이 검사될 수 있도록 기계화되어야 하며, 그리고 아무런 유도 과정의 부재로 인해 실제 버그가 배제되지 않도록 완전성(complete)을 가져야 합니다. 우리는 OCaml의 상당한 부분집합으로 작성된 동시성 프로그램에 대한 부정확성 분리 논리(incorrectness separation logic)인 Mizzle을 제시하며, 이는 부정확성의 개념에 대해 매개변수화되어 있습니다. 우리는 Rocq 증명 보조기(proof assistant)에서 Iris 프레임워크 위에 Mizzle을 기계화하고, 이것이 음이도(sound, 즉 오탐을 결코 정당화하지 않음)하고 완전성(complete, 즉 모든 부정확한 실행은 유도를 허용함)하다는 것을 증명합니다. 우리는 세 가지 부정확성의 개념으로 Mizzle을 인스턴스화합니다: 막힘(stuckness, 정의되지 않은 동작을 유발하는 것), 데이터 구조의 비선형성(non-linearizability), 그리고 경쟁 조건(race)의 존재입니다. 개념 증명으로서, LLM이 버그의 존재를 인증하기 위해 Mizzle을 어떻게 사용할 수 있는지 보여줍니다.