viverra text-to-code with guarantees¶

会议: NeurIPS 2026
arXiv: 2605.14972
OpenReview: https://openreview.net/forum?id=35jwwbZdxS
领域: 代码智能
关键词: 文本到代码生成, 有界模型检测, 程序断言, 组合式验证, 形式化保证

一句话总结¶

Viverra 提出了一种文本到代码的半自动形式化协同规范框架，通过大语言模型同时生成 C 语言程序与候选正确性/安全断言，并结合有界模型检测工具组合完成组合式验证，为 AI 生成的代码提供可证明的行为保证并大幅提升人工理解效率。

研究背景与动机¶

基于大语言模型的文本到代码（Text-to-Code）合成技术极大地提升了软件工程的开发效率，但大模型生成的代码本质上缺乏严格的正确性保证。生成代码往往隐藏着逻辑漏洞、未考虑的边界情况以及隐式假设违背，开发者依然必须投入大量精力审查、测试和维护生成代码，这严重抵消了 AI 编程工具带来的生产力红利。面对自然语言需求与精确代码之间的语义鸿沟，完全依赖人工逐行审查不仅枯燥低效，而且在面对复杂控制流和深层状态机时极易遗漏隐蔽缺陷。

在弥合代码信任缺口方面，传统的测试手段只能采样有限输入空间，无法证明普遍行为特征；而依赖 Lean、Rocq 等交互式定理证明器的全形式化验证门槛极高，即使在大模型辅助下依然需要耗费巨量时间编写完备证明，难以适应高吞吐代码生成场景。现有实践在轻量级测试与重量级形式化验证之间存在明显的中间地带空白。开发者真正需要的是一种无需手动编写复杂规格、成本实用且能提供比单元测试更强形式化保证的代码理解辅助机制。

针对这一核心权衡，本文提出在轻量测试与全形式化之间探索最佳折衷。大模型不仅具备生成代码的能力，同样具备理解自然语言需求并析出对应前置/后置条件与不变式潜力的特征。核心 idea：提出部分协同规范与尽力而为组合式验证范式，由大模型协同生成程序与候选断言，利用有界模型检测投资构筑调用图依赖的断言验证闭环，将形式化验证结果转化为可读自然语言事实嵌入代码以辅助理解。

方法详解¶

整体框架¶

Viverra 框架以用户提供的自然语言任务描述 \(D\) 和循环展开界限 \(k\) 为输入，输出带有可证明形式化事实注释的 C 语言程序。其整体流水线分为五个主要阶段：属性抽取、验证友好型代码合成、断言嵌入与循环界限压缩、组合式有界模型检验、以及事实翻译与代码嵌入。系统通过“协同规范（Co-specification）”将需求抽取为断言，再通过静态分析与 SMT/BMC 求解器组合滤除虚假属性并确定条件依赖，最终把验证通过的断言转化为直观的自然语言行内注释。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["自然语言任务描述 D"] --> B["属性抽取与验证友好型代码合成"]
    B --> C["断言嵌入与静态循环界限压缩"]
    C --> D["基于调用图遍历的断言拓扑排序"]
    D --> E["组合式有界模型检验与蕴含图构建"]
    E --> F["依赖闭包化简与事实自然语言生成"]
    F --> G["输出带形式化保证的 C 代码"]

关键设计¶

1. 属性抽取与验证友好型代码合成：规避复杂语义陷阱的前端协同生成

为了让生成的程序天然具备被自动化 SMT/BMC 工具判定的可行性，Viverra 避免直接沿用标准自由合成模式，而是将合成拆解为显式的约束生成。在属性抽取阶段，LLM 提炼出针对功能性与安全性的自然语言属性集合 \(\Pi = \{\pi_1, \dots, \pi_n\}\) 作为概念核查清单；在代码合成阶段，系统向 LLM 注入强验证友好型约束，明确禁止递归调用、禁止堆动态内存分配（malloc/free）、禁止浮点数运算与复杂指针算术，同时强制要求静态数组边界以及采用 strnlen 替代 strlen。在断言生成步骤中，LLM 将属性映射到函数入口前置条件、出口后置条件以及辅助谓词函数上。通过预编译检查自动捕获语法错误并回传错误重新提示，从源头上消除了未定义行为和发散状态机对后继模型检测器的干扰。

2. 尽力而为的有界循环界限压缩：消除虚假反例的静态预处理

在有界模型检测（BMC）语义中，当循环反向边遍历超过预设界限 \(k\) 时，求解器默认在第 \(k+1\) 次迭代插入 assert(false) 以检测展开溢出。如果目标程序的循环本身合乎逻辑但需要执行多于 \(k\) 次，模型检测器会报告展开违例，形成与程序真实功能无关的虚假反例（Spurious Counterexamples）。为了解决该痛点，Viverra 引入了界限压缩（Bound Reduction）预处理机制：指导 LLM 静态调整并紧缩编译期常量与宏定义（如将最大迭代次数、缓冲区大小等压缩至不大于 \(k\) 的安全阈值），确保在任意可行输入下循环遍历深度均被严格限制在 \(k\) 步以内。这一妥协使系统放弃了对无限状态的完全完备性，换取了完全确定、无伪展开报错的高效判定能力。

