💻 computer science

Can Large Language Models Model Programs Formally?

该论文提出了名为 Model-Bench 的基准测试及配套流程，旨在评估并提升大语言模型将 Python 程序转化为可验证模型检查规范的能力，实验结果表明当前大语言模型在此任务上仍存在显著局限。

原作者： Zhiyong Chen, Jialun Cao, Jiarong Wu, Chang Xu, Shing-Chi Cheung

发布于 2026-04-03

📖 1 分钟阅读☕ 轻松阅读

原作者： Zhiyong Chen, Jialun Cao, Jiarong Wu, Chang Xu, Shing-Chi Cheung

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文就像是在给人工智能（AI）老师出的一道“翻译题”，但这次翻译的不是人类语言，而是把电脑程序翻译成一种极其严谨的“数学说明书”。

为了让你轻松理解，我们可以把整个过程想象成**“把乐高积木城堡变成严谨的建筑设计图”**。

1. 背景：为什么我们需要做这件事？

现状：现在的软件（比如手机 App、银行系统）越来越复杂。以前我们靠“测试”来找 bug，就像是在盖好的房子里到处敲敲墙壁，看看有没有裂缝。但这有个大问题：测试只能证明“这里坏了”，不能证明“这里绝对没坏”。
目标：我们需要一种叫**“形式化验证”的技术。这就像是要求建筑师在盖房前，必须拿出一份100% 无懈可击的数学证明**，保证房子在任何情况下都不会塌。
难点：这种证明通常有两种写法。一种是“定理证明”（像写数学论文，很难），另一种是“模型检测”（像画状态流程图，把程序的所有可能运行路径都画出来）。
- 问题在于：让 AI 自动把复杂的 Python 代码（乐高城堡）变成这种严谨的流程图（设计图），非常困难。以前的 AI 要么画错了，要么画得太乱，机器没法检查。

2. 核心工作：Model-Bench（模型考场）

作者们觉得：“既然没人好好研究怎么让 AI 做这个翻译，那我们就自己建个考场吧！”

Model-Bench 是什么？
它是一个专门的测试题库。
- 题目：从 3 个著名的编程题库（HumanEval, MBPP, LiveCodeBench）里挑了 400 道 Python 编程题。
- 任务：让大语言模型（LLM）把这些 Python 代码，翻译成一种叫 TLA+ 的语言。
- TLA+ 是什么？ 你可以把它想象成**“程序的通用数学语言”**。它不关心代码写得漂不漂亮，只关心逻辑对不对。
- 考官：有一个叫 TLC 的自动检查器，它会拿着 AI 生成的 TLA+ 图纸，去和原始代码对比，看看逻辑是否一致。

3. 他们做了什么实验？

作者们找了各种大模型（比如 DeepSeek, Qwen, Llama 等），让它们做这个翻译任务，并观察了三个关键点：

A. 直接翻译 vs. 先“预处理”再翻译

直接翻译（零样本/少样本）：直接把 Python 代码扔给 AI，让它写 TLA+。
- 结果：AI 经常“翻车”。生成的图纸要么机器读不懂（语法错），要么逻辑跑不通。
代码转换（预处理）：作者发现 Python 代码太灵活了（比如递归、复杂的列表），而 TLA+ 喜欢简单、像状态机一样的结构。
- 做法：他们先写了一个“转换器”，把 Python 代码强行改写成一种更简单、更像流程图的样子（把复杂的循环变成简单的步骤跳转），然后再让 AI 去翻译。
- 比喻：就像让 AI 翻译古文。直接让它翻很难，但如果先把古文改成大白话，再让它翻成数学公式，准确率就高多了。
- 结果：虽然生成的图纸数量稍微少了一点点，但图纸的质量（相似度）大幅提升。

B. AI 的表现如何？

好消息：最强的模型（如 DeepSeek-V3）在给了几个例子（Few-shot）后，能成功生成约 66% 能通过检查的图纸。
坏消息：剩下的 34% 还是挂了。而且，如果代码太复杂（比如循环套循环、变量太多），AI 就更容易犯错。
有趣发现：代码越“难”（算法逻辑复杂），AI 不一定翻得越差；反而是代码结构越乱、嵌套越深，AI 越容易晕头转向。

C. AI 常犯什么错？

作者分析了那些“不及格”的作业，发现 AI 主要犯三类错：

生造词（编译错误）：Python 里有 sort 函数，但 TLA+ 里没有，AI 却直接照搬，导致机器报错。
记性不好（运行时错误）：Python 数组从 0 开始数，TLA+ 从 1 开始数。AI 经常搞混，导致“数组越界”。
太死板（断言错误）：有时候 AI 为了“忠实”于原代码，反而漏掉了关键逻辑（比如漏了一个函数调用），或者把变量搞错了。

