LLMEval-Logic：一个经过求解器验证的、带有对抗性加固的大语言模型逻辑推理中文基准

# LLMEval-Logic：一个通过求解器验证的中文逻辑推理基准，用于大语言模型评估，并采用对抗性硬化策略  
来源：https://arxiv.org/html/2605.19597  

彭启源¹\* 魏银西¹ 沈玉炯¹,² 谭可欣¹ 王宇辉¹ 向正浩¹,² 叶俊杰¹,² 尹章悦¹,² 奚志恒¹,² 窦仕涵¹,² 桂涛¹ Maxm Pan²† 杨瑞芝³† 张奇¹† 黄萱菁¹  

¹ 复旦大学可信具身人工智能研究所  
² 腾讯混元团队  
³ 复旦大学哲学学院  

[email protected]  
[email protected]  
{yangruizhi, qz}@fudan.edu.cn  

###### 摘要  

评估大语言模型在自然语言逻辑推理上的能力至关重要，因为受规则约束的任务要求结论必须严格遵循给定的前提。许多现有的逻辑推理基准是通过从采样公式中对自然语言项进行模板化生成的，仅提供粗略或未经审核的形式化标注，并且现在已经被前沿推理模型迅速饱和。我们提出了 LLMEval-Logic，一个从现实情景场景构建的中文逻辑推理基准。其流程包括：正向创作和专家审核自然语言项及其参考形式化表示，用 Z3 验证标注答案，为自然到形式化评分构建专家评分细则，并通过闭环对抗性工作流程对选定项进行强化。该基准以两个配对的子集发布：一个包含 246 项的基础子集，附带 1,400 个专家开发的评分细则原子；以及一个包含 190 项的困难子集，带有 938 个多步子问题，覆盖封闭模型空间。在 LLMEval-Logic 上评估 14 个前沿大语言模型揭示了当前模型存在的显著差距：最佳模型仅达到 37.5% 的困难项准确率，即使有参考符号，评估模型中最高联合 Z3+评分细则形式化得分也仅达到 60.16%。我们的基准公开于 https://github.com/llmeval/LLMEval-Logic。  

††*同等贡献。†通讯作者。  

## 1 引言  

标题：音乐创作  
背景。考虑到和声适配，在创作这段乐曲时，作曲家只需要管弦乐队的某些部分配合。乐队目前有四个候选部分可以加入：小号、圆号、中音号和低音号。和声舒适规则如下：  
1. 如果加入圆号，则必须加入低音号。  
2. 加入中音号当且仅当加入小号且不加入圆号。  
3. 如果加入低音号，则不加入中音号。  
4. 要么加入小号且不加入低音号，要么加入低音号且不加入小号。  
5. 小号和中音号不能同时加入。  
6. 小号和圆号不能同时缺席。  
问题。最终可以加入哪些部分组合？  
参考答案。圆号和低音号。  

