Towards Autoformalization of LLM-generated Outputs for Requirement Verification

基本信息

• 论文ID: 2511.11829
• 标题: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• 作者: Mihir Gupte, Ramesh S. (General Motors)
• 分类: cs.CL, cs.AI, cs.FL, cs.LO
• 发表时间: November 18, 2025 (arXiv预印本)
• 论文链接: https://arxiv.org/abs/2511.11829

摘要

本文探索了使用自动形式化（Autoformalization）技术来验证大型语言模型（LLM）生成输出的可行性。随着LLM在将自然语言需求转换为结构化输出（如Gherkin场景）方面展现出潜力，如何形式化验证这些输出的准确性成为关键问题。研究团队进行了两组实验：第一组成功识别了两个不同措辞的自然语言需求在逻辑上等价；第二组识别出LLM生成输出与原始需求之间的逻辑不一致。虽然研究范围有限，但结果表明自动形式化在确保LLM生成输出的保真度和逻辑一致性方面具有显著潜力。

研究背景与动机

1. 核心问题

随着LLM应用的普及，特别是在自动生成测试场景等工程任务中，存在一个关键挑战：缺乏形式化方法来验证LLM生成的输出是否准确反映了原始的自然语言需求。例如，从"当车速≥10且安全带未系时，启动安全带提醒"这样的需求生成Gherkin场景后，无法确保生成内容的逻辑正确性。

2. 问题重要性

在汽车工程等安全关键领域，需求验证至关重要。错误的需求转换可能导致：

• 测试用例不完整或错误
• 系统行为与预期不符
• 潜在的安全隐患

3. 现有方法局限性

• 传统形式化方法：主要应用于数学定理证明，缺乏针对工程需求验证的应用
• LLM评估方法：依赖人工检查或启发式方法，缺乏严格的逻辑验证
• 自动形式化研究：主要关注数据集构建和模型训练，较少关注实际工程应用

4. 研究动机

本文提出将自动形式化技术应用于验证LLM输出这一新场景，通过将自然语言需求和LLM生成输出都转换为形式逻辑表示（Lean 4），利用定理证明器验证逻辑等价性。

核心贡献

1. 提出了首个针对LLM生成输出验证的自动形式化管道：将自然语言需求和LLM输出转换为Lean 4形式化表示，并通过双条件等价证明验证逻辑一致性
2. 验证了两个具体应用场景：
   • 识别不同措辞的自然语言需求的逻辑等价性
   • 检测LLM生成输出与原始需求的逻辑不一致
3. 识别了关键技术挑战：
   • 变量接地（variable grounding）的必要性和自动化难题
   • LLM非确定性对形式化的影响
   • 自然语言歧义性的处理
4. 提出了未来研究方向：为构建可靠的LLM输出验证框架奠定基础

方法详解

任务定义

输入：

• 一对需要验证逻辑关系的陈述（S₁, S₂），可以是：
  • 两个自然语言需求
  • 一个自然语言需求和一个LLM生成的Gherkin场景

输出：

• 逻辑等价性判断：等价（可证明 S₁ ↔ S₂）或不等价（证明失败）

约束条件：

• 陈述必须可形式化为命题逻辑
• 需要系统上下文信息进行变量接地

模型架构

整体管道包含四个关键步骤（如图9所示）：

步骤1：自动形式化

使用**DeepSeek-Prover-v2（7B模型）**将自然语言陈述转换为Lean 4命题：

-- 示例：需求R1的形式化
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

提示模板（见附录A.1）：

• 明确要求生成Lean 4的def语句
• 指定使用命题逻辑（Prop类型）
• 要求将条件表示为蕴含关系（A ∧ B → C）

步骤2：变量接地（Variable Grounding）

当前实现：手动识别并统一不同形式化中指向相同概念的变量

问题示例：

• R1中的vehicle_speed_avg和R2中的mean_vehicle_speed指向同一物理量
• 需要明确告知Lean编译器这种等价关系

