假设前沿：验证器引导的大语言模型与符号搜索用于一阶归纳
Hypothesis Frontier: Verifier Guided LLM and Symbolic Search for First-Order Induction
浏览论文内容
中文总结 AI 辅助
本研究提出Hypothesis Frontier框架，结合LLM与符号搜索，在匹配条件下比重复原始提示生成解决更多一阶归纳问题，还可简化所得公式。
中文摘要 AI 辅助
一阶概念合成要求系统推导一个公式，使其在多个有限关系结构中一致地对带标签对象进行分类。每个候选公式都可被精确评估，但量化一阶公式构成庞大搜索空间，且大语言模型（LLM）的输出常语义上有前景却不完全正确。我们提出Hypothesis Frontier，这是一个验证器引导的神经符号框架，它在每个训练对象上评估每个LLM公式，在多轮中保留最强的已验证假设，并利用其剩余错误指导后续生成。符号处理修复无效公式，同时仍锚定LLM生成的假设，且在不改变任何训练预测的情况下简化训练-验证公式。在匹配模型、问题集和LLM轮次预算的条件下，Hypothesis Frontier比重复的原始提示生成解决了多得多的问题。在选择最终公式后，精确简化缩短了许多训练-验证公式，同时保留所有训练预测。因此，精确符号推理既有助于解决更多归纳问题，又能压缩许多所得公式。
英文摘要
First-order concept synthesis asks a system to infer one formula that classifies labeled objects consistently across several finite relational structures. Every candidate can be evaluated exactly, but quantified first-order formulas form a vast search space, and LLM outputs are often semantically promising without being fully correct. We introduce Hypothesis Frontier, a verifier-guided neurosymbolic framework that evaluates each LLM formula on every training object, retains the strongest verified hypothesis across rounds, and uses its remaining errors to guide subsequent generation. Symbolic processing repairs invalid formulas while remaining anchored to the LLM-generated hypothesis, and simplifies train-valid formulas without changing any training prediction. Under matched models, problem sets, and LLM-round budgets, Hypothesis Frontier solves substantially more problems than repeated original-prompt generation. After the final formulas are selected, exact simplification shortens many train-valid formulas while preserving every training prediction. Exact symbolic reasoning therefore helps both to solve more induction problems and to compress many of the resulting formulas.
