LTLZinc

LTLZinc是一个基准测试框架，用于生成涵盖各种不同问题的数据集，可以用于评估神经符号和持续学习方法在时间和约束驱动维度上的性能。该框架从MiniZinc约束上的线性时态逻辑规范和任意图像分类数据集中生成表达式的时态推理和持续学习任务。细粒度的注释允许在相同的生成数据集上进行多种神经和神经符号训练设置。实验表明，LTLZinc生成的任务具有挑战性，并突出了当前最先进方法的局限性。

原始信息汇总

LTLZinc数据集概述

数据集基本信息

• 名称: LTLZinc Benchmark
• 用途: 用于时间维度上的知识驱动学习和推理的基准测试框架
• 论文: LTLZinc Benchmark
• 许可证: CC BY-NC-SA 4.0

数据集特点

• 生成方式: 通过有限域约束求解器（MiniZinc）和基于自动机的采样器联合生成
• 任务类型:
  • 基于序列的学习和推理
  • 增量学习

数据集组成

• 任务组件:
  • 一个或多个有限域（数据类型）
  • 一组通道，将域映射到感知刺激
  • 约束词汇表，描述通道间属性
  • 线性时序逻辑公式（LTLf），指定约束在特定时间是否成立

示例任务

1. 顺序模式示例:

   • 描述: 始终满足Y小于Z当且仅当两步后V、W和X属于同一类
   • 数据集: FMNIST
   • 序列长度: 10-20

2. 增量模式示例:

   • 描述: 植物标签仅在30个任务中的单个任务中观察到
   • 数据集: CIFAR-100
   • 序列长度: 30

数据集使用

• 下载方式: 使用download_images.py脚本或手动放置图像文件
• 配置要求: 创建YAML配置文件并放置在benchmark/tasks/specs/目录下
• 生成命令: 运行python main.py

数据文件说明

• 顺序模式任务:

  • 文件: tasks/TASK_NAME/sequence_SPLIT.csv
  • 包含列: sample_id, seq_id, time, accepted, transition, img_STREAMNAME, out_STREAMNAME, var_STREAMNAME, p_ID

• 增量模式任务:

  • 文件: tasks/TASK_NAME/incremental_SPLIT.csv
  • 额外列: task_id

相关文件

• domain_values.yml: 映射注释到值
• mappings.yml: 映射注释到值
• automaton.yml: 用于规划持续学习策略

系统要求

• 主要依赖:
  • flloat==0.3.0
  • minizinc==0.9.0
  • numpy==2.0.0
  • pandas==2.2.2
  • PyYAML==6.0.1
  • sympy==1.12
  • torch==2.3.0a0+git39ae4d8
  • torchvision==0.18.1
  • tqdm==4.66.1
• 额外要求: 系统级安装MiniZinc

搜集汇总

数据集介绍

构建方式

LTLZinc数据集的构建基于线性时序逻辑（LTL）和MiniZinc约束规范，通过将时序逻辑公式与图像分类数据集结合生成复杂的时序推理任务。具体流程包括：1）定义感知域（如MNIST、Fashion-MNIST）及其符号标签；2）设计一阶约束关系（如算术比较、集合运算）；3）用LTL公式描述时序行为规则；4）通过自动机转换和约束求解生成满足/违反规范的序列。生成器支持两种模式：序列模式（生成带标注的时序数据）和增量模式（构建课程式学习经验），并通过偏置采样避免平凡解。

特点

LTLZinc的核心特点体现在三方面：1）时序-符号耦合性，通过LTL公式将符号约束（如“Y<Z当且仅当两步后V=W=Z”）与图像序列动态绑定；2）多粒度标注，提供图像标签、约束有效性、自动机状态轨迹和序列标签四层监督信号；3）可扩展的模态支持，兼容任意图像数据集（如MNIST/CIFAR）和自定义约束库。其生成的挑战性任务（如罕见事件预测、周期性概念重现）能有效评估模型对推理捷径和灾难性遗忘的鲁棒性。