4. 总结与启示

这篇论文的核心结论可以用三个比喻来概括：

AI 是个天才，但也是个“细节控”：它很擅长模仿和识别模式，但在处理两种完全不同逻辑体系（灵活的 Python vs. 严谨的 TLA+）的转换时，容易在细节上栽跟头。
“先整理，再翻译”是王道：与其指望 AI 直接搞定高难度翻译，不如先帮它把“原材料”（代码）整理成它更容易理解的格式（代码转换），效果会好很多。
路还很长：虽然 AI 能完成约一半的任务，但离“全自动、零错误”的工业级应用还有距离。特别是对于复杂的、嵌套深的程序，AI 还需要更强的逻辑推理能力。

一句话总结：
这篇论文建立了一个**“程序翻译考场”，发现让 AI 把 Python 代码变成严谨的数学证明（TLA+）目前还很难**，但如果我们先把代码“简化”一下再让 AI 去翻，效果会好很多。这为未来让 AI 自动保证软件安全（比如自动驾驶、医疗设备不出错）指明了方向。

这是一份关于论文《Can Large Language Models Model Programs Formally?》（大语言模型能否形式化地建模程序？）的详细技术总结。

1. 研究背景与问题 (Problem)

核心挑战：在数字时代，软件的正确性、安全性和可靠性至关重要。形式化验证（Formal Verification）是确保软件质量的关键手段，主要分为定理证明（Theorem Proving）和模型检测（Model Checking）。
现有差距：近年来，大语言模型（LLM）在辅助定理证明方面取得了显著进展（如自动形式化、证明生成）。然而，模型检测领域进展缓慢，主要瓶颈在于自动程序建模（Automatic Program Modeling）的困难。
具体难点：
- 从代码（特别是动态语言如 Python）自动推导出准确且可处理的行为模型非常困难。
- Python 具有复杂的运行时行为（如可变别名、高阶函数、异步/await、第三方库），需要将其抽象为有限但忠实的状态空间。
- 模型需要在“具体性”和“抽象性”之间取得平衡：太具体会导致模型检测器无法扩展（状态爆炸），太抽象则会导致属性空洞或不可靠。
研究目标：填补这一空白，评估并提升 LLM 将 Python 程序转换为可验证的模型检测规范（TLA+）的能力。

2. 方法论 (Methodology)

为了评估和改进 LLM 的程序建模能力，作者提出了 Model-Bench 基准测试及其配套流水线。

2.1 基准构建 (Benchmark Construction)

数据来源：从三个著名的 Python 代码生成基准（HumanEval, MBPP, LiveCodeBench）中选取了 400 个 Python 程序。
数据处理流程：
1. 去重与标准化：提取原始代码和测试用例，合并为独立的 Python 文件。
2. 简化与重写：
  - 库过滤：仅保留 typing 和 math 库，移除其他复杂依赖。
  - 语言特性处理：针对多重函数声明、递归、列表推导、切片、类、Lambda 表达式等，利用 LLM 将其重写为更简单的等价形式，以适配 TLA+ 的建模能力。
  - 类型过滤：排除涉及复杂类型的变量，仅保留基础类型（None, Number, String 及其派生结构）。
  - 执行验证：确保处理后的代码能通过原始测试用例。
提示工程 (Prompting)：设计了三种提示变体：
1. 原始代码 + 2 个示例（Few-shot）。
2. 原始代码（Zero-shot）。
3. 转换后的代码 + 2 个示例（Few-shot）。

2.2 代码转换技术 (Code Transformation)

为了解决 Python 与 TLA+ 执行模型的差异（TLA+ 基于状态机，Python 基于控制流），作者提出了一种代码转换方法：

控制流图 (CFG) 构建：将 Python 程序转换为 CFG。
状态机模式重写：
- 引入 pc (program counter) 变量跟踪当前状态。
- 将所有变量在开头声明。
- 将代码重写为包含 while 循环和 if 语句的结构，通过 pc 控制跳转，模拟 TLA+ 的动作（Actions）。
- 将 Python 字符串转换为 ASCII 码数组（因为 TLA+ 中字符串是不可变的）。
目的：使输入代码的结构更接近 TLA+ 模型，降低 LLM 的推理难度。

2.3 评估指标 (Evaluation Metrics)

使用模型检测器 TLC 进行验证，并定义了两个核心指标：

