{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:31Z","timestamp":1784797591383,"version":"3.55.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we launched\n                    <jats:sc>Automated Reasoning checks\u00a0(ARc)<\/jats:sc>\n                    : a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies.\n                    <jats:sc>ARc<\/jats:sc>\n                    performs multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that\n                    <jats:sc>ARc<\/jats:sc>\n                    exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text.\n                    <jats:sc>ARc<\/jats:sc>\n                    is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_28","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:46:50Z","timestamp":1784796410000},"page":"601-617","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Neurosymbolic Approach to\u00a0Natural Language Formalization and\u00a0Verification"],"prefix":"10.1007","author":[{"given":"Chenyang","family":"An","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sam","family":"Bayless","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefano","family":"Buliani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Darion","family":"Cassel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Duncan","family":"Clough","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00e9mi","family":"Delmas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nafi","family":"Diallo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ferhat","family":"Erata","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nick","family":"Feng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aman","family":"Goel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aditya","family":"Gokhale","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joe","family":"Hendrix","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Victor","family":"Heorhiadi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"Hudak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dejan","family":"Jovanovi\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew M.","family":"Kent","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin","family":"Kiesl-Reiter","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeffrey J.","family":"Kuna","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nadia","family":"Labai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Lilien","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Divya","family":"Raghunathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niloofar","family":"Razavi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ali","family":"Torkamani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nathaniel","family":"Weir","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianan","family":"Yao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"28_CR1","unstructured":"Amazon Web Services: Amazon logistics automates electric vehicle design reviews on AWS. https:\/\/aws.amazon.com\/solutions\/case-studies\/amazon-logistics-case-study\/ (2025). Accessed 01 May 2026"},{"key":"28_CR2","unstructured":"An, C., et al.: A neurosymbolic approach to natural language formalization and verification (extended version) (2026). https:\/\/arxiv.org\/abs\/2511.09008"},{"key":"28_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"issue":"12","key":"28_CR4","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczy\u0144ski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011). https:\/\/doi.org\/10.1145\/2043174.2043195","journal-title":"Commun. ACM"},{"key":"28_CR5","doi-asserted-by":"publisher","unstructured":"Callewaert, B., Vandevelde, S., Vennekens, J.: VERUS-LM: a versatile framework for combining LLMs with symbolic reasoning. In: Gebser, M., Inclezan, D., Ricca, F., Carro, M., Truszczynski, M. (eds.) Proceedings 41st International Conference on Logic Programming, ICLP 2025, Rende, Italy, 12\u201319th September 2025, pp. 47\u201362. EPTCS (2025). https:\/\/doi.org\/10.4204\/EPTCS.439.5","DOI":"10.4204\/EPTCS.439.5"},{"key":"28_CR6","unstructured":"Carbonnelle, P., Vandevelde, S., Vennekens, J., Denecker, M.: Interactive configurator with fo (.) and idp-z3 (2022). arXiv preprint arXiv:2202.00343"},{"key":"28_CR7","doi-asserted-by":"publisher","unstructured":"Casadio, M., et al.: NLP verification: towards a general methodology for certifying robustness. Eur. J. Appl. Math. 37(1), 180\u2013237 (2026). https:\/\/doi.org\/10.1017\/S0956792525000099","DOI":"10.1017\/S0956792525000099"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"Ganguly, D., Iyengar, S., Chaudhary, V., Kalyanaraman, S.: Proof of thought : neurosymbolic program synthesis allows robust and interpretable reasoning. CoRR abs\/2409.17270 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2409.17270","DOI":"10.48550\/ARXIV.2409.17270"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"Haltaufderheide, J., Ranisch, R.: The ethics of chatgpt in medicine and healthcare: a systematic review on large language models (LLMs). npj Digit. Med. 7(1), (2024). https:\/\/doi.org\/10.1038\/S41746-024-01157-X","DOI":"10.1038\/S41746-024-01157-X"},{"key":"28_CR10","doi-asserted-by":"publisher","unstructured":"Han, S., Liu, T., Li, C., Xiong, X., Cohan, A.: HYBRIDMIND: meta selection of natural language and symbolic language for enhanced LLM reasoning. arXiv e-prints arXiv:2409.19381 (2024). https:\/\/doi.org\/10.48550\/arXiv.2409.19381","DOI":"10.48550\/arXiv.2409.19381"},{"key":"28_CR11","doi-asserted-by":"publisher","unstructured":"Han, S., et al.: FOLIO: natural language reasoning with first-order logic. In: Al-Onaizan, Y., Bansal, M., Chen, Y. (eds.) Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Miami, FL, USA, 12\u201316 November 2024, pp. 22017\u201322031. Association for Computational Linguistics (2024). https:\/\/doi.org\/10.18653\/V1\/2024.EMNLP-MAIN.1229","DOI":"10.18653\/V1\/2024.EMNLP-MAIN.1229"},{"key":"28_CR12","doi-asserted-by":"publisher","unstructured":"Hitzler, P., Sarker, M.K. (eds.): Neuro-Symbolic Artificial Intelligence: The State of the Art, Frontiers in Artificial Intelligence and Applications, vol. 342. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA342","DOI":"10.3233\/FAIA342"},{"key":"28_CR13","doi-asserted-by":"publisher","unstructured":"Hu, X., et al.: Knowledge-centric hallucination detection. In: Al-Onaizan, Y., Bansal, M., Chen, Y.N. (eds.) Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp. 6953\u20136975. Association for Computational Linguistics, Miami, Florida, USA (2024). https:\/\/doi.org\/10.18653\/v1\/2024.emnlp-main.395, https:\/\/aclanthology.org\/2024.emnlp-main.395\/","DOI":"10.18653\/v1\/2024.emnlp-main.395"},{"key":"28_CR14","unstructured":"ICME: AI agents can move money - Lobstar & Wilde proved they can lose it too. https:\/\/blog.icme.io\/ai-agents-can-move-money-lobstar-wilde-proved-they-can-lose-it-too\/ (2026). Accessed 01 May 2026"},{"key":"28_CR15","doi-asserted-by":"publisher","unstructured":"Ishay, A., Yang, Z., Lee, J.: Leveraging large language models to generate answer set programs. In: Marquis, P., Son, T.C., Kern-Isberner, G. (eds.) Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, KR 2023, Rhodes, Greece, 2\u20138 September 2023, pp. 374\u2013383 (2023). https:\/\/doi.org\/10.24963\/KR.2023\/37","DOI":"10.24963\/KR.2023\/37"},{"key":"28_CR16","doi-asserted-by":"publisher","unstructured":"Jacovi, A., et al.: The FACTS grounding leaderboard: benchmarking LLMs\u2019 ability to ground responses to long-form input. CoRR abs\/2501.03200 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2501.03200","DOI":"10.48550\/ARXIV.2501.03200"},{"key":"28_CR17","unstructured":"Jiang, A.Q., et al.: Draft, sketch, and prove: guiding formal theorem provers with informal proofs. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, 1\u20135 May 2023. OpenReview.net (2023). https:\/\/openreview.net\/forum?id=SMa9EAovKMC"},{"key":"28_CR18","unstructured":"Labs, B.: Bespoke-minicheck-7b (2024). https:\/\/huggingface.co\/bespokelabs\/Bespoke-MiniCheck-7B"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Levy, M., Jacoby, A., Goldberg, Y.: Same task, more tokens: the impact of input length on the reasoning performance of large language models. In: Ku, L., Martins, A., Srikumar, V. (eds.) Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2024, Bangkok, Thailand, 11\u201316 August 2024, pp. 15339\u201315353. Association for Computational Linguistics (2024). https:\/\/doi.org\/10.18653\/V1\/2024.ACL-LONG.818","DOI":"10.18653\/V1\/2024.ACL-LONG.818"},{"key":"28_CR20","unstructured":"Lewis, P., et al.: Retrieval-augmented generation for knowledge-intensive NLP tasks (2021). https:\/\/arxiv.org\/abs\/2005.11401"},{"key":"28_CR21","doi-asserted-by":"publisher","unstructured":"Liu, T., et al.: Logic-of-thought: injecting logic into contexts for full reasoning in large language models. In: Chiruzzo, L., Ritter, A., Wang, L. (eds.) Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), pp. 10168\u201310185. Association for Computational Linguistics, Albuquerque, New Mexico (2025). https:\/\/doi.org\/10.18653\/v1\/2025.naacl-long.510, https:\/\/aclanthology.org\/2025.naacl-long.510\/","DOI":"10.18653\/v1\/2025.naacl-long.510"},{"key":"28_CR22","doi-asserted-by":"publisher","unstructured":"Manakul, P., Liusie, A., Gales, M.J.F.: SelfCheckGPT: zero-resource black-box hallucination detection for generative large language models. In: Bouamor, H., Pino, J., Bali, K. (eds.) Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, EMNLP 2023, Singapore, 6\u201310 December 2023, pp. 9004\u20139017. Association for Computational Linguistics (2023). https:\/\/doi.org\/10.18653\/V1\/2023.EMNLP-MAIN.557","DOI":"10.18653\/V1\/2023.EMNLP-MAIN.557"},{"key":"28_CR23","unstructured":"McCune, W.: Release of prover9. In: Mile High Conference On Quasigroups, Loops and Nonassociative Systems, Denver, Colorado (2005)"},{"key":"28_CR24","doi-asserted-by":"publisher","unstructured":"Merigoux, D., Chataing, N., Protzenko, J.: Catala: a programming language for the law. Proc. ACM Program. Lang. 5(ICFP), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3473582","DOI":"10.1145\/3473582"},{"key":"28_CR25","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp. 337\u2013340. Lecture Notes in Computer Science, Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"28_CR26","doi-asserted-by":"publisher","unstructured":"Olausson, T., et al.: LINC: a neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In: Bouamor, H., Pino, J., Bali, K. (eds.) Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 5153\u20135176. Association for Computational Linguistics, Singapore (2023). https:\/\/doi.org\/10.18653\/v1\/2023.emnlp-main.313, https:\/\/aclanthology.org\/2023.emnlp-main.313\/","DOI":"10.18653\/v1\/2023.emnlp-main.313"},{"key":"28_CR27","doi-asserted-by":"publisher","unstructured":"Pan, L., Albalak, A., Wang, X., Wang, W.: Logic-LM: empowering large language models with symbolic solvers for faithful logical reasoning. In: Bouamor, H., Pino, J., Bali, K. (eds.) Findings of the Association for Computational Linguistics: EMNLP 2023, pp. 3806\u20133824. Association for Computational Linguistics, Singapore (2023). https:\/\/doi.org\/10.18653\/v1\/2023.findings-emnlp.248, https:\/\/aclanthology.org\/2023.findings-emnlp.248\/","DOI":"10.18653\/v1\/2023.findings-emnlp.248"},{"key":"28_CR28","unstructured":"PwC Australia: Operationalising responsible AI in education: Automated reasoning and deterministic guardrails on AWS. https:\/\/www.pwc.com.au\/alliances\/amazon-web-services\/operationalising-responsible-ai-in-education.html (2026). Accessed 01 May 2026"},{"key":"28_CR29","doi-asserted-by":"publisher","unstructured":"Rajeev, M.A., et al.: Cats confuse reasoning LLM: query agnostic adversarial triggers for reasoning models. CoRR abs\/2503.01781 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2503.01781","DOI":"10.48550\/ARXIV.2503.01781"},{"key":"28_CR30","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001). https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"key":"28_CR31","unstructured":"Ryu, H., Kim, G., Lee, H.S., Yang, E.: Divide and translate: compositional first-order logic translation and verification for complex logical reasoning. In: The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, 24\u201328 April 2025. OpenReview.net (2025). https:\/\/openreview.net\/forum?id=09FiNmvNMw"},{"key":"28_CR32","doi-asserted-by":"publisher","unstructured":"Sun, H., Cohen, W.W., Salakhutdinov, R.: Conditionalqa: a complex reading comprehension dataset with conditional answers. In: Muresan, S., Nakov, P., Villavicencio, A. (eds.) Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2022, Dublin, Ireland, 22\u201327 May 2022, pp. 3627\u20133637. Association for Computational Linguistics (2022). https:\/\/doi.org\/10.18653\/V1\/2022.ACL-LONG.253","DOI":"10.18653\/V1\/2022.ACL-LONG.253"},{"key":"28_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53518-6_1","volume-title":"Intelligent Computer Mathematics","author":"C Szegedy","year":"2020","unstructured":"Szegedy, C.: A promising path towards autoformalization and general artificial intelligence. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_1"},{"key":"28_CR34","doi-asserted-by":"publisher","unstructured":"Tafjord, O., Dalvi, B., Clark, P.: Proofwriter: generating implications, proofs, and abductive statements over natural language. In: Zong, C., Xia, F., Li, W., Navigli, R. (eds.) Findings of the Association for Computational Linguistics: ACL\/IJCNLP 2021, Online Event, 1\u20136 August 2021, pp. 3621\u20133634. Findings of ACL, Association for Computational Linguistics (2021). https:\/\/doi.org\/10.18653\/V1\/2021.FINDINGS-ACL.317","DOI":"10.18653\/V1\/2021.FINDINGS-ACL.317"},{"key":"28_CR35","doi-asserted-by":"publisher","unstructured":"Tang, L., Laban, P., Durrett, G.: Minicheck: efficient fact-checking of LLMs on grounding documents. In: Al-Onaizan, Y., Bansal, M., Chen, Y. (eds.) Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Miami, FL, USA, 12\u201316 November 2024, pp. 8818\u20138847. Association for Computational Linguistics (2024). https:\/\/doi.org\/10.18653\/V1\/2024.EMNLP-MAIN.499","DOI":"10.18653\/V1\/2024.EMNLP-MAIN.499"},{"key":"28_CR36","doi-asserted-by":"publisher","unstructured":"Tian, J., Li, Y., Chen, W., Xiao, L., He, H., Jin, Y.: Diagnosing the first-order logical reasoning ability through logicnli. In: Moens, M., Huang, X., Specia, L., Yih, S.W. (eds.) Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, EMNLP 2021, Virtual Event \/ Punta Cana, Dominican Republic, 7\u201311 November, 2021, pp. 3738\u20133747. Association for Computational Linguistics (2021). https:\/\/doi.org\/10.18653\/V1\/2021.EMNLP-MAIN.303","DOI":"10.18653\/V1\/2021.EMNLP-MAIN.303"},{"key":"28_CR37","doi-asserted-by":"publisher","unstructured":"Wang, Q., Kaliszyk, C., Urban, J.: First experiments with neural translation of informal to formal mathematics. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, 13\u201317 August 2018, Proceedings. pp. 255\u2013270. Lecture Notes in Computer Science, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_22","DOI":"10.1007\/978-3-319-96812-4_22"},{"key":"28_CR38","doi-asserted-by":"publisher","unstructured":"Wang, Y., et al.: Factcheck-bench: fine-grained evaluation benchmark for automatic fact-checkers. In: Al-Onaizan, Y., Bansal, M., Chen, Y.N. (eds.) Findings of the Association for Computational Linguistics: EMNLP 2024, pp. 14199\u201314230. Association for Computational Linguistics, Miami, Florida, USA (2024). https:\/\/doi.org\/10.18653\/v1\/2024.findings-emnlp.830, https:\/\/aclanthology.org\/2024.findings-emnlp.830\/","DOI":"10.18653\/v1\/2024.findings-emnlp.830"},{"key":"28_CR39","doi-asserted-by":"publisher","unstructured":"Wei, J., et al.: Chain-of-thought prompting elicits reasoning in large language models. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022 (2022). https:\/\/doi.org\/10.52202\/068431-1800, http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html","DOI":"10.52202\/068431-1800"},{"key":"28_CR40","doi-asserted-by":"publisher","unstructured":"Wu, Y., et al.: Autoformalization with large language models. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9 (2022). https:\/\/doi.org\/10.52202\/068431-2344, http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html","DOI":"10.52202\/068431-2344"},{"key":"28_CR41","doi-asserted-by":"publisher","unstructured":"Xu, J., Fei, H., Pan, L., Liu, Q., Lee, M.L., Hsu, W.: Faithful logical reasoning via symbolic chain-of-thought. In: Ku, L.W., Martins, A., Srikumar, V. (eds.) Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 13326\u201313365. Association for Computational Linguistics, Bangkok, Thailand (2024). https:\/\/doi.org\/10.18653\/v1\/2024.acl-long.720","DOI":"10.18653\/v1\/2024.acl-long.720"},{"key":"28_CR42","doi-asserted-by":"publisher","unstructured":"Xu, Z., Jain, S., Kankanhalli, M.S.: Hallucination is inevitable: an innate limitation of large language models. CoRR abs\/2401.11817 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.11817","DOI":"10.48550\/ARXIV.2401.11817"},{"key":"28_CR43","doi-asserted-by":"publisher","unstructured":"Yang, Z., Ishay, A., Lee, J.: Coupling large language models with logic programming for robust and general reasoning from text. In: Rogers, A., Boyd-Graber, J.L., Okazaki, N. (eds.) Findings of the Association for Computational Linguistics: ACL 2023, Toronto, Canada, 9\u201314 July 2023, pp. 5186\u20135219. Findings of ACL, Association for Computational Linguistics (2023). https:\/\/doi.org\/10.18653\/V1\/2023.FINDINGS-ACL.321","DOI":"10.18653\/V1\/2023.FINDINGS-ACL.321"},{"key":"28_CR44","doi-asserted-by":"publisher","unstructured":"Yao, S., et al.: Tree of thoughts: Deliberate problem solving with large language models. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, 10\u201316 December 2023 (2023). https:\/\/doi.org\/10.52202\/075280-0517, http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/271db9922b8d1f4dd7aaef84ed5ac703-Abstract-Conference.html","DOI":"10.52202\/075280-0517"},{"key":"28_CR45","doi-asserted-by":"publisher","unstructured":"Ye, X., Chen, Q., Dillig, I., Durrett, G.: Satlm: satisfiability-aided language models using declarative prompting. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, 10\u201316 December 2023 (2023). https:\/\/doi.org\/10.52202\/075280-1974, http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/8e9c7d4a48bdac81a58f983a64aaf42b-Abstract-Conference.html","DOI":"10.52202\/075280-1974"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:46:56Z","timestamp":1784796416000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}