面向规划的属性导向LLM程序合成

LLM在程序合成方面展现了惊人的成功，发现超越先前解决方案的程序。然而，这些方法依赖简单的数字分数来信号程序质量，如解答值或通过的测试数量。由于分数未提供程序失败原因的指导，系统必须生成和评估许多候选程序以期某些成功，从而增加LLM推理和评估成本。我们研究了另一种方法：属性导向LLM程序合成。不在评估后对程序打分，而是检查候选程序是否满足形式化定义的属性。当属性被违反时，我们提前停止评估，并为LLM提供具体的反例，显示程序确切的失败方式。这种反馈显著减少了程序生成次数和评估成本，并可指导LLM生成更强的程序。我们在PDDL规划域上进行评估，要求LLM合成直接启发函数：严格改进过渡可达的每个状态都有一个严格改进的后继。具有此属性的启发函数可直接引导hill-climbing算法到达目标状态。一个以反例为导向的修复循环生成一个候选程序，检查训练集上的属性，然后返回首个违反属性的案例。我们在十个规划域上进行评估，采用脱节测试集。合成的启发函数在几乎所有测试任务上都有效地是直接的，并且与最佳先前生成方法相比，该方法在每个域上平均生成七分之一的程序数、解决更多任务且无需使用搜索，并需评估候选程序的计算成本降低几个数量级。每当问题容许可验证的属性时，属性导向LLM合成都能降低成本并提高程序质量。