用最小不可满足核心定位翻译错误，让模型不再胡编乱造答案。
From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving
- 生成程序不满足时，提取模型自身约束的最小不可满足核心
- 将虚假答案率从79%降至7%，显著减少胡编现象
- 适合需要可靠证明和防伪造的符号推理场景
让语言模型可靠求解约束问题，通常需将其转化为形式化规范并交由可信求解器处理。但翻译过程本身依赖语言模型，若翻译失真，求解器将正确求解错误问题。现有方法仅修复导致崩溃的翻译，对运行却错误的程序则无能为力。本文提出以‘证明’替代错误信息：当生成程序不可满足时，提取模型自身约束下的最小不可满足核心，并返回无法共存的具体约束集，实现故障精准定位。在包含77个问题的新基准上，对答案集编程的翻译在七个领域中有六个准确，仅在聚合覆盖率调度任务失败，且该失败集中于可诊断模式。相比仅返回错误信息，最小核心能有效阻止弱模型虚构解，使虚构率从79%降至7%。强链式思维基线虽达相同准确率，但符号路径的价值不在于精度，而在于提供可验证证明与拒绝虚构的能力。
原文摘要 · Abstract (English)
Making language models solve constraint problems reliably often means having them translate the problem into a formal specification and delegating the search to a sound solver. But the translation is itself a language-model task, and an unfaithful translation makes the solver faithfully solve the wrong problem. Existing pipelines repair only translations that crash, returning the solver's error message and falling silent when the program runs but is wrong. We replace the error message with a proof: when the generated program is unsatisfiable, we extract a minimal unsatisfiable core over the model's own constraints and hand it back the exact set that cannot hold together, a leakage-free signal that localizes the fault. On a new benchmark of 77 problems with an exact oracle, translation to Answer Set Programming is faithful on six of seven domains and fails only on aggregate coverage scheduling, which concentrates the translation tax in one diagnosable pattern. A minimal core, rather than a bare error, is what stops a weaker model from fabricating solutions to infeasible problems, cutting fabrication from 79% to 7%. A strong chain-of-thought baseline meanwhile matches the symbolic route on accuracy, so the route's value is not accuracy but certificates and its refusal to fabricate.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。