作者：Anjiang Wei, Tianran Sun, Tarun Suresh, Haoze Wu, Ke Wang, Alex
单位： Stanford University；Shanghai Jiao Tong University；University of Illinois Urbana-Champaign；Amherst College；Nanjing UniversityIntelligence 等
来源： ICLR 2026 Workshop VerifAI-2
时间：2026.04.02
链接：[Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis]
一. 研究背景
程序验证的目标是为软件行为提供形式化保证，尤其适用于自动驾驶、航空航天、工业控制、金融系统等安全关键场景。相比普通测试，程序验证希望证明程序在所有可能输入和执行路径下都满足指定性质，而不是只在有限测试样例上表现正确。
但程序中一旦出现循环结构，验证问题就会显著复杂化。循环可能执行任意次数，带来潜在无限状态空间。为了证明循环程序的正确性，验证器通常需要依赖循环不变量。
所谓循环不变量，是指在循环开始前成立、每次循环迭代后仍然成立，并且在循环退出时能够推出目标断言的逻辑条件。例如，一个变量每次循环都加 7，如果初值为 10，那么 x % 7 == 3 可能就是一个非常关键的不变量。它不仅描述了循环过程中变量的结构性规律，还可以帮助验证器排除某些错误状态。
不过，生成循环不变量并不容易。一个不变量仅仅正确还不够，还必须足够强。例如 x > 0 可能始终成立，但它无法帮助证明 x != 700；而 x % 7 == 3 不仅正确，还能直接排除 x == 700，因此更有实际证明价值。
本文关注的问题是：LLM 是否能够通过生成有用的循环不变量来加速程序验证？进一步说，如何把 LLM 的代码理解和逻辑推理能力转化为可信的程序验证能力？
二. 论文概要
论文围绕 LLM-based invariant synthesis 展开，提出 Quokka 作为一个面向评估的 LLM 不变量生成框架。本文的核心贡献主要包括四点：
- Quokka 框架：LLM 负责生成候选循环不变量，验证器直接判断该不变量的 correctness 与 utility，避免复杂后处理。
- Sound evaluation：通过两个验证器查询判断候选不变量是否成立，以及加入该不变量后目标断言是否可证明，并给出 soundness 证明。
- Benchmark 与模型评测：从 SV-COMP 构建 866 个程序验证实例，评估 9 个不同模型家族的大语言模型，比较正确不变量数量、额外解决实例数与平均求解时间。
- 能力增强策略：构造 3589 个训练实例，验证 supervised fine-tuning 和 Best-of-N sampling 都能带来可测量提升。
本文与之前工作的最大不同在于，它直接把 LLM 输出作为待验证的证明候选。Quokka 并不信任 LLM 的自然语言推理结果，而是把 LLM 放在生成候选命题的位置，再由形式化验证器完成可靠性判断。
这与食品推理任务非常相似：LLM 可以提出某类配料占比应满足某个约束、某类食品的营养贡献应符合某种规律等候选命题，但这些命题不能直接入库，必须经过约束求解、误差评估和冲突检测。
三. 核心思想
本文的核心思想可以概括为：LLM 是候选逻辑命题生成器；验证器是可信评价器。
传统 LLM-based verifier 往往采用复杂的“生成—过滤—重组—修复”策略。比如让 LLM 先生成一批谓词，再用模型检查器过滤无效谓词，之后通过合取、析取、Houdini pruning 或回溯算法拼接出最终不变量。这类方法的潜台词是：LLM 输出是不可靠的，需要复杂算法不断补救。
Quokka 的思路更直接：如果 LLM 生成了一个候选不变量，那么就直接交给验证器判断它是否成立、是否有用。若它正确且能帮助证明目标断言，就保留其贡献；若它不正确或无用，就丢弃或判为 inconclusive。
这体现了一个很重要的系统设计思想：不要让 LLM 直接给出最终可信结论，而要让 LLM 生成候选结构，再用可验证机制筛选。
在程序验证中，这个候选结构是不变量；在食品标签推理中，这个候选结构可以是配料比例约束、营养贡献约束、类别先验约束、价格合理性约束或法规合规约束。
因此，Quokka 的价值不只是程序验证本身，而是提供了一种“LLM + 形式化验证器”的通用协同范式。
四. 方法设计
4.1 循环不变量的形式化定义
论文首先用 Hoare Logic 描述循环不变量的作用。
对于一个循环：
while B do S
其中 P 是前置条件，Q 是后置条件，B 是循环条件，S 是循环体。要证明程序从 P 出发执行循环后满足 Q，就需要找到一个循环不变量 I，使其满足三个条件：
- 初始化条件：P ⇒ I
即进入循环前，不变量 I 已经成立。 - 保持性条件：{I ∧ B} S {I}
即如果循环开始时 I 成立，并且循环条件 B 为真，那么执行一次循环体 S 后，I 仍然成立。 - 充分性条件：I ∧ ¬B ⇒ Q
即当循环结束时，如果 I 成立且循环条件不再满足，那么可以推出目标后置条件 Q。
只有同时满足这三个条件，I 才能作为证明循环正确性的归纳式逻辑桥梁。
这里需要注意的是：正确不变量不一定有用。
例如，对于某个程序而言，x > 0 可能确实始终成立，但它可能无法帮助证明最终断言。而 x % 7 == 3 这样的不变量虽然更具体，却能显著缩小状态空间，直接帮助验证器排除错误状态。
因此，Quokka 的评价标准不是“LLM 是否生成了正确不变量”，而是进一步追问：
这个不变量是否强到足以加速目标性质的证明？
4.2 Verifier-Based Approach：两个验证器查询
Quokka 的核心方法是对每个候选不变量执行两个验证器查询。
给定：
P：原始程序
p*：待验证的目标性质
q：LLM 生成的候选不变量
第一个查询是：
da = V(P, ∅, q)
它的作用是验证 q 是否真的是程序 P 中成立的不变量。也就是说，q 本身必须先被证明为正确。
第二个查询是：
db = V(P, {q}, p*)
它的作用是在假设 q 成立的情况下，验证目标性质 p* 是否可以被证明。也就是说，q 不仅要正确，还要对最终证明有帮助。
如果 q 被证明成立，并且加入 q 后目标性质也被证明，那么 Quokka 输出 T，表示证明成功。
如果在 q 的假设下仍然能发现目标性质的反例，那么输出 F，表示目标性质被反驳。
如果验证器无法证明 q，或者加入 q 后仍无法证明目标性质，则输出 U，表示结果不确定。
这一机制的关键在于：LLM 输出不会被直接当成事实，而是被当成待验证的证明候选。系统的 soundness 来自验证器，而不是来自 LLM。
4.3 语法检查与并行验证
在真正调用验证器前，Quokka 会先做语法合法性检查。因为 LLM 可能生成非法表达式，甚至生成会改变程序状态的语句，例如 a += 1、x++、赋值表达式等。
Quokka 只接受不会改变程序状态的布尔条件作为候选不变量。这一步可以避免把非逻辑谓词错误地插入程序中，导致验证结果失真。
在实现上，Quokka 对每个候选不变量并行执行两个验证器查询。这样可以降低整体等待时间，也方便测量加入候选不变量后是否真正带来加速。
这点对我们的研究也有启发：食品命题库中的候选命题也应先经过语法与语义检查。例如：
“白砂糖占比小于 10%”是一个可验证命题；
“这个产品比较健康”则不是一个直接可求解的约束；
“蛋白质主要来自乳源成分”需要进一步转成营养贡献比例约束，才能进入求解器。
4.4 SFT 与 Best-of-N Sampling
除了直接评估不同 LLM 的不变量生成能力，论文还研究了两种能力增强策略。
第一种是 supervised fine-tuning。作者使用 GPT-4o 生成合成 C 程序，再通过 UAutomizer 过滤无效样本并抽取真实不变量，最终得到 3589 个训练实例。随后，作者对 Qwen2.5-7B 进行 LoRA 微调。
实验结果显示，微调带来了一定提升，但幅度并不大。正确不变量数量从 419 提升到 431，60s timeout 下额外解决实例从 5 个提升到 7 个。这说明领域微调确实有帮助，但仅靠监督微调还不足以解决深层程序归纳推理问题。
第二种是 Best-of-N Sampling。它的思路是让 LLM 一次生成多个候选不变量，然后由验证器选择带来最大验证加速的候选。实验显示，当 N 从 1 增加到 4 时，性能明显提升；继续增加到 N=8 时效果最好；超过 N=8 后，由于资源竞争和内存限制，收益趋于平台。
这一点非常适合迁移到食品命题库场景。我们也可以让 LLM 一次生成多个候选食品推理命题，然后通过约束求解器判断哪条命题最能降低反演误差、缩小解空间、提升评分稳定性。最终不是让模型自己决定哪条规则好，而是让任务反馈决定哪条规则入库。
五. 实验设计
本文的评测数据来自 SV-COMP 2025。作者筛选出包含 while 或 for 循环的程序验证任务，构建了 866 个评测实例。相比已有 LLM-based verifier 的数据集，Quokka 的 benchmark 更复杂：程序平均行数更长，并且包含多循环、多函数、数组和指针等结构。这些特征在真实程序验证中非常重要，也更能区分不同模型的能力。
基础验证器方面，论文使用 UAutomizer 作为 base solver。比较两种情况：
- 不使用 LLM 候选不变量时，UAutomizer 原本需要多少时间；
- 使用 LLM 生成的不变量后，验证是否更快，是否能解决更多实例。
评价指标包括：
- 正确不变量数量；
- 额外解决实例数；
- 总解决实例数；
- 平均求解时间。
特别注意的是，论文统计的是端到端时间，也就是包含 LLM 推理开销。这让结果更接近真实系统部署场景，而不是只看验证器内部时间。
5.1 不同 LLM 的表现差异
论文评估了 9 个 LLM，结果显示模型之间差异非常明显。整体趋势是：模型越强，生成正确且有用不变量的能力越强。
从 Llama-3.1-8B 到 gpt-5.2，正确不变量数量从 342 提升到 710，平均求解时间也明显下降。
在 60s timeout 下，gpt-5.2 额外解决了 21 个 UAutomizer baseline 无法解决的实例。
但在 500s timeout 下，额外收益显著下降，说明 LLM 对中等难度任务有明显加速作用，但面对最难验证任务时，仍难以生成足够强的不变量。
这说明 Quokka 是一个能够区分模型逻辑推理能力的 benchmark。它既能展示当前 LLM 的实际价值，也暴露出模型在深层程序归纳推理上的能力上限。
5.2 失败模式分析
论文进一步分析了失败案例。一个重要发现是：很多失败并不是因为 LLM 生成的不变量完全错误，而是因为不变量太弱或者验证过程超时。
部分 LLM 生成的不变量与原始断言几乎相同，缺乏分解作用。也就是说，它没有真正帮助验证器把复杂证明任务拆成更容易处理的子问题。
还有一些不变量只是简单边界条件，虽然可能正确，但无法捕捉循环的核心行为。例如，只给出变量上下界，却没有描述变量之间的关系、模运算结构或归纳式规律。
这对我们的研究很有启发：食品推理中的候选命题也不能只追求“看起来正确”，还要看它是否真正提供推理增益。例如：
“配料总和为 100%”是正确的，但可能过于基础；
“香精、防腐剂、色素总占比通常低于 1%”更有助于压缩解空间；
“乳制品中蛋白质主要来自乳源配料”可能对乳制品反演贡献更大。
命题的价值不只在于 correctness，更在于 utility。
5.3 SFT 与 Best-of-N 的效果
监督微调能带来温和提升，但并没有产生质变。这说明 LLM 对不变量生成的困难不只是格式问题，也涉及真正的程序语义理解和归纳推理。
相比之下，Best-of-N Sampling 的提升更明显。原因在于它把问题从“生成一个绝对正确的答案”变成“生成多个候选，再由验证器选择最优候选”。这是一种非常适合 LLM 的协同方式：模型负责扩大候选空间，验证器负责筛选。
这种机制对自迭代命题库尤其重要。因为在食品标签反演任务中，我们很难一次生成完全正确且最有用的规则。更合理的方式是生成多个候选命题，再通过实际反演效果来筛选：
候选命题 q1：配料顺序满足非增约束；
候选命题 q2：添加剂类配料总占比小于阈值；
候选命题 q3：饮料类食品中水分占比高于阈值；
候选命题 q4：乳源配料贡献主要蛋白质来源；
候选命题 q5：高钠食品中盐类配料贡献主要钠来源。
最终由约束求解器判断哪条命题真正降低营养误差，哪条命题会造成冲突，哪条命题应进入命题库。
5.4 与已有 LLM-based Verifier 的比较
论文将 Quokka 与 LaM4Inv、Clause2Inv、Loopy、LEMUR 等方法进行比较。不同于这些方法中的复杂过滤、组合、修复和回溯机制，Quokka 采用更直接的验证器评价接口。实验结果显示，Quokka-gpt-5.2 best-of-8 在多个 timeout 阈值下取得最强表现。在 LEMUR benchmark 上，UAutomizer 在十分钟内无法解决任何实例，而 Quokka 仍能解决更多任务，并保持更低平均求解时间。
当 LLM 能力增强时，复杂后处理未必总是必要。更重要的是建立一个干净、可靠、可复核的接口：让 LLM 给出候选命题，让验证器判断它是否正确、是否有推理贡献。
从实验结果来看，本文系统证明了 LLM 在循环不变量生成中具有实际价值，但这种价值并不是无限的。
性能上，Quokka-gpt-5.2 在正确不变量数量、额外解决实例和平均求解时间上整体领先，Best-of-N 进一步提升表现。
功能上，Quokka 把 LLM 定位为候选命题生成器，把验证器定位为可信评估器，实现了 LLM 推理能力与形式化验证机制的协同。
但论文也暴露出一些局限：
- 多数失败并非不变量完全错误，而是超时或不变量过弱。
这说明生成“正确但无用”的命题仍然是 LLM 的常见问题。 - SFT 提升有限。
简单监督微调不足以解决深层归纳推理问题，未来可能需要更强的搜索、反馈学习或 verifier-in-the-loop 训练机制。 - Soundness 依赖验证器。
LLM 本身并不提供可靠性保证，系统最终可信性来自 UAutomizer 等形式化验证器。 - 任务仍集中在程序验证。
Quokka 的方法论具有迁移价值，但若迁移到食品、医学、法律等弱形式化领域，需要重新设计“验证器”的定义。
六. 对齐思考
- 在食品配料反演中，可以让 LLM 根据配料表、营养成分表、价格、食品类别、营养数据库和法规知识生成候选命题。例如：
配料顺序约束：排在前面的配料占比不低于后面的配料；
营养贡献约束：产品营养值约等于各配料营养贡献的加权和；
类别先验约束：饮料类食品中水分占比较高，香精和色素占比较低；
价格合理性约束：理论原料成本与市场售价之间存在合理区间；
法规合规约束：某些营养声称、配料标识、添加剂使用需要满足标准要求。
但这些命题不能直接入库，而要像 Quokka 一样接受验证。系统可以设计两个问题：
第一，候选命题是否与已有标签数据、营养数据库和法规知识一致？
第二，加入该命题后，配料比例反演误差是否下降，解空间是否缩小，评分结果是否更稳定？
只有同时具备合理性和推理贡献的命题，才应进入命题库。
- 食品标签数据具有天然的不完整性和噪声。包装食品通常只提供有限营养项，例如能量、蛋白质、脂肪、碳水化合物、钠，而不提供完整配料比例、微量营养素、添加糖、脂肪酸结构等信息。
因此，任务本质上是一个弱信息条件下的反演问题：
已知配料顺序、营养成分表、价格和净含量；
未知各配料真实占比、各营养素贡献来源、理论原料价值和综合性价比。
- Quokka 的思想可以映射为一条完整推理链：品类识别 → 候选命题生成 → 约束反演 → 营养贡献分析 → 价格价值评分 → 解释输出。
首先，系统识别食品品类。例如酸奶、饮料、饼干、坚果棒、预制菜等不同类别，应使用不同的先验命题和约束模板。系统根据品类生成候选命题。例如乳制品更关注乳源蛋白贡献，饮料更关注水分、糖和甜味剂，饼干糕点更关注油脂、糖和精制碳水，坚果棒更关注坚果真实含量和蛋白质密度。
然后，系统通过约束优化器反推配料比例和营养贡献。不是简单看配料表顺序，也不是直接相信模型估计，而是利用营养成分表作为可检验目标。
最后，系统将反演结果用于评分。评分不只看每 100g 的基础营养成分，还可以结合配料质量、蛋白质密度、添加糖风险、钠含量、理论原料价值、单位价格等指标，输出食品性价比判断。
如果某条命题频繁降低误差，就提高其权重；如果某条命题经常导致约束不可满足或解释冲突，就降低权重或淘汰。这样就能形成一个类似 Quokka 的自迭代闭环：
候选命题生成 → 约束验证 → 效果评估 → 命题入库 → 权重更新 → 下一轮推理。