一个大规模计算机生成证明的最优化证明算法
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
摘要：
在最近的工作中，我们形式化了最优大小排序网络的理论，目标是提取一个经过验证的检查器，用于大规模计算机生成的证明，即在对9个输入进行排序时，25个比较是最优的，这需要十多年的CPU时间，并产生27 GB的证明证人。检查器使用基于这些证人的不可信的预言机，并且能够在几天内验证8个输入的较小情况，但它没有扩展到9个输入的完整证明。在本文中，我们描述了几个非平凡的优化算法的检查器，通过适当地改变形式化和资本化的共生与适当的实施的甲骨文。我们提供了8个输入的运行时间和内存占用的数量级改进的实验证据，实际上，我们设法检查了9个输入的完整证明。
英文摘要：
In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