-- 手动接地示例
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

步骤3：双条件等价定理构造

构造形式化定理以验证逻辑等价性：

theorem req1_eq_req2 
  (h_grounding : <变量接地假设>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <证明过程>

步骤4：自动定理证明

再次使用DeepSeek-Prover-v2生成Lean证明代码：

• 成功证明 → 两个陈述逻辑等价
• 证明失败 → 存在逻辑不一致

技术创新点

1. 跨领域应用创新：首次将数学定理证明领域的自动形式化技术应用于软件工程需求验证
2. 双层LLM使用：
   • 第一层：形式化翻译（NL → Lean）
   • 第二层：定理证明（验证等价性）
3. 基于失败的验证机制：利用定理证明器的失败作为逻辑不一致的指示器，这是一种创新的负面验证方法
4. 变量接地识别：明确提出变量接地是自动形式化管道中不可或缺的步骤，这在以往研究中未被充分强调

实验设置

数据集

实验1：需求等价性验证

• R1: "If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime"
• R2: "If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt"

实验2：LLM输出验证

• R3: "When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE."
• G3: LLM生成的Gherkin场景（包含4个示例行，引入了额外变量如seat_occupancy）

评价指标

定性指标：

• Lean 4编译成功/失败
• 定理证明成功/失败

验证标准：

• 逻辑等价：定理PA ↔ PB可证明
• 逻辑不一致：定理证明失败或Lean代码无法编译

实现细节

模型选择：

• DeepSeek-Prover-v2 (7B)
• 选择原因：
  1. 在Lean 4上训练
  2. 具备自然语言理解能力
  3. 采用子目标分解策略

形式化语言：Lean 4

• 强大的定理证明能力
• 精确的逻辑表达
• 与DeepSeek-Prover-v2兼容

手动干预：

• 变量接地步骤完全手动
• 形式化输出的验证依赖Lean编译器

实验结果

主要结果

实验1：需求等价性验证（成功案例）

形式化输出：

• R1和R2被成功转换为Lean命题（图3、图4）
• 变量映射被手动建立：
  • vehicle_speed_avg ≡ mean_vehicle_speed
  • seatbelt_active ≡ seatbelt_plugged_in

验证结果（图5）：

• ✅ Lean编译成功
• ✅ 定理req1_eq_req2证明成功
• 结论：R1和R2逻辑等价

意义：证明了管道可以识别语义相同但措辞不同的需求，有助于需求一致性检查。

实验2：LLM输出验证（失败案例）

形式化输出：

• R3：简单命题，仅包含安全带状态变化条件（图6）
• G3：复杂命题，包含额外变量（seat_occupancy, initial_seatbelt_status）（图7）

关键发现：

• G3引入了R3中未提及的变量
• 逻辑结构更复杂（包含4个场景示例）

验证结果（图8）：

• ❌ Lean代码编译失败或证明失败
• 结论：G3与R3逻辑不一致

意义：成功检测到LLM生成输出的"过度生成"问题——添加了原始需求中不存在的约束条件。

案例分析

案例：歧义性问题（R4）

需求：

"When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE."

问题："vehicle in motion"的形式化存在歧义

两种可能的形式化（图10）：

1. pass@1: 布尔变量 vehicle_in_motion : Bool
2. pass@2: 数值变量 vehicle_speed > 0

分析：

• 两种形式化在系统语义上可能都正确
• 但它们在形式逻辑上不等价（不同类型）
• 突显了自然语言歧义性对形式化的影响

实验发现

1. 形式化依赖可解释性：LLM的非确定性导致同一需求可能产生不同但都"合理"的形式化表示
2. 变量接地是瓶颈：
   • 最耗时的步骤
   • 需要系统领域知识
   • 目前只能手动完成
3. 系统上下文至关重要：缺乏明确的系统定义（如数据字典）会导致形式化不一致
4. 负面验证有效：证明失败能够有效指示逻辑不一致

相关工作

自动形式化的数据集构建

• ProofNet：本科级数学自动形式化
• MiniF2F：奥林匹克级数学基准
• 多语言数据集：Lean、Isabelle、Coq的组合训练提升性能

LLM训练策略

• "草稿-草图-证明"方法（Jiang et al.）：生成证明大纲指导形式化
• 子目标分解：DeepSeek-Prover采用的递归搜索策略
• 强化学习：提升定理证明成功率

应对非确定性

• 符号等价框架：处理pass@1与pass@k的差异
• RAG方法：检索精确形式定义提供上下文

应用领域扩展

• 数学问题求解：高中到本科数学
• 代码验证：程序正确性验证
• 生物医学：事实验证

本文贡献：首次将自动形式化应用于工程需求验证和LLM输出验证，开辟了新的应用方向。

结论与讨论

主要结论

1. 可行性验证：自动形式化管道能够有效验证LLM生成输出与原始需求的逻辑一致性
2. 双重应用价值：
   • 需求一致性检查（识别等价需求）
   • LLM输出质量控制（检测逻辑错误）
3. 概念验证：虽然样本有限，但成功展示了将定理证明技术应用于软件工程的潜力

局限性

1. 规模限制：
   • 仅测试了3个需求对
   • 缺乏大规模评估
   • 无统计显著性分析
2. 手动依赖：
   • 变量接地完全手动
   • 耗时且易出错
   • 限制了可扩展性
3. 模型限制：
   • 使用7B模型（资源受限）
   • 更大模型（671B）可能表现更好
   • 形式化质量依赖模型能力
4. 歧义性未解决：
   • 自然语言的固有歧义性
   • 缺乏系统本体论支持
   • 可能产生多个"正确"但不等价的形式化
5. 领域特定性：
   • 实验仅限于汽车安全需求
   • 泛化能力未知

未来方向

论文提出三个关键研究问题（RQ）：

RQ1：最佳形式化方法

• 探索k-pass策略（生成多个形式化，选择最可能的）
• 对比单次转换与多次采样的准确性

RQ2：变量接地自动化

• 方法1：上下文单次形式化（在单次调用中处理所有陈述）
• 方法2：基于相似度的接地（使用嵌入匹配系统本体）
• 挑战：如何验证LLM的接地假设本身的正确性

RQ3：约束系统中的LLM验证

• 构建系统动作的知识图谱
• 开发LLM遍历机制
• 使用自动形式化保证输出的逻辑一致性
• 应用场景：智能家居、车载助手等有限动作空间系统

其他方向：

• 开发自动化的变量规范化技术
• 集成领域特定本体（如汽车系统数据字典）
• 扩展到更复杂的逻辑表示（如时序逻辑）

深度评价

优点

1. 问题定义新颖：
   • 首次系统性地将自动形式化应用于LLM输出验证
   • 解决了工程实践中的真实痛点
   • 开辟了新的研究方向
2. 方法论清晰：
   • 管道设计简洁明了
   • 利用成熟工具（Lean 4, DeepSeek-Prover）
   • 可复现性强
3. 问题识别深刻：
   • 明确指出变量接地的关键性
   • 深入分析歧义性问题
   • 诚实讨论LLM非确定性的影响
4. 实用价值高：
   • 针对安全关键领域（汽车工程）
   • 可直接应用于需求工程流程
   • 有助于提升LLM应用的可信度
5. 写作质量优秀：
   • 结构清晰，逻辑严密
   • 提供了详细的提示模板（附录）
   • 图表丰富，易于理解

不足

1. 实验规模严重不足：
   • 仅3个样本：无法得出统计学结论
   • 缺乏不同领域、不同复杂度的需求测试
   • 未评估在更大数据集上的表现
   • 建议：至少需要50-100个需求对进行充分评估
2. 缺乏定量评估：
   • 无准确率、召回率等指标
   • 未报告形式化成功率
   • 缺乏与人工验证的对比
   • 建议：建立标注数据集，计算精确度指标
3. 手动干预过多：
   • 变量接地完全手动，削弱了自动化声明
   • 未提供自动化方案的具体实现
   • 可扩展性存疑
   • 建议：至少实现一个原型自动接地系统
4. 模型选择受限：
   • 因资源限制仅使用7B模型
   • 未探索671B模型或其他替代方案
   • 缺乏模型大小对结果影响的分析
   • 建议：至少在少量样本上对比不同模型
5. 缺乏失败案例分析：
   • 未详细分析定理证明失败的原因
   • 未区分形式化错误vs真实逻辑不一致
   • 缺乏假阳性/假阴性分析
   • 建议：建立错误分类体系
6. 评估标准单一：
   • 仅依赖Lean编译成功/失败
   • 未考虑部分正确的情况
   • 缺乏细粒度的错误类型分析
7. 泛化能力未知：
   • 仅测试汽车安全需求
   • 未验证在其他领域（医疗、金融等）的适用性
   • Gherkin场景的特殊性可能限制方法的通用性

影响力

对领域的贡献：

• ⭐⭐⭐⭐ 概念贡献高：提出了新的研究方向和应用场景
• ⭐⭐ 技术贡献中等：主要是现有技术的组合应用
• ⭐⭐⭐ 实用价值较高：解决了工程实践中的真实问题

实用价值：

• 短期：为需求工程师提供了验证思路
• 中期：可能催生专门的需求验证工具
• 长期：可能成为LLM应用质量保证的标准流程

可复现性：

• ✅ 使用开源工具（Lean 4, DeepSeek-Prover）
• ✅ 提供了详细的提示模板
• ❌ 未发布代码或数据
• ❌ 手动步骤难以复现
• 评分：⭐⭐⭐（中等）

预期影响：

• 可能引发更多关于LLM输出形式化验证的研究
• 可能推动需求工程与形式化方法的结合
• 变量接地问题可能成为新的研究热点

适用场景

高度适用：

• ✅ 安全关键系统的需求验证（汽车、航空、医疗）
• ✅ 需求一致性检查和去重
• ✅ LLM生成测试用例的质量控制

中度适用：

• ⚠️ 复杂业务逻辑的验证（需要扩展形式化能力）
• ⚠️ 多模态需求（如包含图表的需求）
• ⚠️ 实时系统（需要时序逻辑扩展）

不适用：

• ❌ 高度歧义的自然语言文本
• ❌ 缺乏明确系统定义的场景
• ❌ 需要实时响应的场景（当前手动步骤太慢）

改进建议

1. 立即可行：
   • 扩展到至少50个需求对
   • 实现基础的自动变量接地原型
   • 建立错误分类体系
2. 短期改进：
   • 对比不同规模的模型
   • 引入定量评估指标
   • 测试多个领域
3. 长期目标：
   • 完全自动化管道
   • 集成领域知识图谱
   • 支持时序逻辑和复杂约束

参考文献（关键文献）

1. Weng et al. (2025): Autoformalization in the era of large language models: A survey - 综述文献
2. Wu et al. (2022): Autoformalization with large language models - 自动形式化基础工作
3. Ren et al. (2025): DeepSeek-Prover-v2 - 本文使用的核心模型
4. Jiang et al. (2022): Draft, sketch, and prove - 子目标分解方法
5. de Moura & Ullrich (2021): The Lean 4 theorem prover - 形式化语言

总体评价：这是一篇概念验证型的探索性论文，提出了一个有价值的新研究方向，但实验验证严重不足。作为预印本和初步研究，它成功地识别了关键问题并提供了可行的技术路径，但距离成熟的解决方案还有很大距离。论文的主要价值在于问题定义和方向指引，而非技术突破。建议后续工作重点解决变量接地自动化和大规模评估问题。