| تعداد نشریات | 45 |
| تعداد شمارهها | 1,558 |
| تعداد مقالات | 19,018 |
| تعداد مشاهده مقاله | 64,515,359 |
| تعداد دریافت فایل اصل مقاله | 23,595,724 |
Neuro-Symbolic Reconstruction of Philosophical and Formal Arguments: Automated Propositional Mapping and Verdict Verification via LLMs and SMT Solvers | ||
| مجله پژوهش های فلسفی | ||
| مقاله 49، دوره 20، شماره 56، مهر 1405، صفحه 845-856 اصل مقاله (1.28 M) | ||
| نوع مقاله: مقاله علمی- پژوهشی | ||
| شناسه دیجیتال (DOI): 10.22034/jpiut.2026.22498 | ||
| نویسندگان | ||
| آریان اسماعیلی نسب1؛ امیر امین زاده قوی فکر* 2 | ||
| 1گروه مهندسی کنترل، دانشگاه تبریز، تبریز، ایران. | ||
| 2استادیار گروه مهندسی کنترل، دانشگاه تبریز، تبریز، ایران | ||
| چکیده | ||
| “To test whether an end-to-end neuro-symbolic pipeline (deterministic segmentation, LLM formalisation into SMT-LIB2, automated symbolic repair, and three-way Z3 SMT verification with countermodel generation) can reconstruct classical philosophical arguments, and to quantify where scaling changes the character of formalisation failures.” Five-stage pipeline evaluated on 31 curated philosophical and explicit-logic arguments plus the full 204-item FOLIO validation split under a three-way protocol, replicated across three independently pinned backends (Qwen3-4B-Instruct; Gemini 3.8 Flash; Nemotron-3-Ultra-550B). An independent audit script re-derives every reported number from the archived raw records. Explicit logic vs. philosophical prose: 68.8%/27.3% (Qwen) and 93.8%/63.6% (Gemini); replicated effect sizes of −41.5 and −30.2 percentage points (Fisher p = 0.054/0.125, not significant for the larger model). Enthymemes: 0.0% vs 50.0%; a warrant-eliciting prompt repairs the barrier only for the larger model (7/11 to 10/11) at a cost on explicit items (8/8 to 6/8). FOLIO: a refutation asymmetry replicates in all three families and decided-item refutation never exceeds 58.1% (36/62); the direct no-solver baseline is 66.7% for the small model. LLMs transcribe fluently but reconstruct poorly; the deficit on classical prose is necessary rather than technical. The pipeline's value is inspectable judgment — solver-checked verdicts, per-stage diagnosis, and countermodels as automated thought experiments. | ||
| کلیدواژهها | ||
| Argument Reconstruction؛ Enthymemes؛ First-order Logic؛ Large Language Models؛ Neuro-Symbolic Systems؛ Z3 SMT solver | ||
| مراجع | ||
|
de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (pp. 337–340). Springer. https://doi.org/10.1007/978-3-540-78800-3_24 Dziri, N., Lu, X., Sclar, M., Li, X. L., Jiang, L., Lin, B. Y., West, P., Bhagavatula, C., Le Bras, R., Hwang, J. D., Sanyal, S., Welleck, S., Ren, X., Ettinger, A., Harchaoui, Z., & Choi, Y. (2023). Faith and fate: Limits of transformers on compositionality. Advances in Neural Information Processing Systems, 36. https://arxiv.org/abs/2305.18654 Frege, G. (1967). Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought (S. Bauer-Mengelberg, Trans.). In J. van Heijenoort (Ed.), From Frege to Gödel: A source book in mathematical logic, 1879–1931 (pp. 1–82). Harvard University Press. (Original work published 1879) Han, S., Schoelkopf, H., Zhao, Y., Qi, Z., Riddell, M., Zhou, W., Coady, J., Peng, D., Qiao, Y., Benson, L., Sun, L., Wardle-Solano, A., Szabó, H., Zubova, E., Burtell, M., Fan, J., Liu, Y., Wong, B., Sailor, M., … Radev, D. (2024). FOLIO: Natural language reasoning with first-order logic. In Proceedings of EMNLP 2024 (pp. 22017–22031). https://doi.org/10.18653/v1/2024.emnlp-main.1229 Nabavi, L., & Mirsanei, S. A. (2026). Paraconsistency, relevance and vagueness: A proof theoretic approach to fuzzy relevant logic FR. Journal of Philosophical Investigations, 20(55), 325–352. https://doi.org/10.22034/jpiut.2026.70950.4391 Olausson, T. X., Gu, A., Lipkin, B., Zhang, C., Solar-Lezama, A., Tenenbaum, J. B., & Levy, R. (2023). LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of EMNLP 2023 (pp. 5153–5176). https://doi.org/10.18653/v1/2023.emnlp-main.313 Pan, L., Albalak, A., Wang, X., & Wang, W. Y. (2023). Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of EMNLP 2023 (pp. 3806–3824). https://doi.org/10.18653/v1/2023.findings-emnlp.248 Saparov, A., & He, H. (2023). Language models are greedy reasoners: A systematic formal analysis of chain-of-thought. In Proceedings of ICLR 2023. https://arxiv.org/abs/2210.01240 Tafjord, O., Dalvi, B., & Clark, P. (2021). ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL 2021 (pp. 3621–3634). Toulmin, S. E. (2003). The uses of argument (Updated ed.). Cambridge University Press. (Original work published 1958) Walton, D., Reed, C., & Macagno, F. (2008). Argumentation schemes. Cambridge University Press. Ye, X., Chen, Q., Dillig, I., & Durrett, G. (2023). SatLM: Satisfiability-aided language models using declarative prompting. Advances in Neural Information Processing Systems, 36. https://arxiv.org/abs/2308.10457 | ||
|
آمار تعداد مشاهده مقاله: 14 تعداد دریافت فایل اصل مقاله: 5 |
||