图 1：一个代表性的基础项（英文翻译）：模型在封闭世界场景中枚举可行解，根据 Z3 验证的参考答案评分。困难项链式包含约 5 个反事实子问题（附录 G (https://arxiv.org/html/2605.19597#A7)）。  

自然语言的逻辑推理是许多高风险大语言模型应用的基础，从合同审查、法规合规到临床指南检查和多步证明自动评分，其中结论必须严格遵循陈述的前提，而不是表面模式匹配 [logicbench:parmar2024, folio:han2024]。因此，对此能力的可靠基准测试是可信赖地在受规则约束的任务中部署大语言模型的先决条件。  

参见图注  
图 2：LLMEval-Logic 概述。构建流程从现实场景正向创作项目，审核自然语言→形式语言对齐的黄金标准，用 Z3 验证标注答案，构建专家评分细则，并通过闭环对抗性智能体工作流程对选定项进行强化。发布的基准包含配对的基础和困难子集，沿两个互补轴评估：模型响应的*答案准确率*（项/子问题）和模型生成形式化的*形式化准确率*（Z3 执行 + 评分细则匹配）。  

然而，当前的逻辑推理基准在三个互补维度上存在不足，我们将动机组织为以下挑战。  

挑战 1：如何让项目保持语义上扎根于现实场景？大量工作通过反向构建生成项目，即先采样一个形式结构，然后渲染成自然语言 [ruletaker:clark2020, proofwriter:tafjord2021, logicbench:parmar2024, wei-etal-2025-satbench, DBLP:journals/access/NadasDT25]。此类项目继承了模板化的措辞和公式化的篇章，偏离了现实场景，留下了分布痕迹，使得大语言模型无需执行底层推理即可从表面线索预测答案 [DBLP:conf/naacl/WuQRA0WKAK24, DBLP:conf/emnlp/JiangXHWM0TR24, DBLP:conf/ijcnlp/XieHZYCLLGK25]。  

挑战 2：如何以局部语义单元而非仅最终答案的粒度审核自然到形式化的翻译？人类编写的逻辑叙事 [folio:han2024, han-etal-2024-p] 提高了自然性，但只发布有限或未经审核的形式化标注，且未提供评分模型生成形式化的细则。因此，即使模型输出候选的一阶逻辑翻译，现有基准也无法判断逻辑关系、陈述约束和查询是否被忠实编码 [DBLP:journals/tai/McIntoshSALXWH26]。  

挑战 3：如何让基准保持足够困难以区分前沿推理模型？许多已发表的分割在现代推理模型下迅速饱和，顶级系统在项目级准确率上接近上限，几乎没有留下空间来定位这些模型仍然失败的地方 [suzgun-etal-2023-challenging, DBLP:conf/acl/KazemiFBPAMJAJC25]。  

图 3：LLMEval-Logic 的组成。基础涵盖单问题命题逻辑/一阶逻辑推理和形式化评分，包含 1,400 个评分细则原子（756 个逻辑关系，398 个陈述约束，246 个查询对齐）。困难包含对抗性强化的多问题项；一个项只有当每个子问题都正确时才正确。  

一个理论视角。自动推理面临终极复杂性限制：命题可满足性（SAT）是 NP-困难的 [DBLP:conf/stoc/Cook71]，一阶逻辑（FOL）可满足性是不可判定的 [Church1936-CHUANO]。这些界限对任何形式推理系统（包括 SMT 求解器和证明助手）都是不可逾越的。然而，大语言模型在自然语言中运作，无论证明复杂性如何都能产生答案 [saparov-he-2023-language]。对它们而言，更直接的实证瓶颈远在任何计算复杂性壁垒之前就出现了：大语言模型难以识别忠实形式化自然语言推理所需的逻辑关系、类型和量词 [yang-etal-2024-harnessing, DBLP:conf/acl/XuC00LHHC025, DBLP:journals/corr/abs-2601-23048]。因此，稳健的逻辑对齐，即忠实的自然到形式化翻译，仍然是一个关键且未解决的挑战，这激励了 LLMEval-Logic 的提出。  

为应对这些挑战，我们提出了 LLMEval-Logic，一个通过三阶段审核流程构建的中文逻辑推理基准。  

*首先*，经过逻辑课程预先培训的受训作者从真实情景场景（如资格规则、排程、角色或机构程序）正向创作每个项目，并将其与一个形式语言形式化配对。然后由具备形式推理学科研究生水平训练的标注员审核形式化。  

*其次*，每个项目通过一个四层归一化流程，涵盖词汇、句法、语义以及类型与参数检查。归一化后的项目进入 Z3 验证阶段，求解器检查形式化的前提和查询是否支持标注答案，在相应的 SAT、蕴涵或模型枚举语义下，由三个基础任务标签之一（possible, necessary, enumerate_models）分派。底层 SAT、蕴涵和模型枚举语义在第 2.1 节 (https://arxiv.org/html/2605.19597#S2.SS1) 中精确说明。每个经验证的项目还附带专家开发的评分细则，将自然到形式化的忠实度分解为逻辑关系、陈述约束和查询对齐。  

*第三*，在模型探测后被判定为过于简单的项目进入一个闭环对抗性强化工作流程，包含五个智能体角色：决策者、提议者、审查者、回答者和验证者。该工作流程沿六种强化策略重写这些项目，直到每个被接受的困难项通过审查和验证，并附带每一步的审计轨迹。  

所发布的基准包含两个配对的子集：基础子集用于审核过的单问题推理和自然到形式化评估，困难子集用于在同一正向创作项目基础上的多问题对抗性推理。  

我们的贡献有三点：  
1. 我们发布了 *LLMEval-Logic*，一个正向创作、经 Z3 审核的中文逻辑推理基准，配有专家开发的评分细则和配对的基础/困难子集。  
2. 我们设计了一个闭环对抗性强化工作流程（决策者、提议者、审查者、回答者、验证者），沿六种结构策略重写高准确率项目，仅发布通过审查和验证的项目。  
3. 我们在三个独立运行上对 14 个前沿大语言模型变体进行了系统评估，评估了自然语言逻辑推理和忠实的自然到形式化翻译。  

## 2 设计  

### 2.1 数据集构建  

参见图注  
图 4：两个已发布子集的组成。左：基础问题类型分布（项目可能带有多个标签）和命题逻辑/一阶逻辑分割。右：困难子问题数量分布（突出条 = 众数 5）。  

LLMEval-Logic 围绕三个构建目标：通过正向创作而非反向模板化来创作中文推理项目；为每个项目配对一个经 Z3 验证的形式表示和专家开发的评分细则；校准基准难度，使项目对前沿大语言模型仍具挑战性。基础项目构建分为五个按序的审核阶段（正向创作、专家审查、分层归一化、基于 Z3 的形式验证、评分细则构建）；然后，经过验证的基础项目进入第 2.2 节 (https://arxiv.org/html/2605.19597#S2.SS2) 的对抗性强化流程，以生成困难子集。表 3 (https://arxiv.org/html/2605.19597#S1.F3) 总结了已发布组成，图 4 (https://arxiv.org/html/2605.19597#S2.F4) 可视化了其在问题类型和困难子问题数量上的分布。  

##### 正向创作、专家审查和归一化。  

LLMEval-Logic 从 521 个人工种子中文推理项目开始，这些项目由具有逻辑课程背景的贡献者编写，他们将可形式化的逻辑结构嵌入自然主义场景（规则、排程、资格、机构程序），而不是反向翻译采样公式。然后，具有形式推理学科研究生水平训练的标注员审查概念稳定性、推理有效性、清晰度以及自然语言到形式语言的忠实度，将每个变量、谓词、前提和标注答案追溯回中文问题陈述（Lean 被用作选定项目的辅助正确性检查）。经过审查的项目通过一个四层归一化流程（词汇、句法、语义对齐、类型/参数），将人工审核的形式化转换为一致的、可解析且可审计的对象，同时不改变其语义；逐层归一化细节见附录 A (https://arxiv.org/html/2605.19597#A1)。  

##### 形式验证。  

我们使用 Z3 SMT 求解器对归一化和人工审核的形式化进行形式验证，将形式化的前提和形式化的查询都发送给求解器。此阶段有双重目的：它验证标注答案在逻辑上通过适当的求解器操作得到认证，并揭示残留的形式化缺陷，如缺失或冗余前提、问题类型不匹配或符号映射不一致。我们将基础问题分为三种任务类型：possible, necessary 和 enumerate_models——这些被视为 NLP 任务标签，映射到不同的 Z3 求解模式，而非严格的模态逻辑算子。对于前提集 Σ 和查询 φ，possible 检查可满足性 Sat(Σ ∪ {φ})（等价于 Σ ⊭ ¬φ）；necessary 通过 Unsat(Σ ∪ {¬φ}) 检查蕴涵 Σ ⊨ φ；enumerate_models 返回封闭场景上的不同满足赋值。失败的检查触发项目修复和 Z3 重新验证，因此干净的基准只包含通过形式验证的项目。  

##### 专家开发的评分细则。  

形式验证验证了标注答案从归一化的参考形式化中推导出来，但它本身并不能提供一个细粒度的标准来评估模型生成的形式化。因此，我们为每个基础项目构建专家开发的评分细则，以局部语义单元粒度审计自然语言到形式语言的忠实度。评分细则将参考形式化分解为三组：logical_relation 检查核心关系如蕴含、否定、析取、排他性和量词是否被正确编码；stated_constraint 检查显式事实、边界条件、对象域和类型限制是否被保留；query_alignment 检查形式化查询是否与自然语言问题匹配。每个评分细则以两种对齐形式存储：一个用于语义检查的自然语言标准和一个用于自动评分的 Z3 可检查语句。我们根据专家确认的参考形式化校准所有评分细则，要求黄金形式化在下游 NL 到 FL 评估之前通过完整的自然语言评分细则集。  

##### LLMEval-Logic-Base。  

LLMEval-Logic-Base 是用于答案评估和形式化评分的单问题子集。每个项目都经过专家审查、归一化和基于 Z3 的形式验证，并使用上面定义的一个或多个基础问题类型：possible, necessary 和 enumerate_models。每个基础项目都配有用于评分模型生成形式化的专家开发评分细则。  

表 1：LLMEval-Logic 在基础（单问题项准确率）和困难（项准确率加子问题准确率）上的排行榜，gpt-5.1-chat judge，3 次运行的平均值±标准差。与另外两个前沿判断器（Claude Opus 4.6, Gemini 3.1 Pro）之间的判断一致性见附录 D (https://arxiv.org/html/2605.19597#A4)。条形图编码分数在 0-100 范围内。困难项准确率要求一个项的所有子问题都匹配；子问题准确率对单个子问题评分。行按困难项准确率排序；每列最佳值加粗。  

### 2.2 对抗性强化  

##### 强化工作流程。  

经过专家审查、归一化和验证后，用代表性大语言模型探测候选项目，以估计其经验难度。由此产生的探测分数仅用于路由，从不用于答案验证：低准确率项目被手动重新检查，并在验证后保留在基础中，而高准确率项目进入一个包含五个智能体角色的闭环强化工作流程。这五个角色实现如下强化循环。决策者诊断浅层解决路径并发出