# 结合语义等价自博弈与形式化验证提升 LLM 代码推理能力

# 通过形式化验证驱动的语义等价自博弈提升大语言模型的代码推理能力
Source: https://arxiv.org/html/2604.17010 
Poon Tsz Nok School of Informatics University of Edinburgh trevorpoon@gmail\.com &Antonio Valerio Miceli Barone School of Informatics University of Edinburgh antonio@ed\.ac\.uk

###### Abstract
我们提出了一种在 Haskell 中实现语义等价的自博弈框架，利用形式化验证来指导生成器与评估器之间的对抗性训练。该框架结合 Liquid Haskell 证明来验证等价性，并使用基于执行的反例来判断不等价性，整体由难度感知型课程调度进行组织。为此，我们发布了 OpInstruct-HSx，一个包含约 28k 个经过验证的 Haskell 程序的合成数据集。实验表明，我们的评估器能有效迁移至下游任务，在 EquiBench 上准确率最高提升 13.3 个百分点，并在 PySecDB 上保持一致的性能提升。针对 SEQ-SINQ 任务模式的消融研究表明，尽管不等价监督主要用于扩充数据规模，但等价证明才是赋予模型推理能力的唯一关键因素。完整的训练管线与数据集已分别公开发布于 GitHub 和 Hugging Face。

Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification
Poon Tsz NokSchool of InformaticsUniversity of Edinburghtrevorpoon@gmail\.comAntonio Valerio Miceli BaroneSchool of InformaticsUniversity of Edinburghantonio@ed\.ac\.uk