使用方法

该数据集支持三类典型用法：1）时序分类任务，利用序列级标签训练模型判断整体时序行为；2）远程监督学习，仅通过序列标签反推符号级映射关系；3）约束归纳任务，从时序规则中推导约束语义。使用时需注意：对于神经符号方法，建议采用分阶段训练（先预训练感知模块再联合优化）；对于持续学习场景，可利用自动机状态作为课程先验知识。实验配置推荐使用温度校准缓解概率估计偏差，并通过中间监督（如约束有效性标注）提升模块协同性。

背景与挑战

背景概述

LTLZinc是由Luca Salvatore Lorello等人于2025年提出的一个基准测试框架，旨在结合持续学习和神经符号时序推理的研究领域。该框架通过线性时序逻辑（LTL）规范和MiniZinc约束生成多样化的任务，用于评估神经符号方法和持续学习算法在时序和约束驱动维度上的性能。LTLZinc的提出填补了现有基准测试在时序推理和持续学习结合方面的空白，为相关领域的研究提供了重要的工具。

当前挑战

LTLZinc面临的挑战主要包括两个方面：1) 在领域问题解决方面，该数据集旨在解决时序推理和持续学习中的复杂问题，如如何在动态环境中保持知识的同时避免灾难性遗忘，以及如何有效地结合符号推理和神经网络学习；2) 在构建过程中，面临的挑战包括如何高效地将LTL规范转换为可执行的约束满足问题，以及如何处理大规模数据生成中的计算复杂性问题。此外，确保生成的数据集既能覆盖多样化的任务，又能保持实验的可重复性和一致性，也是一个重要的挑战。

常用场景

经典使用场景

LTLZinc数据集在神经符号人工智能和持续学习领域中被广泛用于评估时间推理和关系学习的能力。该数据集通过结合线性时序逻辑（LTL）和MiniZinc约束，生成了多种复杂的时间序列任务，特别适用于需要处理动态知识和避免灾难性遗忘的场景。经典使用场景包括序列分类、时间距离监督和约束归纳等任务，这些任务要求模型在时间维度上进行复杂的符号推理。

衍生相关工作

LTLZinc数据集衍生了许多相关的研究工作，特别是在神经符号集成和时间推理领域。例如，基于该数据集的DeepDFA和NesyA等研究探索了如何将时序逻辑与神经网络结合。此外，该数据集还启发了KANDY等持续学习基准的扩展，这些工作进一步推动了神经符号方法在复杂时间行为下的评估。LTLZinc的开源生成器也为社区提供了自定义任务的能力，促进了更多创新研究的产生。

数据集最近研究

最新研究方向

LTLZinc数据集作为神经符号人工智能和持续学习领域的前沿基准框架，其最新研究聚焦于时间推理与约束驱动的多维度评估。该数据集通过线性时序逻辑（LTL）规范与MiniZinc约束的融合，支持生成涵盖序列分类、远程监督和约束归纳等复杂任务的多样化问题，尤其强调时序维度上的知识整合与推理能力。当前研究热点包括：1）探索神经符号架构在动态时序场景下的知识遗忘与稳定性平衡；2）开发新型持续学习策略以应对周期性重复出现的类别或概念漂移；3）利用符号化自动机背景知识增强神经网络对时序约束的理解。相关实验表明，现有方法在长序列时序推理任务中仍面临显著挑战，尤其在算术约束与跨域知识迁移方面存在优化瓶颈。该数据集的发布为构建统一的时间学习与推理框架提供了关键实验平台，推动了可信AI系统中时序知识表示与持续适应能力的研究。

相关研究论文

• LTLZinc: a Benchmarking Framework for Continual Learning and Neuro-Symbolic Temporal Reasoning

  意大利比萨大学计算机科学系、意大利摩德纳和雷焦艾米利亚大学、比利时鲁汶大学、希腊NCSR“Demokritos”研究中心 · 2025年