从错误到证明：面向神经符号约束求解的最小核引导修复

要让语言模型可靠地求解约束问题，通常做法是让它们把问题翻译为形式化规范，再把搜索委托给可靠的求解器。但翻译本身就是语言模型任务，一次不忠实的翻译会让求解器忠实地解错题。现有流水线只修复会崩溃的翻译：返回求解器的错误信息，而当程序能运行但结果错误时便束手无策。我们用证明取代错误信息：当生成的程序不可满足时，我们在模型自身的约束之上提取最小不可满足核，把恰好无法同时成立的那一组约束交还给模型——这是一个无泄漏且能定位故障的信号。在一个带精确oracle的77个问题的新基准上，到Answer Set Programming的翻译在七个领域中的六个上是忠实的，仅在聚合覆盖调度上失败，从而把翻译税集中到一种可诊断的模式上。正是最小核而非裸错误，阻止了较弱的模型为不可满足的问题捏造解，把捏造率从79%降到7%。与此同时，一个强思维链基线在准确率上与符号路线相当，因此符号路线的价值不在于准确率，而在于证书与拒绝捏造。