Hypothesis Frontier：验证器引导的大语言模型与符号搜索求解一阶归纳

一阶概念合成要求系统推断出一个公式，使其在多个有限关系结构上都能一致地对带标注对象进行分类。每个候选公式都可以被精确评估，但带量词的一阶公式构成巨大的搜索空间，且大语言模型（LLM）的输出常常语义上有希望却并不完全正确。我们提出Hypothesis Frontier，一个验证器引导的神经符号框架，它在每个训练对象上评估每个LLM公式，跨轮次保留最强的已验证假设，并利用其剩余错误引导后续生成。符号处理在保持锚定于LLM所生成假设的前提下修复无效公式，并在不改变任何训练预测的情况下简化训练有效公式。在匹配的模型、问题集和LLM轮次预算下，Hypothesis Frontier求解的问题显著多于重复原始提示词生成。在最终公式选定后，精确简化可在保留每条训练预测的同时缩短许多训练有效公式。因此，精确符号推理既有助于求解更多归纳问题，也有助于压缩所得的许多公式。