IRONPROOF：COBOL 到 Python 的转换以及基于 SMT 的等效性检查

将 COBOL 翻译为现代语言可能会改变程序的计算内容，并且 LLM 翻译不保证等效性。我们提出了 IRONPROOF，它将 COBOL 解析为中间表示，生成 Python，通过共享输入将两者编码为 Z3 公式，并发出机器可检查的等价证书 (UNSAT) 或反例 (SAT)。在 2,345 个 COBOL 文件（GnuCOBOL 测试、NIST CCVS85、开源集合以及我们生成或编写的程序）中，有 782 个进入检查路径：606 个（77.5%）被证明是等效的，101 个经过部分验证，没有一个被反驳，75 个在我们的管道内失败并留在分母中。在独立编写的程序中，这一比例为 52.6%（291 个程序中的 153 个），而在我们编写的程序中，这一比例为 92.3%。在 153 个独立证明中，37 个涵盖了读取编码器未建模的输入的程序的单次执行，并且在所有 606 个证明中，只有 14 个对已证明输出所依赖的输入进行量化。在两个公共业务应用程序语料库（AWS CardDemo 和 IBM GenApp）上，编码器没有端到端地对程序进行建模。 2026 年 4 月 仅 LLM 基线在 94 个独立编写的程序中的 54 个上失败，计算我们的编码器无法验证的翻译。 PIC 范围溢出检测会标记其可分析的 22.1% 程序中的超出范围输出（这是上限）。早期与 GnuCOBOL 3.2.0 的对抗发现 49 个可执行独立证明中有 24 个与证明域中变量的运行时不一致。证明表明生成的 Python 计算的是我们的中间表示形式所说的 COBOL 计算的内容，而不是等同于 COBOL 实现。