Formal Reasoning for Intelligent QA Systems: A Case Study in the Educational Domain
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912587362336768 |
|---|---|
| author | Bui, Tuan Nguyen, An Thai, Phat Hua, Minh N., Ngan Pham L. B., Ngan Pham T. Le, Dung Nguyen, Long Tran, Thanh-Tung Bui, Thang Quan, Tho |
| author_facet | Bui, Tuan Nguyen, An Thai, Phat Hua, Minh N., Ngan Pham L. B., Ngan Pham T. Le, Dung Nguyen, Long Tran, Thanh-Tung Bui, Thang Quan, Tho |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_11572 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Reasoning for Intelligent QA Systems: A Case Study in the Educational Domain Bui, Tuan Nguyen, An Thai, Phat Hua, Minh N., Ngan Pham L. B., Ngan Pham T. Le, Dung Nguyen, Long Tran, Thanh-Tung Bui, Thang Quan, Tho Artificial Intelligence Computation and Language 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. |
| title | Formal Reasoning for Intelligent QA Systems: A Case Study in the Educational Domain |
| topic | Artificial Intelligence Computation and Language |
| url | https://arxiv.org/abs/2509.11572 |