Runnable@k：在生成的 $k$ 个模型中，至少有一个能通过 TLC 检查（无编译或运行时错误）的比例。
状态相似度 (State Similarity)：衡量生成模型与人工构建的“真值模型”（Oracle Model）在状态空间上的重合度。
- 定义：生成模型的状态集合与真值模型状态集合的交集比例。
- 阈值：设定为 1.0，要求生成模型的所有变量值对必须存在于真值模型中，且允许生成模型包含额外的辅助变量（如 pc）。

3. 主要贡献 (Key Contributions)

Model-Bench 基准：首个专注于从源代码自动生成模型检测规范（TLA+）的 LLM 基准测试，包含 400 个经过严格筛选和转换的 Python 程序及 1639 个测试用例。
代码转换方法：提出了一种将 Python 代码转换为类状态机形式（State Machine Pattern）的方法，显著提升了 LLM 生成模型的语义相似度。
全面评估与发现：通过大量实验揭示了 LLM 在形式化建模方面的局限性，并分析了代码复杂度、提示策略对性能的影响。

4. 实验结果 (Results)

实验在多个 LLM（包括 DeepSeek-V3, Qwen3, Llama, Gemma 等）上进行，主要发现如下：

整体性能 (RQ1)：
- LLM 在自动建模任务上表现有限。表现最好的模型 DeepSeek-V3 在 Few-shot 设置下的 Runnable@1 仅为 51.75%，状态相似度为 49.55%。
- Few-shot 学习至关重要：相比 Zero-shot，Few-shot 提示使 Runnable@1 平均提升了 17.57%，相似度提升了 31.44%。部分小模型在 Zero-shot 下几乎无法生成可运行模型（接近 0%），但在 Few-shot 下有了显著突破。
- 模型能力差异巨大：高性能模型（DeepSeek-V3）与低性能模型（Llama-3.1-8B）之间存在显著差距。
代码转换的有效性 (RQ2)：
- 权衡效应：使用转换后的代码（Transformed Code）虽然导致 Runnable@k 略有下降（因为代码变长导致“迷失在中间”现象，且减少了 LLM 完全重写程序的机会），但显著提高了状态相似度（例如 DeepSeek-V3 的相似度从 49.55% 提升至 68.54%）。
- 互补性：原始代码提示和转换代码提示生成的可运行模型集合具有互补性，结合两者可以覆盖更多可运行的模型。
代码复杂度的影响 (RQ3)：
- 负相关性：Python 代码的语法复杂度（如圈复杂度、最大循环深度、变量数量）与 LLM 的建模成功率（Runnable@k）和相似度呈负相关。
- 算法难度无关：建模难度与算法本身的逻辑难度（如 LiveCodeBench 的难度评级）相关性不强，主要取决于代码结构的复杂性（如嵌套循环和数据结构）。
错误分析 (RQ4)：
- 编译错误：主要源于 LLM 对 TLA+ 内置操作符（如 Sort）不熟悉，或混淆了 Python 和 TLA+ 的库。
- 运行时错误：源于语言特性差异，最典型的是数组索引问题（Python 从 0 开始，TLA+ 从 1 开始），LLM 常在此处出错。
- 断言错误：源于对源代码的过度忠实（Over-fidelity），例如遗漏了 Python 中的 .lower() 调用，或者错误地使用常量代替动态长度（如 Len(arr)）。

5. 意义与展望 (Significance)

推动形式化验证：Model-Bench 为评估 LLM 在模型检测领域的潜力提供了标准，填补了从代码到形式化规范自动生成的研究空白。
指导未来方向：
- 表明当前的 LLM 在复杂程序的形式化建模上仍存在显著局限，特别是在处理语言差异和复杂控制流时。
- 证明了代码转换（将代码重构为更接近目标语言范式的形式）是一种有效的辅助手段，能显著提升生成模型的语义准确性。
- 未来的 LLM 需要更强的推理能力，以处理语言间的语义鸿沟（如索引差异、类型系统差异）和长上下文的保持能力。
工业应用潜力：虽然目前成功率有限，但通过结合 Few-shot 学习和代码转换，LLM 有望成为辅助软件工程师进行形式化验证的实用工具，特别是在关键基础设施的安全保障中。

总结：该论文通过构建 Model-Bench，系统性地评估了 LLM 将 Python 代码转换为 TLA+ 模型的能力。研究发现，虽然 LLM 目前尚不能完全可靠地自动完成此任务，但通过 Few-shot 学习和特定的代码转换策略，可以显著提升生成模型的质量。这为未来利用 LLM 加速形式化验证流程指明了方向。