SYNTCOMP 2025 基准数据集

该数据集由SYNTCOMP 2025反应式合成竞赛的基准规范构成，旨在为硬件电路自动生成提供标准化评估框架。数据集包含1586条以时序逻辑合成格式（TLSF）编写的规格说明，涵盖可实现与不可实现两类问题，数据来源于年度竞赛的累积成果。其创建过程通过竞赛组织者系统收集与格式化，确保逻辑严谨性与可比性。该数据集主要应用于形式验证与硬件设计自动化领域，用于测试和比较不同合成工具在从逻辑规约生成正确硬件电路方面的性能，旨在推动反应式合成算法的前沿发展。This dataset comprises benchmark specifications from the SYNTCOMP 2025 Reactive Synthesis Competition, designed to offer a standardized evaluation framework for automatic hardware circuit generation. It contains 1,586 specification documents written in the Temporal Logic Synthesis Format (TLSF), covering both realizable and unrealizable problem cases, with data sourced from the cumulative outcomes of the annual competition. The dataset was systematically collected and formatted by the competition organizers during its curation, ensuring logical rigor and cross-sample comparability. Primarily applied in the fields of formal verification and hardware design automation, this dataset is used to test and compare the performance of various synthesis tools when generating correct hardware circuits from logical specifications, with the ultimate goal of advancing cutting-edge research in reactive synthesis algorithms.

原始信息汇总

数据集概述

该数据集由 SYNTCOMP 社区收集整理，主要用于反应合成与验证领域的基准测试。

数据类型与格式

数据集包含以下四种类型的基准测试，分别以不同格式保存：

• AIGER 格式：安全博弈（safety games），编码在扩展的 AIGER 格式中
• TLSF 格式：LTL（线性时态逻辑）合成问题
• TLSF-fin 格式：有限词上的 LTLf（LTL for finite words）合成问题，使用扩展的 TLSF 格式
• Parity 格式：奇偶博弈（parity games），使用扩展的 HOA 格式

下载链接

数据集按年份提供下载，以下是各年份的下载地址：

• 2025 年

  • TLSF：https://github.com/SYNTCOMP/benchmarks/releases/download/v2025.1/selection-ltl-2025v2.zip
  • TLSF-fin：https://github.com/SYNTCOMP/benchmarks/releases/download/v2025.1/selection-ltlf-2025.zip
  • Parity：https://github.com/SYNTCOMP/benchmarks/releases/download/v2025.1/selection-parity-2025.zip

• 2024 年

  • TLSF：https://github.com/SYNTCOMP/benchmarks/releases/download/v2024.0.1/tlsfSelection2024.zip
  • TLSF-fin：https://github.com/SYNTCOMP/benchmarks/releases/download/v2024.0.1/tlsfFinSelection2024.zip
  • Parity：https://github.com/SYNTCOMP/benchmarks/releases/download/v2024.0.1/paritySelection2024.zip

• 2023 年

  • TLSF：https://github.com/SYNTCOMP/benchmarks/releases/download/v2023.4/TLSF_2023.zip
  • TLSF-fin：https://github.com/SYNTCOMP/benchmarks/releases/download/v2023.4/TLSF-fin_2023.zip
  • Parity：https://github.com/SYNTCOMP/benchmarks/releases/download/v2023.4/Parity_2023.zip

• 2022 年

  • TLSF：https://github.com/SYNTCOMP/benchmarks/releases/download/v2022/TLSF_2022.zip
  • Parity：https://github.com/SYNTCOMP/benchmarks/releases/download/v2022/PGAME_2022.zip

• 2021 年

  • TLSF：https://github.com/SYNTCOMP/benchmarks/releases/download/v2021/TLSF_2021.zip
  • Parity（合成问题）：https://github.com/SYNTCOMP/benchmarks/releases/download/v2021/PGAME_Synth_2021.zip
  • Parity（可实现性问题）：https://github.com/SYNTCOMP/benchmarks/releases/download/v2021/PGAME_Real_2021.zip

• 2020 年

  • AIGER：https://github.com/5nizza/syntcomp_benchmarks/releases/download/v2020/AIGER_2020.zip
  • TLSF：https://github.com/5nizza/syntcomp_benchmarks/releases/download/v2020/TLSF_2020.zip
  • Parity：请参见仓库

• 2019 年

  • AIGER：https://github.com/5nizza/syntcomp_benchmarks/releases/download/v2019/AIGER_2019.zip
  • TLSF：https://github.com/5nizza/syntcomp_benchmarks/releases/download/v2019/TLSF_2019.zip

• 2015-2018 年：请访问 https://syntcomp.react.uni-saarland.de/

提交新基准测试

如需提交新基准测试，可通过以下方式：

• 创建新 Issue，并将包含新基准测试的压缩包附加到 Issue 中
• 压缩包中应包含 readme.md 或 readme.pdf 文件，描述基准测试及相关论文等信息
• 亦可直接创建 Pull Request 提交基准测试

搜集汇总

数据集介绍

构建方式

