PROMISE：基于结构模仿的人类推理证明自动化
计算机科学中的逻辑
2026-04-10 v2 软件工程
摘要
自动化证明生成在形式软件验证中仍然基本未解决，尽管大型语言模型（LLM）取得了进展。虽然LLM在自然语言处理、视觉和代码生成方面表现良好，但形式验证仍需大量人工工作。交互式定理证明（ITP）要求在严格的逻辑约束下进行手动证明构建，限制了可扩展性；例如，验证seL4微内核需要数十年的工作。现有的LLM-based方法试图自动化此过程，但仍受限。大多数方法依赖单次生成或浅层检索，这在小规模证明上可能有效，但在大规模、相互依赖的验证任务中难以应对，这些任务具有深层结构依赖。我们提出了PROMISE（PROof MIning via Structural Embeddings），一种结构感知框架，将证明生成重新表述为证明状态转换上的有状态搜索。与表层级检索不同，PROMISE从证明状态和战术转换中挖掘结构模式，使其能够在迭代搜索期间检索和适应兼容的证明片段。我们在seL4基准测试上对PROMISE进行评估，使用多个LLM后端，并与诸如Selene和Rango等先前系统进行比较。PROMISE在所有情况下都优于先前方法，实现了最高可达+26分点的提升（186%的相对增长），同时在不同模型间保持鲁棒性，证明了结构感知证明挖掘在可扩展定理证明中的有效性。
引用
@article{arxiv.2604.05399,
title = {PROMISE: Proof Automation as Structural Imitation of Human Reasoning},
author = {Youngjoo Ahn and Sangyeop Yeo and Gijung Im and Jongmin Lee and Jinyoung Yeo and Jieung Kim},
journal= {arXiv preprint arXiv:2604.05399},
year = {2026}
}