UnsatChristmas

UnsatChristmas数据集存放在`database_small`文件夹中，用于进行交互式计划修复实验。The UnsatChristmas Dataset is stored in the `database_small` folder and is utilized for interactive plan repair experiments.

原始信息汇总

大型语言模型可以使用形式验证工具严格解决现实世界规划问题

本文代码和数据集对应于论文《Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools》。

框架

环境设置

1. 创建conda环境并安装依赖： bash conda create -n fmtravelplanner python=3.9 conda activate fmtravelplanner pip install -r requirements.txt

2. UnsatChristmas 数据集位于 database_small 文件夹中。您可以使用此数据库运行交互式计划修复实验。

3. 要运行可满足计划生成实验，请参考论文《TravelPlanner: A Benchmark for Real-World Planning with Language Agents》及其GitHub仓库，下载数据库和训练/验证/测试集。

运行

可满足计划求解

可满足计划生成实验的文件是 test_travelplanner.py。一个示例命令是 python test_travelplanner.py --set_type train --model_name gpt 注意：您可能需要使用训练集来调整不同LLM的提示语。您可以添加自定义的步骤和代码检查器以进一步提高性能。

不可满足计划修复

• 运行 test_travelplanner_interactive.py 以进行TravelPlanner的不可满足交互式计划修复实验。按照文件中的说明，首先收集初始代码，然后进行计划修复。
• 运行 test_unsat.py 以进行UnsatChristmas的不可满足交互式计划修复实验。按照文件中的说明，首先收集初始代码，然后进行计划修复。

提示语

我们使用的提示语包含在 prompts 文件夹中。

搜集汇总

数据集介绍

构建方式

UnsatChristmas数据集旨在为大型语言模型在现实世界规划任务中的应用提供严格的正式验证工具。该数据集的构建依托于TravelPlanner框架，包含在`database_small`文件夹中的实例，用于支持交互式规划修复实验。数据集的构建涉及从现实世界规划任务中提取出的不可满足规划场景，为语言代理在规划任务中的表现提供评估基础。

特点

UnsatChristmas数据集的主要特点是聚焦于不可满足的规划修复，为研究提供了针对规划任务中特定挑战的测试案例。数据集包含实际场景的复杂数据，要求语言模型不仅生成可行的规划，还需通过正式验证工具进行验证。此外，数据集的设计允许研究者在不同的语言模型上进行实验，以评估其性能和泛化能力。

使用方法

使用UnsatChristmas数据集，研究者首先需设置实验环境，创建conda环境并安装相关依赖。数据集的使用涉及两个主要实验：可满足规划生成实验和不可满足规划修复实验。前者通过`test_travelplanner.py`文件进行，后者则通过`test_unsat.py`文件执行。实验中，研究者需遵循脚本中的指示，收集初始代码并进行规划修复。同时，`prompts`文件夹中包含了用于实验的提示信息，以辅助研究者在不同的大型语言模型上进行实验操作。

背景与挑战

背景概述

UnsatChristmas数据集作为大型语言模型在现实世界规划中应用的研究成果之一，其创建旨在通过形式化验证工具严格解决实际规划问题。该数据集伴随着论文《Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools》的发表而公之于众，由相关研究人员精心构建。该数据集的研究背景聚焦于大型语言模型在旅行规划等实际场景中的应用，核心研究问题是如何利用这些模型生成满足特定条件的规划，并对生成的规划进行形式化验证，确保规划的准确性。该数据集的发布对自然语言处理、自动规划以及形式化验证等领域产生了显著影响，推动了相关领域的研究进展。

当前挑战

该数据集在构建和应用过程中面临的挑战主要包括：1）领域问题挑战，即如何在复杂多变的现实世界规划任务中，利用大型语言模型生成既符合用户需求又满足逻辑一致性的规划；2）构建挑战，包括如何设计有效的数据收集和验证流程，确保数据集的质量和多样性，以及如何处理不满足条件的规划，即不可满足规划修复问题。这些挑战要求研究人员在模型设计、数据处理和算法优化等方面进行深入探索和创新。

常用场景

经典使用场景

在智能规划与调度领域，UnsatChristmas数据集被广泛应用于检验大型语言模型在处理实际世界规划任务时的严谨性与有效性。该数据集提供了一个独特的视角，即通过形式化验证工具对规划进行严格的评估。

解决学术问题

UnsatChristmas数据集解决了学术研究中如何评估和提升大型语言模型在实际世界规划任务中的表现这一关键问题。其通过提供一系列不可满足的规划案例，促使研究者在模型无法生成有效规划时进行修复，从而推动了规划算法的鲁棒性和适应性的研究。

衍生相关工作

基于UnsatChristmas数据集，研究者们衍生出了一系列相关工作，包括对大型语言模型进行改进以更好地处理不可满足的规划案例，以及开发新的形式化验证方法来评估规划任务的解决方案。这些研究进一步推动了智能规划领域的发展。