3. 基于调用图拓扑的组合式验证：利用前序断言假设的依赖求解

生成的断言可能涉及跨函数的调用依赖，单一断言直接求解极易遭遇状态爆炸或前置条件缺失导致的未定/假证伪。Viverra 首先借助 libclang 提取程序的调用图 \(G(\mathcal{P})\)，从 main 函数出发执行深度优先遍历（结合成环规避策略）构造全局断言线性拓扑序 \(t = [a_1, \dots, a_m]\)。在该顺序中，被调用函数的后置条件总是在调用点之后的主调函数断言之前完成处理。在核心验证过程（VerifyAll）中，系统维护一个记录逻辑依赖关系的蕴含图 \(IG\)。对任意候选断言 \(a_i = \langle f_i, l_i, \phi_i \rangle\)，算法首先尝试无假设的独立检验 \(\mathcal{V}_k(\mathcal{P}, \emptyset, a_i)\)；若无法独立证明，则将所有位于其前序的断言集合 \(S = \{a_j : j < i\}\) 提升为假设约束 \(\mathsf{assume}(\phi_j)\)，进行条件检验 \(\mathcal{V}_k(\mathsf{Asm}(\mathcal{P}, S), \emptyset, a_i)\)。若在先验假设下验证通过，则将依赖关系 \(IG[i] \leftarrow S\) 记录在案。

4. 依赖闭包收敛与自然语言事实生成：可解释形式化凭据的交付呈现

为了向用户提供简洁可信的形式化结论，系统基于蕴含图计算每个断言的依赖闭包 \(\mathsf{Deps}(a_i) = \bigcup_{a_j \in IG[i]} \mathsf{Deps}(a_j)\)，递归回溯至最原始的根假设集合。论文从理论上严格证明了在 \(k\)-有界执行集合 \(\mathsf{Exec}_k(\mathsf{Asm}(\mathcal{P}, \mathsf{Deps}(a_i)))\) 下断言成立的可靠性（Soundness）。最终，Viverra 将成功通过验证的断言分类打标：无依赖成立的独立性质标注为 //FACT[k=K]，带有前序依赖的条件性质标注为 //FACT[k=K, cond] 并附带依赖集合。系统再次调用 LLM 将数学断言一对一翻译为易读的自然语言描述，替换原代码中的底层 assert() 宏，让开发者在保留原始代码排版的同时获得经过数学证明的语义注解。

一个完整示例¶

以冒泡排序任务（Bubble Sort）为例，系统从任务需求中抽取属性：\(\pi_1\)（循环后相邻元素有序）与 \(\pi_2\)（调用辅助函数校验整个数组处于升序）。 1. 代码合成生成包含嵌套循环与辅助验证函数 is_sorted 的 C 代码。 2. 断言生成阶段在内层循环后插入 \(a_1: \texttt{assert}(arr[j] \le arr[j+1])\)，在函数末尾插入 \(a_2: \texttt{assert}(is\_sorted(arr, n))\)。 3. 循环界限压缩将数组上限常量定义宏从原始可能的 100 缩减至 \(k=5\)。 4. 模型检测器先验证内层局部性质 \(a_1\)，BMC 顺利返回 Verified，因此 \(IG[1] = \emptyset\)。 5. 验证全局排序性质 \(a_2\) 时，先尝试无假设求解，若求解超时或复杂度过高，系统将 \(a_1\) 作为前提约束 \(\mathsf{assume}\) 引入求解上下文，成功证明 \(a_2\) 在条件集合 \(\{a_1\}\) 下成立。 6. 最终在输出代码中将 \(a_1\) 与 \(a_2\) 分别替换为 //FACT[k=5]: Adjacent elements are in non-decreasing order. 与 //FACT[k=5, cond]: Array is fully sorted.。

实验关键数据¶

主实验¶

论文在涵盖算法（如冒泡排序、最短路径、单纯形法、高斯消元）、经典游戏逻辑（数独、井字棋、四子棋、Numberle）以及文本/数据处理等 18 个不同难度的实用 C 语言文本到代码基准任务上进行了评测。模型检测后端配置了 CBMC（原生及配备 Bitwuzla SMT 后端）与 ESBMC（Bitwuzla 后端）的并行求解器组合，单断言超时时间设为 60 秒，循环展开界限 \(k=5\)。