SYNTCOMP 2025 基准数据集源自年度反应式综合竞赛（SYNTCOMP）的LTL综合赛道，汇集了1586个以时间逻辑综合格式（TLSF）表述的规格说明。这些规格说明在收集过程中被剥离了所有注释、描述和名称，以避免对解决方式或可实现性提供任何提示。其中，458个规格已知可实现，419个已知不可实现，其余规格的可实现性状态未知。此外，基于竞赛基准中参数值等价的规格，进一步提炼出57个通用参数化规格，构成参数化综合子集。同时，为支持从自然语言到硬件电路的端到端综合，还手工创建了包含57条自然语言描述的NATURAL数据集，每条描述均对应一个参数化规格，参数值设置为SYNTCOMP中的最大值，形成高难度测试基准。

特点

该数据集最显著的特点在于其规模与难度：1586个规格覆盖了反应式综合领域最具挑战性的标准化基准，是评估综合工具性能的行业标准。数据集不仅包含标准LTL综合问题，还延伸至参数化综合这一理论上不可判定的问题域，以及自然语言驱动的综合任务，极大拓展了传统综合的边界。NATURAL子集的手工构建确保了自然语言描述与形式化规格之间的紧密对应，使得从非正式需求到硬件实现的端到端验证成为可能。此外，数据集附带可实现性标注，支持对综合算法的全面评估，包括对可实现与不可实现规格的处理能力。

使用方法

该数据集主要用于评估和对比不同反应式综合方法的性能。标准用法是将TLSF格式的规格作为输入，要求综合工具生成满足规格的Verilog模块（可实现情况）或环境策略（不可实现情况），并通过模型检查器验证正确性。对于参数化综合，则要求生成含参数声明的Verilog模块，并在多个参数值下进行验证。自然语言综合实验则需将NATURAL数据集中的自然语言描述作为输入，可选择先自动形式化为TLSF再进行综合，也可以直接端到端生成Verilog代码，最终均通过形式化验证评估正确性。建议运行结果取多次重复实验的平均值以考虑非确定性影响。

背景与挑战

背景概述

SYNTCOMP 2025基准数据集是国际反应式综合竞赛（SYNTCOMP）官方发布的标准化评测集合，由CISPA亥姆霍兹信息安全中心与慕尼黑工业大学的研究团队于2026年整理并公开。该数据集收录了1586条以时序逻辑综合格式（TLSF）描述的规格说明，覆盖了从简单控制器到多客户检测器等多样化的反应式系统设计问题，旨在为自动生成正确硬件电路的算法提供公平、可复现的评估平台。作为领域内最具权威性的标杆之一，SYNTCOMP数据集长期驱动着反应式综合算法的迭代与竞争，其年度竞赛结果直接映射着该领域从经典符号方法到新兴神经符号范式的演进轨迹，对验证形式化方法的实用化进展具有不可替代的引导作用。

当前挑战

该数据集所聚焦的核心挑战在于攻克反应式综合固有的高计算复杂度——该问题对于线性时序逻辑而言是2-EXPTIME完全的，传统符号工具在面对大规模或参数化规格时常遭遇可扩展性瓶颈。具体而言，构建过程中的挑战体现在三个层面：其一，1)从TLSF规格到可综合Verilog代码的自动翻译需要精准捕获时序逻辑的深层语义，且需同时处理可实现与不可实现的规格类别；其二，2)参数化综合问题（如n客户检测器）已被证明为不可判定，传统算法无法生成与参数无关的通用实现；其三，3)模型检验步骤本身计算昂贵，对大规模参数值的验证易出现超时，形成综合流水线中的瓶颈环节。

常用场景

经典使用场景

SYNTCOMP 2025 基准数据集是反应式综合领域最权威的评估平台，汇集了来自年度竞赛的1586个时序逻辑规范，涵盖可实现与不可实现两类规格。该数据集的核心用途在于衡量各类反应式综合工具的性能表现，特别是大型推理模型在结合形式化验证反馈后，能否在标准化的竞争基准上超越传统符号化综合工具。通过将TLSF格式的规范作为输入，研究者可以评估模型生成Verilog硬件描述的能力，并在模型检查器提供的反例引导下迭代修复实现，从而在严格设定的时间与内存约束下，检验神经符号方法的鲁棒性与效率。

解决学术问题

该数据集主要解决了反应式综合领域长期存在的计算复杂性困境，即线性时序逻辑的2-EXPTIME完全性问题。传统符号化算法虽理论完备，却难以应对工业规模的系统设计。SYNTCOMP 2025 基准数据集为评估神经符号方法提供了坚实平台，证明了大型推理模型能够在不依赖穷举游戏求解的情况下，通过猜测-检查循环高效生成正确实现。此外，数据集中的参数化规范子集还使研究者得以探索传统上不可判定的参数化综合问题，推动了对可复用、可配置硬件设计模板的学术研究，显著拓宽了反应式综合的理论边界与应用潜力。

衍生相关工作

基于SYNTCOMP 2025 基准数据集，衍生了一系列重要学术工作。在神经符号综合方面，研究者开发了CEX-LRM方法，将反例引导与大型推理模型结合，显著提升了综合成功率。在自动形式化领域，该数据集催生了从自然语言到时序逻辑的翻译研究，如nl2spec框架，通过分解子翻译和模型检查反馈增强翻译准确性。此外，参数化综合子集激发了关于不可判定问题的实证探索，推动了Verilog参数化模块的自动生成技术。这些衍生工作共同构建了从规格描述到形式验证的完整工具链，为反应式综合的工业化落地奠定了方法论基础。