Imandra CodeLogician：用于精确分析软件逻辑的神经符号推理

大型语言模型（LLM）在代码理解任务上表现强劲，但它们从根本上缺乏对程序行为进行精确、穷举数学推理的能力。现有基准要么侧重于数学证明自动化，与实际软件严重脱节，要么侧重于不需要语义严谨性的工程任务。我们提出了 CodeLogician，一个用于精确分析软件逻辑的神经符号智能体，并与 ImandraX 集成，后者是部署在金融市场和安全关键系统中的工业级自动推理引擎。与先前主要使用形式化方法验证 LLM 输出的方法不同，CodeLogician 使用 LLM 构建软件系统的显式形式化模型，从而能够进行自动推理，以回答超越二元验证结果的丰富语义问题。为了严格评估关于软件逻辑的数学推理，我们引入了 code-logic-bench，这是一个针对定理证明与软件工程基准之间中间地带的基准。它衡量关于程序状态空间、控制流、覆盖约束和边缘情况的推理正确性，其真实答案通过形式化建模和区域分解来定义。将仅使用 LLM 的推理与通过 CodeLogician 增强的 LLM 进行比较，形式化增强带来了显著改进，弥合了 41-47 个百分点的推理准确率差距。这些结果表明，神经符号集成对于将程序分析扩展至严谨、自主的软件理解至关重要。