用神经符号方法解释数独类谜题的解题步骤，融合逻辑推理与语言模型优势。
Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions
- 结合SAT求解器与大语言模型，分阶段生成决策解释
- 在数独类谜题中实现可解释的逐步推理过程
- 适合需要透明决策过程的研究者与教育场景
我们提出一种神经符号方法，用于解释复杂决策序列，结合了决策程序与大语言模型（LLM）的优势。以数独类谜题Hitori为例，其规则包含局部约束（可用简短证明解释）和连通性约束（更适合视觉化说明）。因此，Hitori成为融合SAT求解器与LLM的灵活组合的理想测试平台。我们实现了一款辅助人类解谜的工具，并通过实验验证了其有效性。
原文摘要 · Abstract (English)
We propose a neurosymbolic approach to the explanation of complex sequences of decisions that combines the strengths of decision procedures and Large Language Models (LLMs). We demonstrate this approach by producing explanations for the solutions of Hitori puzzles. The rules of Hitori include local constraints that are effectively explained by short resolution proofs. However, they also include a connectivity constraint that is more suitable for visual explanations. Hence, Hitori provides an excellent testing ground for a flexible combination of SAT solvers and LLMs. We have implemented a tool that assists humans in solving Hitori puzzles, and we present experimental evidence of its effectiveness.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。