AI 中文总结
针对电路最小化中缺乏最优性证明的问题，提出带DRAT证明的合成流水线，认证121个最优结果，验证发现代码审查遗漏的缺陷。
AI 中文摘要
综合流水线越来越多地声称程序不仅正确，而且是最优的。这样的声明包含两个部分，其验证故事截然不同。上界“存在一个大小为 m 的程序”由一个可重新执行的人工制品见证，该制品被证明与其规范等价，并附带机器检查的证书。下界“不存在大小为 m-1 的程序”没有见证，而是通过运行求解器直到其报告 UNSAT 来消解。组合优化数十年前就认识到这种不对称性，并已基本解决：认证算法使其显式化（McConnell 等人，2011），伪布尔证明记录可以通过形式化验证的检查器端到端地认证最优性（Bogaerts 等人，2023；Koops 等人，2025）。该纪律尚未触及电路最小化。我们称之为反驳差距：已发布的最小 XOR 电路的逻辑门数量没有为声明的任何一半提供证书，我们自己产生的 121 个最优性结果也没有。我们通过一个流水线弥合了这一差距，该流水线在 GF(2) 上合成最小线性直线程序，其中每个决定性的 UNSAT 答案都会发出 DRAT 证明，并由独立的第三方检查器检查。我们认证了该项目建立的所有 121 个最优性结果，涵盖 n = 6 到 9：111 个携带独立验证的反驳，10 个由自由计数界限闭合，没有一个与未认证的值不一致。证明的中位大小为 1.1 MB，检查成本为求解成本的 1.9 倍。我们给出了五个案例研究，其中验证捕获了代码审查未发现的缺陷，报告了两个将从业者推向未认证路径的接口障碍，并描述了一次对抗性审计，该审计揭示了一个失败尾部，我们原本要将其归因于问题，实际上是由我们自己的预算造成的。
英文摘要
Synthesis pipelines increasingly claim not just that a program is correct, but that it is optimal. Such a claim has two halves with radically different verification stories. The upper bound, "a program of size m exists", is witnessed by an artifact that can be re-executed, proved equivalent to its specification, and shipped with a machine-checked certificate. The lower bound, "no program of size m-1 exists", has no witness and is discharged by running a solver until it reports UNSAT. Combinatorial optimization has known this asymmetry for decades and has largely addressed it: certifying algorithms make it explicit (McConnell et al., 2011), and pseudo-Boolean proof logging can certify optimality end to end with a formally verified checker (Bogaerts et al., 2023; Koops et al., 2025). That discipline has not reached circuit minimization. We call this the refutation gap: published gate counts for minimal XOR circuits provide no certificate for either half of the claim, and neither did 121 optimality results we ourselves produced. We close the gap with a pipeline that synthesizes minimal linear straight-line programs over GF(2), where every decisive UNSAT answer emits a DRAT proof checked by an independent third-party checker. We certify all 121 optimality results established by the project, across n = 6 to 9: 111 carry independently verified refutations, 10 are closed by a free counting bound, and none disagrees with the uncertified value. The median proof is 1.1 MB and checking costs 1.9x solving. We give five case studies where verification caught defects that code review did not, report two interface obstacles that push practitioners toward the uncertified path, and describe an adversarial audit that revealed a failure tail we were about to attribute to the problem was actually caused by our own budget.
