大规模计算机生成证明的认证证明检查器的优化

在近期工作中，我们形式化了最优规模排序网络的理论，旨在提取一个经过验证的检查器，用于验证大规模计算机生成的证明——该证明表明在对9个输入进行排序时25次比较是最优的，其需要超过十年的CPU时间并产生了27 GB的证明见证。该检查器使用基于这些见证的不可信预言机，能够在几天内验证8个输入的较小情况，但无法扩展到9个输入的完整证明。本文中，我们描述了检查器中算法的若干非平凡优化，通过适当改变形式化并充分利用与预言机恰当实现的共生关系获得。我们提供了实验证据，表明对于8个输入，运行时间和内存占用量级均改善数个数量级，并且实际成功检查了9个输入的完整证明。