智能问答系统的形式化推理：教育领域的案例研究
Formal Reasoning for Intelligent QA Systems: A Case Study in the Educational Domain
AI总结：
本文提出MCFR神经符号框架，结合LLMs与模型检查进行属性验证，并引入EduMC-QA基准，显著提升了闭域问答系统的推理忠实度与可解释性。
摘要：
推理对于程序正确性和政策合规性至关重要的闭域QA系统而言是必不可少的。尽管大型语言模型（LLMs）在许多推理任务中表现出色，但最近的研究表明，它们的推理轨迹往往是不忠实的——更多是作为看似合理的解释，而非基于因果的推导。将LLMs与符号引擎（例如，Prover9、Z3）相结合的努力提高了可靠性，但仍局限于静态形式的逻辑，难以处理动态的、基于状态的推理，如多步推进和条件转换。在本文中，我们提出了MCFR（Model Checking for Formal Reasoning，用于形式化推理的模型检查），这是一个将LLMs与模型检查相集成以支持属性验证的神经符号框架。MCFR将自然语言转换为形式化规范，并在转换模型上对其进行验证。为了支持评估，我们引入了EduMC-QA，这是一个基于真实学术程序的基准数据集。我们的结果表明，MCFR提高了推理的忠实度和可解释性，为高风险闭域应用中可验证的QA提供了一条可行的路径。除了评估MCFR外，我们还将其性能与ChatGPT、DeepSeek和Claude等最先进的LLMs进行了比较，以说明其有效性。
英文摘要：
Reasoning is essential for closed-domain QA systems in which procedural correctness and policy compliance are critical. While large language models (LLMs) have shown strong performance on many reasoning tasks, recent work reveals that their reasoning traces are often unfaithful - serving more as plausible justifications than as causally grounded derivations. Efforts to combine LLMs with symbolic engines (e.g., Prover9, Z3) have improved reliability but remain limited to static forms of logic, struggling with dynamic, state-based reasoning such as multi-step progressions and conditional transitions. In this paper, we propose MCFR (Model Checking for Formal Reasoning), a neuro-symbolic framework that integrates LLMs with model checking to support property verification. MCFR translates natural language into formal specifications and verifies them over transition models. To support evaluation, we introduce EduMC-QA, a benchmark dataset grounded in real academic procedures. Our results show that MCFR improves reasoning faithfulness and interpretability, offering a viable path toward verifiable QA in high-stakes closed-domain applications. In addition to evaluating MCFR, we compare its performance with state-of-the-art LLMs such as ChatGPT, DeepSeek, and Claude to contextualize its effectiveness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
