一句话：提出 ProofCoop，让多个证明合成模型在搜索中协作，显著提升 Coq 定理自动证明成功率。
在 Coq、Lean 等证明助手中，机器学习虽可自动合成证明，但现有方法成功率有限。已有组合多模型的方法（如 Diva）让各模型独立搜索，未能利用模型间协作。本文提出 ProofCoop，首次实现模型间协作式证明合成，支持六种协作方式：联合下一步预测、投票/竞标/堆叠式偏好预测、搜索中共享已证明引理，以及模型补全彼此的部分证明。在 CoqGym（124 个开源 Coq 项目、68.5K 定理，11.9K 测试定理）上，五个模型组合下 Diva 证明 3287 个（27.5%），最佳单模型证明 2604 个（21.8%），而 ProofCoop 证明 3937 个（33.0%），比此前最优组合方法平均高 19.8%；结合 CoqHammer 可达 36.0%。
Formal verification using proof assistants, such as Coq or Lean, is an effective way of ensuring software correctness. Recent research has shown that machine learning can automate proof synthesis, but such approaches are only successful a fraction of the time. Methods for improving such proof synthesis include training more precise models, improving the model-driven synthesis search mechanisms, and effectively combining multiple models into synthesis search. This paper focuses on the latter and develops ProofCoop, for the first time demonstrating collaborative cooperation between models. Diva, the state-of-the-art method for combining models, uses a disparate search for each model. On the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects a Diva combination of five models automatically proves 3,287 (27.5%) of CoqGym’s 11.9K test set theorems, while the best individual model proves only 2,604 (21.8%). By contrast, our method, ProofCoop can use the same five models to fully automatically prove 3,937 (33.0%) theorems, meaning that ProofCoop is 19.8% more likely to prove a theorem, on average, than the prior state of the art combination method. ProofCoop allows its models to build on each other’s contributions and demonstrates that such collaboration significantly increases synthesis success. ProofCoop enables six different types of collaboration: joint model next-step prediction at each search step; preferential next-step prediction via voting, bidding, and stacking; sharing lemmas proven across models mid-search, and models completing each other’s partial proofs. Together with CoqHammer, ProofCoop synthesizes proofs for 36.0% of the theorems. Our research demonstrates that creative uses of learned models can lead to collaborative synthesis that is more effective than prior approaches, suggesting a powerful new research direction in automated formal verification.
@inproceedings{paperbot11952,
title = {ProofCoop: Collaborative Automated Formal Verification},
author = {Zhanna Kaufman and Emily First and Alex Sanchez-Stern and Kyle Thompson and Sorin Lerner and Yuriy Brun},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787783}
}