[Paper] 1001 LoC的故事：潜在运行时错误引导的规范合成用于验证大规模程序

Source: arXiv - 2512.24594v1

概述

本文介绍了 Preguss，一个将静态分析与大语言模型（LLM）辅助相结合的全新框架，用于自动生成和细化大规模程序的形式规范。通过聚焦于 潜在运行时错误（RTEs），将代码库划分为可管理的验证单元，Preguss 使得演绎验证在数千行代码的项目中变得实用，手动工作量最多可降低 90 %。

关键贡献

• 错误引导的分解：一种新颖的静态分析过程，识别可能的运行时错误位置，并利用这些位置将程序划分为小的、独立的验证单元。
• 细粒度 LLM 合成：一种在单元层面工作的 LLM 驱动规格生成器，生成跨过程合约（前置/后置条件、不变式），并进行迭代细化。
• 分而治之的验证循环：将上述两个组件紧密集成，使生成的规格立即由演绎验证器检查，任何反例都会反馈回规格细化。
• 实证验证：在真实的开源项目（≥ 1 k 行代码）上进行实验，结果表明 Preguss 将人工验证工作量降低 80.6 %–88.9 %，相较于之前的基于 LLM 的流水线，并实现了完全的运行时错误消除。
• 开源原型：作者发布了可用实现，可嵌入现有的静态分析和验证工具链（如 LLVM、Frama‑C、Why3）。

方法论

1. Static‑analysis front‑end – Preguss 扫描程序的抽象语法树，以定位可能导致运行时错误的语句（空指针解引用、越界访问、除零等）。每个此类“热点”成为 verification unit 边界。
2. Unit‑level spec synthesis – 对于每个单元，构造一个提示，包含该单元的源代码、已识别的热点以及任何已知的契约。LLM（例如 GPT‑4）生成候选的前置条件、后置条件和循环不变式。
3. Deductive checking – 将生成的契约输入到定理证明器（Why3/Coq）。如果证明器成功，标记该单元为已验证；如果失败，则提取反例。
4. Iterative refinement – 将反例反馈到提示中，促使 LLM 调整规范。该循环持续进行，直至验证器证明该单元或达到超时。
5. Composition – 将已验证的单元链接在一起；跨单元的契约合并形成全局规范，从而实现整个程序的 RTE‑freeness（运行时错误自由）保证。

整个流水线实现自动化，开发者只需执行一个命令。

结果与发现

• 验证成功率：Preguss 始终能够达到 > 90 % 的 RTE‑无错误率，而纯 LLM 驱动的方法停留在 < 15 % 以下。
• 规范质量：生成的合约平均比手工编写的短 30 %，但仍能通过相同的验证检查。
• 可扩展性：运行时间随验证单元数量线性增长；最长的运行（2,100 LoC）在普通工作站上不到 12 分钟即可完成。

这些数据表明，基于错误引导的分解显著降低了 LLM 必须处理的上下文规模，规避了现有方法受限于长上下文的瓶颈。

实际影响

• 开发者生产力：团队可以在 CI/CD 中运行 Preguss，自动标记缺失的合约并提供修复建议，将传统上手动的验证步骤转变为“一键”检查。
• 安全关键代码：嵌入式、汽车和物联网开发者可以在不重写大量代码的情况下，为遗留代码库获得形式化的运行时错误（RTE）保证。
• LLM 集成最佳实践：论文展示了一种具体模式——使用静态分析来 聚焦 LLM 提示——可应用于其他代码生成任务（例如，测试用例合成、API 文档）。
• 工具链兼容性：由于 Preguss 与标准前端（LLVM IR）和后端（Why3）兼容，可轻松集成到现有的静态分析流水线中，几乎没有摩擦。

简而言之，Preguss 弥合了 LLM 的原始生成能力与演绎验证的严谨性之间的鸿沟，使形式化方法对日常软件工程更易于接受。

限制与未来工作

• 规范表达能力：当前的提示模板针对相对简单的合约（前置/后置条件、循环不变式）。更复杂的关系属性（例如时序或安全策略）仍超出范围。
• 对 LLM 的依赖：虽然框架通过细化循环容忍偶尔的 LLM 幻觉，但其成功仍取决于底层模型对目标语言/库 API 的了解。
• 动态特性：静态分析假设代码主要是过程式风格；大量使用反射、动态分派或 JIT 生成的代码可能会破坏单元分解。
• 未来方向：作者计划（1）扩展 Preguss 以处理并发原语，（2）探索多 LLM 集成以获得更丰富的规范词汇表，以及（3）集成学习的成本模型，以优先验证最“有影响”的单元。

Preguss 标志着朝着真正自动化、大规模形式化验证迈出的有希望的一步，其模块化设计为渴望在生产代码中引入形式化保证的开发者提供了实用路径。

作者

• Zhongyi Wang
• Tengjie Lin
• Mingshuai Chen
• Haokun Li
• Mingqi Yang
• Xiao Yi
• Shengchao Qin
• Yixing Luo
• Xiaofeng Li
• Bin Gu
• Liqiang Lu
• Jianwei Yin

论文信息

• arXiv ID: 2512.24594v1
• 分类: cs.SE, cs.LO
• 发表时间: 2025年12月31日
• PDF: 下载 PDF