## 1 Introduction
大语言模型（LLM）的兴起彻底改变了软件生成与维护的方式。尽管 Codex 和 Qwen2.5-coder 等模型已展现出从自然语言提示生成可用功能代码的强大能力(Murphyet al.,2024 (https://arxiv.org/html/2604.17010#bib.bib2); Huiet al.,2024 (https://arxiv.org/html/2604.17010#bib.bib1))，但其输出往往难以超越基础测试覆盖率来保证预期的程序行为(Laneveet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib3); Nguyenet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib4); Weiet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib5))。这一差距提出了一个根本性问题：如何设计训练流程，使模型能够显式地推理程序间的语义等价关系？解决此问题不仅对可靠的代码生成至关重要，也对程序优化、自动化重构和漏洞检测等下游应用具有关键意义。

当前方法主要依赖测试套件，这不足以捕捉深层的语义属性和边界情况。为弥补这一差距，我们将框架建立在 Haskell 之上，主要基于以下三个原因。首先，其纯函数式特性与强静态类型系统消除了隐藏状态与副作用(Thompson,2011 (https://arxiv.org/html/2604.17010#bib.bib6))(详见附录A (https://arxiv.org/html/2604.17010#A1)示例)，使得等价推理在数学上具有可操作性(Launchbury,1993 (https://arxiv.org/html/2604.17010#bib.bib12); Sestoft,1997 (https://arxiv.org/html/2604.17010#bib.bib13))。其次，Liquid Haskell 生态系支持通过精化类型生成机器可检查的证明，从而能够对部分 Haskell 程序进行语义等价认证(Liquid Haskell Tutorial,2025 (https://arxiv.org/html/2604.17010#bib.bib11))。这提供了一种在其他如 Python 或 Java 等语言中难以实现的形式化监督信号，因为后者的形式化验证难度要大得多。最后，在对代表性不足的函数式范式进行训练，能推动模型突破标准的面向对象编程模式(van Damet al.,2024 (https://arxiv.org/html/2604.17010#bib.bib15); Giagnorioet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib14))，激发更深层次的抽象能力。

我们提出了一种用于语义等价的自博弈框架，其中包含两个专用智能体的交互：Alice（生成器），负责生成参考程序的变体；Bob（评估器），经过训练以判断两个程序是否等价。自博弈循环交替执行程序生成、通过证明或反例进行验证、难度评分以及双智能体的微调。通过将问题构建为生成器与评估器之间的博弈，该系统能够激励模型面对逐渐递增难度的样本，并深入进行语义推理。

本研究围绕函数式编程在 LLM 对齐中的效用探讨了三个核心问题。首先，我们考察自博弈的动态过程，探究在函数式语言中引入对抗循环是否能引发渐进式课程学习以提升语义推理能力。其次，我们评估跨领域与跨语言的迁移能力，检验在 Haskell 中习得的语义推理技能能否泛化到更广泛的代码基准测试中的零样本合成与漏洞检测任务。最后，我们进行了受控消融实验以确定各类监督信号的相对贡献，区分了形式化等价证明与基于执行的反例对评估器鲁棒性的具体影响。

## 2 Related Work
确定语义等价性在一般情况下极具挑战性，且当前的 LLM 经常无法识别代码中的语义等价关系(Laneveet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib3); Nguyenet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib4); Weiet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib5))。根据莱西定理（Rice's Theorem），判定任意两个程序是否语义等价通常是不可判定的(Rice,1953 (https://arxiv.org/html/2604.17010#bib.bib16))。传统方法依赖单元测试；然而，即使是扩展后的测试套件（如 HumanEval+ 和 MBPP+）仍不足以保证程序正确性(Gren and Antinyan,2017 (https://arxiv.org/html/2604.17010#bib.bib19); Chioteliet al.,2021 (https://arxiv.org/html/2604.17010#bib.bib18))。同样，符号执行提供了路径敏感分析，但随着程序复杂度的增加，会遭遇组合状态空间爆炸的问题(Badihiet al.,2020 (https://arxiv.org/html/2604.17010#bib.bib20))。

为解决这些不完备性问题，近期研究已转向形式化验证。在 LLM 领域，DeepSeek-Prover(Xinet al.,2024a (https://arxiv.org/html/2604.17010#bib.bib21),b (https://arxiv.org/html/2604.17010#bib.bib22); Renet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib23))和 Kimina-Prover(Wanget al.,2025 (https://arxiv.org/html/2604.17010#bib.bib24))等框架已证明，在模型上微调自生成的证明（例如在 Lean 中编写的证明）能显著提升其可验证的推理能力。然而，除了极简单的场景外，为 Python 或 C++ 等命令式语言生成完全机器可检查的等价证明仍是当前工具所无法企及的(Miceli-Baroneet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib25))。我们通过使用 Haskell 与 Liquid Haskell 来弥合这一差距。

Liquid Haskell 将精化类型嵌入编程语言中(Vazouet al.,2014 (https://arxiv.org/html/2604.17010#bib.bib8))，允许通过可满足模理论（SMT）求解器自动验证逻辑属性(Diatchki,2015 (https://arxiv.org/html/2604.17010#bib.bib10); Jhalaet al.,2020 (https://arxiv.org/html/2604.17010#bib.bib26); Liquid Haskell Tutorial,2025 (https://arxiv.org/html/2604.17010#bib.bib11))。该框架利用反射机制与逻辑评估证明（PLE）构建机器可检查的引理，从而形式化地认证候选函数之间的逐点相等性。这为自博弈循环提供了确定性的、高保真的反馈信号。

自博弈历史上曾推动 AlphaZero(Silveret al.,2017 (https://arxiv.org/html/2604.17010#bib.bib27))和 OpenAI Five(OpenAIet al.,2019 (https://arxiv.org/html/2604.17010#bib.bib28))等游戏代理取得突破性进展。在代码领域，Sol-Ver(Linet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib29))和 AutoIF(Donget al.,2025 (https://arxiv.org/html/2604.17010#bib.bib30))等近期框架借鉴了这一思路，利用模型生成的单元测试与执行反馈过滤合成数据，在 MBPP 和 IFEval 等基准测试中取得了显著收益。我们的工作最直接地建立在 Miceli-Barone et al.(2025 (https://arxiv.org/html/2604.17010#bib.bib25))提出的对抗框架之上，即语义不等价游戏（SINQ）。在其设定中，生成器（“Alice”）创建程序变体与分歧输入（反例），而评估器（“Bob”）则尝试在不查看生成器论证的情况下检测不等价性。这种对抗循环提供了一个可扩展的课程体系，有助于提升语义推理能力。我们通过引入语义等价任务（SEQ）对该范式进行了扩展。Miceli-Barone et al.(2025 (https://arxiv.org/html/2604.17010#bib.bib25))的工作仅专注于通过执行反馈处理不等价问题，而我们整合了基于 Liquid Haskell 的形式化验证。这使得我们能够基于带有推理轨迹的等价正样本进行训练。

## 3 Methodology
我们介绍了通过两个互补任务（SEQ 与 SINQ）提升 LLM 代码推理能力的自博弈框架核心方法。在 SEQ 任务中，生成器模型被要求生成给定 Haskell 程序的功能等效变体，并提供证明其等价性的形式化证明。相比之下，SINQ 任务要求生成一个至少在单个输入上与原始程序行为发生偏离的函数。Figure1 (https://arxiv.org/html/2604.17010#S3.F1)展示了完整的自博弈框架，其中基于难度的监督微调引导着自适应训练循环。
Refer to captionFigure 1:通过 Haskell 提升 LLM 代码推理能力的语义自博弈框架概览

### 3.1 Framework Overview
自博弈框架被建模为 Alice（生成器）与 Bob（评估器）之间的两方对抗博弈。
1. 每一轮始于一个参考 Haskell 程序 $P$。Alice 的任务是生成程序 $Q$，它要么是 $P$ 的语义等价变体（附带证明），要么是语义不等价程序（附带展示两者行为差异的分歧输入）。
2. 随后验证该证明或分歧输入，若验证失败，Alice 败北。
3. 接着 Bob 判断 $(P,Q)$ 是否语义等价。若 Bob 判断准确，则 Bob 获胜（Alice 败），反之亦然。Alice 的目标是构造令 Bob 难以分类的实例，而 Bob 的任务是做出正确评估。通过反复交互，双方智能体的性能逐步提升。Miceli-Barone et al.(2025 (https://arxiv.org/html/2604.17010#bib.bib25))已证明，该对抗框架对模型性能的提升没有理论上限，原则上双方在真实代码数据集上训练时，可以无休止地学习复杂的编程逻辑。

### 3.2 Dataset Generation and Preparation
高质量 Haskell 数据集的匮乏局面依然严峻。在众多有限的可用资源中，体量最大的是 Blastwind dataset1 https://huggingface.co/datasets/blastwind/github-code-haskell-file，它聚合了从公开 GitHub 仓库抓取的真实源代码文件。然而，大量噪声严重制约了其可用性：数据中包含未标注、格式不一致且经常无法编译的代码。为应对高质量 Haskell 数据集稀缺的问题，我们采取了一种互补策略：引入 OpInstruct-HSx，即通过改编专为 Python 代码生成构建的大规模高质量指令语料库 nvidia-OpenCodeInstruct 数据集(Ahmadet al.,2025 (https://arxiv.org/html/2604.17010#bib.bib33))，来合成 Haskell 数据集。这些程序首先经过预过滤，随后使用 DeepSeek-R1-Distill-Llama-70B 模型转换为 Haskell 程序。该流程最终生成了一套 Haskell 程序合成数据集。

为确保数据质量，我们引入了自动化过滤与验证阶段。对于每个生成的 Haskell 程序，我们利用句法启发式规则提取函数名及其参数类型，并使用支持常见基本类型（如 Int, Bool, List, Tuple）的递归字面量生成器合成类型正确的输入。每个程序均使用 Glasgow Haskell Compiler (GHC) 进行编译，并在合成输入上执行。仅保留编译成功且执行无误的程序。此过滤流程清除了格式错误或无法运行的代码，确保最终数据集由具备最小运行功能且可执行的 Haskell 程序构成。Figure2 (https://arxiv.org/html/2604.17010#S3.F2)展示了完整的多阶段过滤机制。

我们发布了 OpInstruct-HSx，这是一个适用于 SEQ 与 SINQ 游戏的干净且可执行的 Haskell 数据集，包含约 28,000 个源自实际问题的已验证 Haskell 函数。该数据集已公开发布2 https://huggingface.co/datasets/Trevor0501/OpInstruct-HSx，可作为训练 LLM 进行语义推理任务的高质量合成 Haskell 资源。用于构建数据及复现实验的代码已开源至公共代码仓库3 https://github.com/TrevorPoon/llm-self-play-liquidhaskell。
Refer to captionFigure 2:OpInstruct-HSx 数据集生成的完整流水线

### 3.3 The Self-Play Loop: Alice and Bob
#### Step 1: Program Selection and Branching
设 $\mathcal{D}$ 为参考 Haskell 程序数据集。我们随机选择一个参考程序 $P \in \mathcal{D}$，然后以 50% 的概率选择 SEQ 游戏，否则选择 SINQ 游戏。

#### Step 2a: SEQ Game (Alice’s Turn)
在 SEQ 游戏中，Alice 接收 $P$ 并必须合成 $Q$，使得对所有输入 $x$ 满足：$∀x∈𝒳. P(x)=Q(x)$。为了挑战 Bob，鼓励 Alice 构造高难度实例 $Q$，目标达到最大难度等级（$d=10$，定义于第 3.4.1 节 (https://arxiv.org/html/2604.17010#S3.SS4.SSS1)）。此外，Alice 需提供关于该语义等价性的形式化证明（基于 Liquid Haskell）。参见附录 B (https://arxiv.org/html/2604.17010#A2) 获取 SEQ 实例。

#### Step 2b: SINQ Game (Alice’s Turn)
而在 SINQ 游戏中，Alice 被指示生成至少在一个输入上与 $P$ 发生偏离的函数 $Q$：$∃x^*∈𝒳: P(x^*)≠Q(x^*)$。Alice 同样被激励去构造令 Bob 极易误判的高难度函数 $Q$，目标同样是最大难度等级（$d=10$）。Alice 还必须输出展示该不等价性的分歧输入 $x_a$，满足 $P(x_a)≠Q(x_a)$。参见附录 B (https://arxiv.org/html/2604.17010#A2) 获取 SINQ 实例。

#### Step 3: Verification through Liquid Haskell or Execution
- SEQ Game: Alice 的证明由充当外部预言机的 Liquid Haskell 进行验证。若证明被接受，则该证明将作为微调样本被保留。
- SINQ Game: 候选分歧输入 $x_a$ 将通过执行进行测试：若 $P(x_a)≠Q(x_a)$，则接受该实例；否则丢弃该样本。
所有候选实例均需经过编译、执行与形式化验证检查。这确保了 Alice 与 Bob 的训练数据始终保持高质量且可执行。

#### Step 4: Bob’s Turn – Difficulty Estimation
Alice 生成候选程序 $Q$ 后，Bob 将面临