LTLf Learning Benchmarks

该仓库包含10个LTLf学习基准家族，提供了生成实例的脚本，并包含超过15,000个学习问题，总计2GB的文件。基准文件以JSON格式结构化，每个文件代表一个学习问题。每个问题提供一组正负轨迹，分别位于`positive_traces`和`negative_traces`键下。每个轨迹是一个字典，其中键是原子命题，值是表示命题在每个步骤中真值分配的二进制值列表。

This repository contains 10 LTLf learning benchmark families, accompanied by scripts for generating instances, and includes over 15,000 learning problems with a total file size of 2 GB. The benchmark files are structured in JSON format, with each file representing a single learning problem. Each learning problem provides a set of positive and negative traces, which are stored under the `positive_traces` and `negative_traces` keys respectively. Each trace is a dictionary, where the keys are atomic propositions and the values are lists of binary values indicating the truth assignment of each proposition at each step.

原始信息汇总

LTLf Learning Benchmarks 数据集概述

数据集基本信息

• 数据集名称: LTLf Learning Benchmarks
• 数据量: 超过15,000个学习问题，原始文件2GB，压缩后100MB
• 数据格式: JSON格式

数据结构

• 核心字段:
  • positive_traces: 正例轨迹集合
  • negative_traces: 反例轨迹集合
  • atomic_propositions: 使用的原子命题列表
• 元数据字段:
  • 数量统计: number_traces, number_positive_traces, number_negative_traces, max_length_traces
  • 类型标识: trace_type
  • 来源信息: smallest_known_formula, generating_formula, generating_seed, original_repository, name, parameters

数据生成方法

• 主要脚本: sample.py
• 输入: 包含公式的文本文件
• 生成方式: 通过编译LTL公式为确定性自动机进行均匀随机采样

仓库结构

Fixed_Formulas

• 核心文件: formulas.txt（包含公式、原子命题和名称的三元组）
• 生成建议参数:
  • 轨迹数量(X): few=5, much=20, many=100
  • 轨迹长度(Y): short=16, medium=32, long=64

Generating_Instances

• 包含脚本: gen_X.py（X为特定算法名称）
• 算法来源:
  • Hamming: 来自VFB
  • OrderedSequence: 来自Syntcomp
  • Subword: 来自Scarlet
  • Subset: 来自Scarlet和Syntcomp
  • RandomBooleanCombinationsofFactors: 本论文新增

Generating_Formulas

• 包含脚本: gen_X.py（X为特定算法名称）
• 算法来源:
  • SingleCounter/DoubleCounter/Nim: 来自finite-synthesis
  • RandomConjunctsFromBasis: 基于Symbolic LTLf Synthesis论文

搜集汇总

数据集介绍

构建方式

LTLf Learning Benchmarks数据集通过系统化的方法构建，涵盖了10个不同的学习基准家族。其构建过程依赖于脚本生成实例，支持通过调整参数控制轨迹数量和长度。数据集采用JSON格式存储，每个文件代表一个学习问题，包含正负轨迹集合及元数据信息。构建过程中借鉴了Scarlet等工具的方法，将LTL公式编译为确定性自动机以实现轨迹采样，确保了数据的多样性和复杂性。

特点

该数据集包含超过15,000个学习问题，总数据量达2GB，压缩后仅100MB。其核心特点在于丰富的轨迹表示，每条轨迹以原子命题的二进制赋值序列呈现，并附带详细的统计元数据。数据集特别设计了不同难度级别的实例，包括固定公式生成的基准案例和特定家族构建的复杂问题，为LTLf学习算法提供了全面的评估基准。轨迹类型严格限定为有限轨迹，且每个问题都标注了生成公式和种子信息，保证了实验的可重复性。

使用方法

使用该数据集时，可通过sample.py脚本根据输入公式生成学习实例，支持自定义轨迹数量和长度参数。数据集按功能分为固定公式、生成实例和生成公式三大模块，研究者可根据需要选择不同复杂度的测试案例。对于高级应用，可调用各家族专属的gen_X.py脚本生成特定类型的公式或实例。JSON结构的设计便于直接解析，其中positive_traces和negative_traces字段为监督学习提供了标准化的训练数据，而原子命题列表和轨迹统计信息则方便进行特征工程分析。

背景与挑战

背景概述

LTLf Learning Benchmarks数据集由多个研究团队共同构建，旨在为有限线性时序逻辑（LTLf）学习提供标准化的评估基准。该数据集汇集了来自Scarlet、SYNTCOMP、finite-synthesis等多个知名项目的公式与实例，覆盖了10种不同的LTLf问题家族。其核心研究问题聚焦于如何高效地从有限轨迹中学习LTLf公式，这对形式化方法、程序合成和人工智能规划等领域具有重要理论价值与应用潜力。数据集通过结构化JSON格式存储了超过15,000个学习问题，每个问题包含正负轨迹样本及元数据，为算法验证提供了丰富素材。

当前挑战

该数据集面临的挑战主要体现在两方面：在领域问题层面，LTLf公式学习需解决轨迹稀疏性、逻辑表达复杂性以及学习算法可扩展性等难题，尤其当原子命题数量增加时，搜索空间呈指数级增长；在构建过程中，需平衡不同问题家族的难度分布，确保生成轨迹既能反映真实场景又具备计算可处理性，同时还需协调多源数据的格式统一与元数据标注。生成脚本需处理随机采样与特定模式轨迹的兼容性问题，这对基准的全面性与公平性提出了较高要求。

常用场景

经典使用场景

在形式化方法与自动机理论领域，LTLf Learning Benchmarks数据集为研究者提供了丰富的有限线性时序逻辑（LTLf）学习问题实例。该数据集通过生成包含正负样本的轨迹集合，成为验证新型学习算法性能的黄金标准。其多参数生成机制支持从简单模式到复杂布尔组合的梯度测试，尤其适合评估模型在轨迹长度和命题数量变化时的泛化能力。

衍生相关工作

该数据集已催生多个里程碑式研究，包括基于Scarlet框架的神经符号学习方法、结合GPU加速的VFB算法等。其衍生工作覆盖了从基础理论（如Syntcomp竞赛中的公式合成）到工程实践（如finite-synthesis项目中的计数器系统验证）的完整链条，相关成果发表在CAV、TACAS等顶级会议。

数据集最近研究

最新研究方向

在形式化方法与人工智能的交叉领域，LTLf Learning Benchmarks数据集正推动着有限线性时序逻辑（LTLf）学习算法的前沿探索。该数据集通过15,000余个结构化学习问题，为基于自动机的轨迹采样与公式推理提供了标准化测试平台。近期研究聚焦于三个核心方向：一是结合强化学习与符号推理的混合方法，利用数据集中标注的正负轨迹优化策略搜索效率；二是探索生成式模型在复杂公式合成中的应用，如RandomBooleanCombinationsofFactors等新型问题族所呈现的高阶逻辑组合特性；三是在硬件加速框架下验证算法可扩展性，部分研究已基于该数据集在GPU架构上实现了数量级的速度提升。这些进展直接响应了自动驾驶规划与物联网协议验证等领域对高效时序规约学习的需求，为构建可解释的决策系统提供了理论基础。