证明助手中的测试用例自动约简：以 Coq 为例
软件工程
2025-03-12 v2
摘要
随着证明助手采用的增加，亟需高效地识别、记录并修复由证明助手演进引发的兼容性问题。我们提出 Coq Bug Minimizer，一种用最小且独立文件复现缺陷行为的工具，并与 coqbot 集成以在 Coq 反向 CI 失败时自动触发。我们的工具消除了下载、配置、编译然后探索和理解大型开发项目的开销：使 Coq 开发者能轻松获取模块化测试用例文件以进行快速实验。本文中，我们描述了关于 Coq 中测试用例约简不同于传统编译器的见解。我们期望这些见解能推广到其他证明助手。我们在超过 150 个 CI 失败上评估了 Coq Bug Minimizer。该工具约 75% 的情况下成功将失败约简为更小的测试用例。约简器在 89% 的情况下生成完全独立的测试用例，其平均大小约为原始测试的三分之一。平均约简测试用例在 1.25 秒内编译，其中 75% 在半秒内完成。
引用
@article{arxiv.2202.13823,
title = {Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq},
author = {Jason Gross and Théo Zimmermann and Rajashree Agrawal and Adam Chlipala},
journal= {arXiv preprint arXiv:2202.13823},
year = {2025}
}