Automated Reasoning Synthesis Benchmarks

本数据集是由维也纳工业大学等研究机构的研究人员创建的，旨在为自动推理的合成问题提供标准基准集。数据集包含290个基准问题，其中180个是非递归问题，110个是关于代数数据类型的递归问题。数据集采用了SMT-LIB和SyGuS两种格式，支持不可计算符号的限制，并提供了辅助引理来帮助证明解决方案的存在性。数据集适用于评估自动推理工具在第一阶逻辑中的证明和合成能力，包括对理论和归纳的推理。

搜集汇总

数据集介绍

构建方式

Automated Reasoning Synthesis Benchmarks数据集通过整合现有基准并新增253个问题，构建了一个包含290个合成问题的动态增长集合。该数据集采用SMT-LIB 2.7语法扩展的SMT-LIB-SYNU格式，支持通过∀∃-公式定义程序规范，并引入不可计算符号限制。每个问题由规范公式和不可计算符号集合构成，其中规范公式采用多类一阶逻辑表达式，可能包含理论和递归定义。数据集还提供了与SyGuS 2.1语法的双向转换脚本，实现了两种合成框架的兼容性。

特点

该数据集的核心特征体现在其形式化规范的表达能力和问题多样性。所有基准问题均采用∀∃-一阶逻辑公式定义程序规范，支持理论推理和归纳法应用，包含180个非递归问题和110个递归问题。递归问题涉及自然数、列表和二叉树等代数数据类型，需要归纳推理能力。数据集特别设计了不可计算符号限制机制，通过语法约束确保合成程序的正确性。问题覆盖线性算术、非线性算术、未解释函数等多种理论领域，并细分为辅助引理增强的assisted版本和基础original版本，为评估自动推理工具的证明与合成能力提供了多维度的测试平台。

使用方法

使用该数据集时，研究者可通过三种典型方式开展实验评估。首先，采用支持SMT-LIB-SYNU格式的自动推理工具（如cvc5、Synthesiz3或Vampire）直接处理.smt2文件，通过assert-synth命令定义合成任务。其次，通过配套Python脚本将问题转换为SyGuS格式，利用语法引导合成框架进行求解。对于递归问题，需配置工具启用归纳推理模式。评估时应区分original和assisted两类基准，前者仅包含必要公理，后者附加辅助引理，可分别测试工具的自主推理能力和引理利用效率。数据集持续更新机制鼓励研究者贡献新问题，推动自动合成技术的边界拓展。

背景与挑战

背景概述

Automated Reasoning Synthesis Benchmarks数据集由维也纳技术大学、捷克技术大学、曼彻斯特大学等机构的研究团队于2025年创建，旨在填补演绎式程序合成领域基准测试集的空白。该数据集专注于以∀∃-形式逻辑公式作为程序规范的合成问题，支持不可计算符号限制这一关键特性。作为首个采用SMT-LIB-SYNU格式的基准集，它有效桥接了语法引导合成(SyGuS)与传统一阶逻辑方法之间的技术鸿沟，为自动推理引擎在理论证明与程序生成方面的性能评估提供了标准化平台。

当前挑战

该数据集面临双重挑战：在领域层面，需解决包含理论、量词和归纳法的复杂规范验证问题，现有工具对递归问题的解决率仅为15.5%；在构建层面，需平衡不可计算符号限制与语法表达力，处理SMT-LIB与SyGuS格式的语义等价转换，并设计支持归纳推理的递归问题表示方法。特别在递归问题类别中，如何有效编码代数数据类型的归纳特性成为制约合成成功率的关键瓶颈。

常用场景

经典使用场景

Automated Reasoning Synthesis Benchmarks数据集在程序合成领域中被广泛用于评估基于一阶逻辑的演绎合成方法。该数据集通过提供形式化的∀∃-公式规范，支持研究者测试和验证自动化推理引擎在理论和归纳推理方面的能力。特别是在处理包含不可计算符号限制的合成问题时，该数据集为比较不同合成工具的效能提供了标准化平台。

衍生相关工作

该数据集催生了多项重要研究，包括维也纳工业大学团队开发的基于饱和的递归程序合成方法，以及结合SMT求解与不可计算符号处理的Synthesiz3系统。相关成果发表在CAV、FMCAD等顶级会议，推动了程序合成与自动推理的交叉研究，并为SyGuS标准的扩展提供了理论基础。

数据集最近研究

最新研究方向

近年来，Automated Reasoning Synthesis Benchmarks数据集在程序合成领域引起了广泛关注，特别是在演绎合成和自动化推理方向。该数据集通过提供以∀∃-公式形式给出的规范，填补了现有基准测试集的空白，并支持不可计算符号限制。数据集不仅包含了37个现有基准测试，还新增了253个问题，涵盖了非递归和递归问题，涉及线性整数算术、线性实数算术、未解释函数和归纳数据类型等多种理论。前沿研究主要集中在如何利用SMT求解和一阶定理证明技术来处理这些复杂的合成问题。该数据集的动态扩展特性为自动化推理、程序验证和计算机数学等领域的进一步发展提供了重要支持。

相关研究论文

• Synthesis Benchmarks for Automated Reasoning

  维也纳工业大学, 捷克理工大学, 曼彻斯特大学, EasyChair · 2025年