一句话：提出一种全自动、鲁棒于等价表述的定理性质测试策略，把生成器搜索建模为约束调度问题。
交互式定理证明中，先用基于性质的测试检验定理，有助于在投入证明前发现错误定义或错误陈述。但现代证明助手的测试基础设施仍不完善：Rocq 的 QuickChick 虽能为归纳关系随机生成满足约束的数据，却常需大量专业技巧，且效果高度依赖定理中假设顺序和归纳关系中约束顺序。本文提出一种全新定理测试策略，将 QuickChick 风格的性质与生成器空间刻画为约束调度问题，并引入归纳关系的“密度”概念估计生成器在任意输入下成功的倾向，从而自动搜索最佳性质或生成器。作者在 Rocq 的 QuickChick 上实现该算法，并用文献案例评估，表明一键自动化可与专家手工测试媲美，有时更能发现缺陷。
While the ultimate goal of interactive theorem proving is to prove theorems, it can really help to test them first. Testing theorems, specifically using property-based testing, helps users identify incorrect definitions and theorem statements before they waste time on a proof that could never succeed. Unfortunately, the testing infrastructure provided by modern theorem provers has yet to reach its full potential. Even QuickChick, the state-of-the-art property-based testing framework for Rocq, which offers random generation for data satisfying inductively defined relations, often requires substantial effort and expertise to be used effectively. This is in part because this effectiveness is heavily sensitive to both the order that hypotheses appear within a theorem, and to the order that inductive constraints appear within the inductive relations involved. In this paper, we present a novel strategy for testing theorems that is highly effective, fully automatic, and robust to equivalent formulations of theorem and definition statements. To do so, we characterize the exponentially large space of possible QuickChick-style properties and generators as solutions to a constrained scheduling problem. To find the best property or generator in this space, we estimate effectiveness by introducing a notion of "density" for inductive relations, which approximates the tendency for a generator to succeed given arbitrary inputs. We implement our algorithm on top of the QuickChick framework for Rocq and evaluate it in a number of case studies from the literature, demonstrating that our push-button automation is on par with and in some cases even more effective at finding bugs than expertly handcrafted tests.
@article{paperbot12148,
title = {Testing Theorems, Fully Automatically},
author = {Segev Elazar Mittelman and Harrison Goldstein and Leonidas Lampropoulos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839453}
}