AI 中文总结
针对大语言模型在程序错误查找中产生大量误报的问题，提出Mizzle方法，它是一种用于并发程序的错误分离逻辑，在Rocq证明助手实现机械化，能防止误报且完整，还通过三种错误概念实例化并展示其可用于证明错误存在。
AI 中文摘要
大型语言模型越来越多地用于在实际程序中查找错误，但它们也会产生大量误报，浪费开发者时间。我们提出一种方法，要求语言模型在每个错误报告中附带一个在程序逻辑中经过机器检查的证明，以表明报告的错误是真实的，从而防止误报。我们采用错误逻辑的方法，其欠近似推理确定声称的行为确实可达，因此是真正的阳性。然而，在我们的案例中，该逻辑必须对现实的编程语言进行建模，具有机械化以便可以检查证明，并且是完整的，这样就不会因缺乏推导而排除任何真正的错误。我们展示了Mizzle，一种针对用OCaml的大量子集编写的并发程序的错误分离逻辑，在错误概念上是参数化的。我们在Iris框架之上的Rocq证明助手对Mizzle进行机械化，并证明它既合理（即从不为误报辩护）又完整（即每个不正确的执行都允许推导）。我们用三种错误概念实例化Mizzle：卡住（触发未定义行为）、数据结构的非线性化和竞争的存在。作为概念验证，我们说明了语言模型如何使用Mizzle来证明错误的存在。
英文摘要
Large language models are increasingly used to find bugs in real-world programs, but they also produce a flood of false alarms that waste developers' time. We propose a method to prevent these false alarms by requiring an LLM to accompany each bug report with a machine-checked proof, in a program logic, that the reported bug is real. We follow the approach of incorrectness logics, whose under-approximate reasoning establishes that a claimed behavior is genuinely reachable, and hence a true positive. In our case, however, the logic must model a realistic programming language, have a mechanization so that proofs can be checked, and be complete, so that no real bug is ruled out for want of a derivation. We present Mizzle, an incorrectness separation logic for concurrent programs written in a substantial subset of OCaml, parametric in the notion of incorrectness. We mechanize Mizzle in the Rocq proof assistant on top of the Iris framework, and we prove that it is both sound (that is, it never justifies a false alarm) and complete (that is, every incorrect execution admits a derivation). We instantiate Mizzle with three notions of incorrectness: stuckness (triggering undefined behavior), the non-linearizability of a data structure, and the presence of a race. As a proof of concept, we illustrate how an LLM can use Mizzle in order to certify the existence of a bug.
