A2RBench：一种可形式化验证的抽象推理基准自动生成范式

摘要

抽象推理能力反映了LLM提取和应用抽象规则的智力与泛化能力。然而，准确测量这一能力仍然充满挑战：现有基准要么依赖昂贵的人工标注而限制规模，要么有测得记忆而非真正推理的风险。为解决这一问题，我们提出名为A2RBench的自动化流水线，涵盖生成、扩展、评估与分析。具体而言，在生成阶段，LLM创造需要真正推理的多样化任务；在扩展阶段，LLM复用已验证规则并扩展新输入空间以生成任务变体，实现规模化。然而，这样的过程可能引发幻觉。为消除幻觉，我们进一步建立理论框架并证明：程序化验证——检验逆运算是否完美逆转前向运算（循环一致性）——可保证解的唯一性。通过对主流LLM的大量评估，我们发现：(1) 当前LLM在抽象推理上存在根本性缺陷，顶级模型在代表性子集上显著落后于人类（39.8%对68.5%）。(2) 当前LLM生成的3D任务复杂度远不及2D和1D，暴露其对高维任务缺乏理解。(3) 出人意料的是，信息复杂度更高的输入反而可能简化推理过程。

A2RBench：一种可形式化验证的抽象推理基准自动生成范式：论文配图 — 图 1：A2RBench 自动化管道以示例进行说明（规则：“通过模算术进行索引排列”）。该规则排列位置：给定输入长度 nn，找到最小整数 kk，其中 2≤k≤n−12\leq k\leq n-1 且 gcd⁡(k,n)=1\gcd(k,n)=1，然后将位置 ii 映射到 (i×k)modn(i\times k)\bmod n。当n=14n=14时，最小互质为k=3k=3，映射0→00\to 0、1→31\to 3、2→62\to 6等。第1阶段（种子生成）：作者模型生成由法官模型验证的规则描述。作者在Python中实现了正向函数ff（编码器）、逆向函数gg（解码器）、示例输入和查询输入。循环一致性检查验证所有输入的 g⁡(f⁡(x))=xg(f(x))=x，然后对琐碎案例进行判断过滤。第 2 阶段（任务扩展）：扩展器模型生成跨三个难度级别（标准、边缘情况、复杂）的输入变化，重用经过验证的规则代码。每个变体都经过循环一致性和判断验证。第 3 阶段（评估）：求解器模型接收示例、推断规则并回答查询。 Judge模型根据groundtruth验证正确性；对于符号任务，符号重新映射 (phi\phi) 衡量对熟悉标记的依赖。第 4 阶段（分析）：我们从三个维度进行分析：性能统计（准确性指标）、代码复杂性（基于 AST 的难度）和认知质量（推理分类）。该管道大规模生成经过形式验证的任务，同时实现超越二进制正确性的诊断评估。