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

LLM在程序合成方面取得了令人瞩目的成功，能够发现超越既有解的程序。然而，这些方法依赖简单的数值分数来表示程序质量，例如解的取值或通过的测试数量。由于分数无法说明程序失败的原因，系统必须生成并评估大量候选、寄希望于其中某些成功，从而推高LLM推理与评估成本。我们研究另一种方法：属性引导的LLM程序合成。我们不是在评估后给程序打分，而是检查候选是否满足一个形式化定义的属性。当属性被违反时，我们提前终止评估，并向LLM提供一个具体反例，精确展示程序是如何失败的。这种反馈大幅减少了程序生成次数与评估成本，并能引导LLM生成更强的程序。我们在PDDL规划域上评估该方法，要求LLM合成直接启发式函数：每个通过严格改进转移可达的状态都存在一个严格改进的后继。具有该属性的启发式能引导爬山算法直达目标状态。反例引导的修复循环生成一个候选程序，在训练集上检查该属性，并返回第一个违反属性的用例。我们在十个规划域上用分布外测试集评估该方法。合成的启发式在几乎所有测试任务上都是有效的直接启发式；与最佳的先前生成方法相比，我们的方法平均每域少生成7倍的程序，在不使用搜索的情况下解决更多任务，且评估候选所需的计算量低几个数量级。只要问题存在可验证的属性，属性引导的LLM合成就能降低成本并提升程序质量。