一句话：提出 Adapt 框架，用 LLM 引导的决策器动态选择证明精化策略，显著提升定理证明的自动化成功率。
定理证明可实现严格的软件正确性验证，但因需要大量人工投入与专业知识而难以规模化。LLM 虽在自动生成证明上展现潜力，但首次生成的证明往往不正确，需要迭代精化；而现有方法大多采用固定的精化策略，无法根据具体情况动态选择有效策略，限制了性能。本文提出 Adapt，一个新颖的证明精化框架：它利用 LLM 引导的决策器，根据证明助手的状态以及错误证明的可用上下文，动态选择适合的精化策略。作者在两个基准套件上对比五种现有方法，Adapt 分别比最佳基线多证明 11.26% 和 18.58% 的定理；同时在六种不同 LLM 上验证了泛化性，并通过消融实验量化各组件的贡献、比较不同决策器设计的取舍。
Formal verification via theorem proving enables rigorous proofs of software correctness, but it is difficult to scale due to the significant manual effort and expertise required. While Large Language Models (LLMs) have shown potential in automating proof generation, they frequently produce incorrect proofs on the first attempt that require iterative refinement to fix. However, most existing approaches employ fixed refinement strategies and cannot dynamically choose an effective strategy, which limits their performance. To overcome this limitation, we introduce Adapt, a novel proof refinement framework that leverages an LLM-guided decision-maker to dynamically select a suitable refinement strategy according to the state of the proof assistant and available context of an incorrect proof. We evaluate Adapt on two benchmark suites against five existing methods and find that it significantly outperforms the best baseline on both by proving 11.26% and 18.58% more theorems, respectively. Furthermore, we demonstrate Adapt’s generalizability by evaluating it across six different LLMs. We also conduct ablation studies to measure the contribution of each component and compare the trade-offs of alternative decision-maker designs.
@inproceedings{abs-2510-25103,
title = {Adaptive Proof Refinement with LLM-Guided Strategy Selection},
author = {Minghai Lu and Zhe Zhou and Danning Xie and Songlin Jia and Benjamin Delaware and Tianyi Zhang},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834382}
}