基准任务 (Benchmark)	断言总数 (#Assert)	独立验证 (Verified)	条件验证 (C-Verified)	未验证/失败 (Unverified)	LLM耗时 (s)	验证耗时 (s)
bubblesort	10	10	0	0	36.6	2.9
condorcet	25	22	0	3	172.5	253.0
connected_component	21	21	0	0	95.7	127.5
shortest_path	25	24	0	1	143.0	32.8
knapsack	23	15	4	4	125.3	879.3
sudoku	49	43	0	6	164.9	2077.6
tictactoe	85	85	0	0	182.0	21.6
connect4	59	56	0	3	459.3	981.0
numberle	34	32	0	2	345.3	8.6
gaussian_elimination	17	17	0	0	89.8	139.7
simplex	21	21	0	0	234.0	163.2
log_timestamp_filter	20	18	1	1	223.0	9.3
sort_timestamp	34	34	0	0	121.3	24.0
shift_letter	19	19	0	0	104.9	2.4
base_addition	23	9	0	14	44.5	12.6
cellular_automata	17	17	0	0	159.3	206.9
maze	32	31	0	1	65.4	436.2
均值 ± 标准差	30.2 ± 18.6	27.9 ± 19.0	0.3 ± 1.0	1.3 ± 3.4	162.8 ± 108.0	316.4 ± 542.7

用户研究实验（代码理解辅助效果）¶

为了评估验证事实对人类理解代码的实际增益，作者招募了超过 400 名通过资格认证的 MTurk IT 从业人员开展双盲用户测试。研究设计了 10 道针对程序核心性质的四选一单选题，比较无注释基线组（Group A）与带 //FACT: 事实注释组（Group B）的作答准确率与完成耗时。

评估维度 / 任务指标	Group A（无事实注释基线）	Group B（含 Viverra 验证事实）	差异与提升效果
题目作答准确率 (Accuracy)	8/10 题落后于 B 组	8/10 题明显高于 A 组	事实注释使大部分题目准确率显著提升（如连通分量题从 40% 跃升至 100%）
平均回答用时 (Overall Time)	基线参考用时较高	整体耗时普遍缩短	经过验证的断言消除了逆向推理开销，加快审阅决策速度
正确作答者用时 (Correct Users)	4/10 任务用时更短	6/10 任务用时显著更短	在准确理解代码的前提下，注释显著减少认知负荷

关键发现¶

绝大多数断言可独立证明：在平均每任务生成的 30.2 个断言中，高达 27.9 个（占比超过 92%）能够直接被有界模型检测器独立证明，验证了“自然语言协同规范”可生成高度符合程序语义的高质量局部断言。
全局关系型断言构成验证瓶颈：耗时最长与发生超时的任务均集中于涉及全局互异性或全局排序的性质（例如 Sudoku 中的行列宫唯一性检查单项耗时超 2000 秒，背包问题中全数组密度递减检查导致超时），显示出 BMC 求解器在此类全局约束上的可扩展性瓶颈。
认知收益与阅读开销的权衡：用户研究显示，在连通分量遍历顺序这类复杂属性上，注释组虽然因为阅读注释花费了更长时间（96 秒 vs 82 秒），但正确率从 40% 巨幅提升至 100%，表明验证事实对于深层隐式逻辑排错具有决定性辅助价值。

亮点与洞察¶

务实的形式化验证妥协思路：放弃全量数学归纳或定理证明器的完备证明要求，退一步追求 \(k\) 步展开的有界模型检测，既规避了不可判定性又提供了远强于随机测试的状态遍历数学保证。
协同规范（Co-specification）对冲生成幻觉：让大模型在写代码的同时将自然语言需求转化为形式化规格断言，并借助严格求解器充当外部客观评判者，构建了 LLM 软推理与 SMT 硬求解的互补闭环。
调用图驱动的组合式假设降维：将程序调用图转化为断言拓扑依赖序列，自底向上将已证明性质提升为后续断言的假设（\(\mathsf{assume}\)），以极低的代价化解了深层调用状态组合爆炸难题。

局限与展望¶

有界深度的固有不完备性：所有事实均严格限定在预设的展开深度 \(k\)（实验中 \(k=5\)）内成立，无法防范深层越界循环和渐进性质引发的潜在缺陷。
C 语言受限子集的工程局限：目前框架高度依赖验证友好型约束，排除了动态堆内存分配、复杂指针链表以及浮点运算，尚不能直接泛化至包含复杂外部库与异构并发的实际工业级代码。
属性质量受制于 LLM 表现：若大语言模型遗漏了关键业务属性或生成了语义琐碎的弱断言，系统只能保证所生成断言本身的真伪，无法判定代码对完整自然语言需求的规格覆盖率。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次将文本到代码、大模型协同规范与组合式有界模型检测融为一体，开创了轻量验证增强代码理解的新路径。
实验充分度: ⭐⭐⭐⭐☆ 覆盖 18 项非平凡 C 语言基准任务并进行了超过 400 人的真实众包开发者对照研究，验证数据完备详实。
写作质量: ⭐⭐⭐⭐⭐ 形式化理论推导严谨（定理 1 与定理 2 完备证明），系统架构与算法流程交代极为清晰。
价值: ⭐⭐⭐⭐⭐ 为大模型生成代码的安全性与可解释性提供了极具工程落地潜力的实用方案。