Agentified Assessment of Logical Reasoning Agents¶

会议: ICLR 2026
arXiv: 2603.02788
代码: HuggingFace数据集
领域: LLM推理
关键词: 逻辑推理评测, Agent-to-Agent评估, 一阶逻辑, 自动形式化, SMT求解

一句话总结¶

提出基于Agent的评测框架(AAA)，将评估逻辑封装为assessor agent并通过标准A2A接口与被测agent交互，在经Vampire定理证明器系统清洗的FOLIO数据集上，自动形式化agent（NL→Z3Py+SMT求解）达到86.70%准确率，大幅超过CoT基线73.89%，尤其在矛盾检测(False类)上提升32.79个百分点。

研究背景与动机¶

评估痛点一——失败模式混淆: 评估推理agent时，运行失败(超时/解析错误/运行时异常)与推理错误常被混淆在单一准确率数字中，难以区分"模型不会推理"和"模型的工具出了问题"
评估痛点二——集成成本线性增长: 传统评测harness将benchmark逻辑与agent实现紧耦合，每增加一个benchmark就需要重新集成，成本为O(n)
数据质量问题: FOLIO数据集存在潜在标签错误(训练集3.8%、验证集1.5%)和NL-FOL翻译质量问题，在不可靠数据上评估推理能力本身就不可靠
标准化接口缺失: 不同agent有不同的输入输出格式、执行环境和错误处理方式，缺乏统一的即插即用接口
形式化验证价值: 一阶逻辑推理是LLM的重要能力，但CoT方法无法保证逻辑有效性，形式化验证(SMT求解)提供确定性保证

方法详解¶

整体框架¶

Agentified Agent Assessment (AAA) = Assessor Agent(评估协议) + Agent Under Test(被测agent) + 标准A2A接口(AgentBeats/A2A Protocol)。评测逻辑被agent化，与被测agent通过标准接口通信。

关键设计¶

1. AAA评估框架: - Assessor agent负责完整评估流程: 下发任务→执行预算控制(超时/重试次数)→输出解析→结构化失败类型记录→生成机器可读评测报告 - 失败类型细分: Timeout(执行超时)、RuntimeError(运行时异常)、ParseError(输出解析失败)——区别于推理错误 - 核心价值: 集成成本从O(n)降至O(1)——agent实现A2A接口一次，即可参与任何assessor的评估 - 不丢弃失败: 传统harness将无法解析的输出计为错误，AAA区分执行失败和推理错误，支持事后审计

2. FOLIO数据清洗流水线: - Step 1: 用Vampire定理证明器对FOL表示做形式化验证——检查\(\bigwedge_i \phi_i \wedge \neg\varphi\)的可满足性判断True/False/Uncertain标签 - Step 2: 验证结果与标签冲突时，critique agent诊断翻译错误(括号不匹配/命名不一致等)，refiner agent执行定向修复 - Step 3: 迭代验证-修复直到一致，超阈值则标记人工审查 - 结果: 训练集674(67.3%)直接验证通过，23(2.3%)修复后通过，304(30.4%)仍有问题

3. 自动形式化Agent: - Stage 1 (代码生成): LLM将自然语言前提+结论生成可执行Z3Py程序 - Stage 2 (执行与验证): 沙箱执行(60s超时)，通过可满足性检查判断True/False/Uncertain - 自修复循环: 最多3次，遇语法错误时提取错误信息做定向代码修复后重试

4. CoT基线: 标准chain-of-thought提示，要求step-by-step推理后输出最终标签

实验关键数据¶

主实验表¶

方法	True准确率	False准确率	Uncertain准确率	总体准确率
Chain-of-Thought	89.04%	44.26%	84.06%	73.89%
Auto-formalization	90.41%	77.05%	91.30%	86.70%

消融分析¶

分析维度	发现
False类提升	+32.79pp，矛盾检测是CoT最弱项，形式化验证优势最显著
Uncertain类提升	+7.24pp，solver擅长处理逻辑不确定性
True类	89.04%→90.41%，已较高，提升有限
数据清洗影响	清洗后标签更可靠，评估结果更真实

关键发现¶

False类别的巨大提升(44.26%→77.05%)说明CoT在逻辑矛盾推理上的系统性弱点：模型难以从前提推导出矛盾(需要证明\(\phi \wedge \neg\varphi\)不可满足)
形式化验证将"好像对"式的推理替换为确定性的逻辑保证
Backbone使用Gemini 2.5 Flash(T=0.0)，确保确定性输出
数据清洗揭示了现有benchmark的隐含质量问题——在错误标签上评估会系统性低估模型能力

亮点与洞察¶

评测agent化的范式创新: 将评估本身变成agent，解耦了评估逻辑与被测agent实现，降低集成成本
结构化失败记录: 区分Timeout/RuntimeError/ParseError vs 推理错误，使评测可审计可追溯
数据清洗的启示: 用形式化定理证明器验证NLI数据集标签，比人工标注更可靠更可扩展
False类的巨大提升: 揭示了CoT在逻辑否定/矛盾推理上的根本局限——非形式化方法此处天花板有限

局限与展望¶

仅在单一数据集(FOLIO 203例验证集)上验证，规模极小，统计功效有限
仅比较了CoT和Auto-formalization两种agent，缺乏更多方法(如LINC/Logic-LM/SymbCoT)对比
数据清洗流水线仍有30.4%训练样本标记为"problematic"未解决，pipeline的完整性待提升
A2A接口的实际互操作性、通信延迟和开销未详细分析
自动形式化的Z3Py代码质量高度依赖backbone LLM能力
未测试在更复杂的推理任务(如高阶逻辑/概率推理)上的表现

评分¶

新颖性: ⭐⭐⭐ (AAA框架概念新颖，但自动形式化技术相对简单)
实验充分度: ⭐⭐ (单数据集、少对比方法、规模极小)
写作质量: ⭐⭐⭐⭐ (清晰规范，问题定义精确)
价值: ⭐⭐⭐ (评测agent化范式有启发性，数据清洗有实践价值)