一句话：Cobblestone 用 LLM 分治合成 Coq 证明：拆分已验证子目标并迭代，保持可靠性，自动化形式验证。
Coq 等证明助手可提升软件可靠性，但验证需大量专家工作，现有机器学习证明合成仅能证明少数性质。Cobblestone 用分治法合成证明：大语言模型生成候选证明，将其拆成更简单子目标，自动识别已证部分，再对剩余子目标迭代，最终即使依赖不可靠 LLM 也能产出可靠证明。作者在四个开源 Coq 项目基准上控制数据泄露评估：全自动模式优于最先进非 LLM 工具，也能证明许多其他 LLM 工具无法证明的定理；平均每次成本 1.25 美元、耗时 14.7 分钟，使用外部 oracle 时最高证明 58% 定理。
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to prove only a fraction of desired software properties. We introduce Cobblestone, a divide-and-conquer approach for proof synthesis. Cobblestone uses a large language model (LLM) to generate potential proofs, uses those proofs to break the problem into simpler parts, automatically identifies which of those parts were successfully proven, and iterates on the remaining parts to build a correct proof that is guaranteed to be sound, despite the reliance on unsound LLMs. We evaluate Cobblestone on four benchmarks of open-source Coq projects, controlling for training data leakage. Fully automatically, Cobblestone outperforms state-of-the-art non-LLM tools, and proves many theorems that other LLM-based tools cannot, and on many benchmarks, outperforms them. Each Cobblestone run costs only $1.25 and takes 14.7 minutes, on average. Cobblestone can also be used with external input, from a user or another tool, providing a proof structure or relevant lemmas. Evaluated with such an oracle, Cobblestone proves up to 58% of theorems. Overall, our research shows that tools can make use of partial progress and external input to more effectively automate formal verification.
@inproceedings{paperbot11590,
title = {Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification},
author = {Saketh Ram Kasibatla and Arpan Agrawal and Yuriy Brun and Sorin Lerner and Talia Ringer and Emily First},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3773178}
}