Large Language Models (LLMs) are capable of transforming natural language
domain descriptions into plausibly looking PDDL markup. However, ensuring that
actions are consistent within domains still remains a challenging task. In this
paper we present a novel concept to significantly improve the quality of
LLM-generated PDDL models by performing automated consistency checking during
the generation process. Although the proposed consistency checking strategies
still can't guarantee absolute correctness of generated models, they can serve
as valuable source of feedback reducing the amount of correction efforts
expected from a human in the loop. We demonstrate the capabilities of our error
detection approach on a number of classical and custom planning domains
(logistics, gripper, tyreworld, household, pizza).

用自动一致性检查策略显著改善由大型语言模型生成的 PDDL 模型的质量，并减少后续纠正工作的人力投入。

使用大型语言模型生成一致的 PDDL 领域

Generating consistent PDDL domains with Large Language Models

The use of large language models for code generation is a rapidly growing
trend in software development. However, without effective methods for ensuring
the correctness of generated code, this trend could lead to any number of
undesirable outcomes. In this paper, we lay out a vision for addressing this
challenge: the Clover paradigm, short for Closed-Loop Verifiable Code
Generation, which reduces correctness checking to the more accessible problem
of consistency checking. At the core of Clover lies a checker that performs
consistency checks among code, docstrings, and formal annotations. The checker
is implemented using a novel integration of formal verification tools and large
language models. We provide a theoretical analysis to support our thesis that
Clover should be effective at consistency checking. We also empirically
investigate its feasibility on a hand-designed dataset (CloverBench) featuring
annotated Dafny programs at a textbook level of difficulty. Experimental
results show that for this dataset, (i) LLMs are reasonably successful at
automatically generating formal specifications; and (ii) our consistency
checker achieves a promising acceptance rate (up to 87%) for correct instances
while maintaining zero tolerance for incorrect ones (no false positives).

大语言模型用于代码生成是软件开发中的一个快速增长的趋势，本文提出了一个名为 Clover 的闭环可验证代码生成范式，它通过将正确性检查简化为一致性检查的问题来解决这个挑战，并使用形式验证工具和大语言模型的新型集成方法来实现一致性检查。

Clover: 闭环可验证代码生成

Clover: Closed-Loop Verifiable Code Generation

In answer set programming, inconsistencies arise when the constraints placed
on a program become unsatisfiable. In this paper, we introduce a technique for
dynamic consistency checking for our goal-directed method for computing answer
sets, under which only those constraints deemed relevant to the partial answer
set are tested, allowing inconsistent knowledgebases to be successfully
queried. However, the algorithm guarantees that, if a program has at least one
consistent answer set, any partial answer set returned will be a subset of some
consistent answer set. To appear in Theory and Practice of Logic Programming
(TPLP).

本文介绍了一种动态一致性检查技术，可以在我们的面向目标的方法中实现计算答案集，只测试与部分答案集相关的约束条件，从而使不一致的知识库能够成功查询。但是，该算法保证，如果一个程序至少有一个一致的答案集，则返回的任何部分答案集都将是一些一致答案集的子集。