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

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