一句话：首次对多个 NP 完全优化问题的近似算法进行形式化验证，发现已有证明的不完备性并改进了一个近似比。
本文首次对 NP 完全优化问题的近似算法进行形式化验证，涵盖顶点覆盖、独立集、集合覆盖、中心选择、负载均衡和装箱六个经典问题。作者在证明助手 Isabelle/HOL 中采用统一的基于不变式的方法，为每个算法建立机器检验的正确性证明，并据此给出近似比保证。该工作不仅填补了近似算法机器验证的空白，还揭示出已有文献中证明的不完备之处，并在一个案例中改进了近似比。所有证明均以不变式为核心组织，展示了统一验证框架的可行性。
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balancing, and bin packing. We uncover incompletenesses in existing proofs and improve the approximation ratio in one case. All proofs are uniformly invariant based.
@article{paperbot1719,
title = {Verified Approximation Algorithms},
author = {Robin Eßmann and Tobias Nipkow and Simon Robillard and Ujkan Sulejmani},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:36)2022}
}