{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T20:19:31Z","timestamp":1783369171306,"version":"3.54.6"},"reference-count":43,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Polish National Centre for Research and Development","award":["INFOSTRATEG4\/0003\/2022"],"award-info":[{"award-number":["INFOSTRATEG4\/0003\/2022"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2026]]},"DOI":"10.1109\/access.2026.3706430","type":"journal-article","created":{"date-parts":[[2026,6,23]],"date-time":"2026-06-23T19:46:19Z","timestamp":1782243979000},"page":"98311-98327","source":"Crossref","is-referenced-by-count":0,"title":["Integrating Expert Knowledge Into Logical Programs via LLMs"],"prefix":"10.1109","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-3555-1669","authenticated-orcid":false,"given":"Franciszek","family":"G\u00f3rski","sequence":"first","affiliation":[{"name":"Multimedia Systems Department, Gdańsk University of Technology, Gdańsk, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7053-4919","authenticated-orcid":false,"given":"Oskar","family":"Wysocki","sequence":"additional","affiliation":[{"name":"Idiap Research Institute, Martigny, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9959-8385","authenticated-orcid":false,"given":"Marco","family":"Valentino","sequence":"additional","affiliation":[{"name":"University of Sheffield, Western Bank, Sheffield, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andre","family":"Freitas","sequence":"additional","affiliation":[{"name":"Idiap Research Institute, Martigny, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9159-8658","authenticated-orcid":false,"given":"Andrzej","family":"Czy\u017cewski","sequence":"additional","affiliation":[{"name":"Multimedia Systems Department, Gdańsk University of Technology, Gdańsk, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.naacl-long.416"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.findings-emnlp.248"},{"key":"ref3","article-title":"LLM-ARC: Enhancing LLMs with an automated reasoning critic","author":"Kalyanpur","year":"2024","journal-title":"arXiv:2406.17663"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.findings-acl.138"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.acl-long.720"},{"key":"ref6","article-title":"The LLAMA 3 herd of models","author":"Grattafiori","year":"2024","journal-title":"arXiv:2407.21783"},{"key":"ref7","article-title":"Gemma 3 technical report","volume-title":"arXiv:2503.19786","author":"Team","year":"2025"},{"key":"ref8","volume-title":"Codestral: Hello, World!, 2024","author":"Mistral","year":"2024"},{"key":"ref9","article-title":"Qwen2.5-coder technical report","volume-title":"arXiv:2409.12186","author":"Hui","year":"2024"},{"key":"ref10","article-title":"Multi-agent verification: Scaling test-time compute with multiple verifiers","author":"Lifshitz","year":"2025","journal-title":"arXiv:2502.20379"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.29007\/2n9m"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.emnlp-main.313"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.emnlp-main.128"},{"key":"ref14","article-title":"RuleArena: A benchmark for rule-guided reasoning with LLMs in real-world scenarios","author":"Zhou","year":"2024","journal-title":"arXiv:2412.08972"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.naacl-long.52"},{"key":"ref16","article-title":"Improving LLM reasoning through scaling inference computation with collaborative verification","author":"Liang","year":"2024","journal-title":"arXiv:2410.05318"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2025.findings-acl.18"},{"key":"ref18","article-title":"Improve mathematical reasoning in language models by automated process supervision","author":"Luo","year":"2024","journal-title":"arXiv:2406.06592"},{"key":"ref19","article-title":"Logic agent: Enhancing validity with logic rule invocation","author":"Liu","year":"2024","journal-title":"arXiv:2404.18130"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2025.naacl-long.371"},{"key":"ref21","first-page":"217","article-title":"Inference to the best explanation in large language models","volume-title":"Proc. 62nd Annu. Meeting Assoc. Comput. Linguistics","author":"Dalal"},{"key":"ref22","first-page":"2933","article-title":"Verification and refinement of natural language explanations through LLM-symbolic theorem proving","volume-title":"Proc. Conf. Empirical Methods Natural Lang. Process.","author":"Quan"},{"key":"ref23","first-page":"1","article-title":"Enhancing ethical explanations of large language models through iterative symbolic refinement","volume-title":"Proc. 18th Conf. Eur. Chapter Assoc. Comput. Linguistics","author":"Quan"},{"key":"ref24","first-page":"1505","article-title":"A symbolic framework for evaluating mathematical reasoning and generalisation with transformers","volume-title":"Proc. Conf. North Amer. Chapter Assoc. Comput. Linguistics, Human Lang. Technol.","author":"Meadows"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v39i23.34668"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/MedAI59581.2023.00044"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.findings-emnlp.996"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.acl-long.531"},{"key":"ref29","article-title":"Lemur: Integrating large language models in automated program verification","author":"Wu","year":"2023","journal-title":"arXiv:2310.04870"},{"key":"ref30","article-title":"Language models can be logical solvers","author":"Feng","year":"2023","journal-title":"arXiv:2311.06158"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.findings-naacl.254"},{"key":"ref32","article-title":"Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks","author":"Chen","year":"2022","journal-title":"arXiv:2211.12588"},{"key":"ref33","article-title":"Leveraging LLMs for hypothetical deduction in logical inference: A neuro-symbolic approach","author":"Li","year":"2024","journal-title":"arXiv:2410.21779"},{"key":"ref34","article-title":"COAST: Enhancing the code debugging ability of LLMs through communicative agent based data synthesis","author":"Yang","year":"2024","journal-title":"arXiv:2408.05006"},{"key":"ref35","article-title":"Are your LLMs capable of stable reasoning?","author":"Liu","year":"2024","journal-title":"arXiv:2412.13147"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2025.acl-long.390"},{"key":"ref37","article-title":"Not all votes count! Programs as verifiers improve self-consistency of language models for math reasoning","author":"Toh","year":"2024","journal-title":"arXiv:2410.12608"},{"key":"ref38","article-title":"Beyond accuracy: Evaluating self-consistency of code large language models with IdentityChain","author":"Min","year":"2023","journal-title":"arXiv:2310.14053"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v39i24.34717"},{"key":"ref40","article-title":"Model editing for LLMs4Code: How far are we?","author":"Li","year":"2024","journal-title":"arXiv:2411.06638"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.emnlp-main.859"},{"key":"ref42","article-title":"Goedel-prover: A frontier model for open-source automated theorem proving","author":"Lin","year":"2025","journal-title":"arXiv:2502.07640"},{"key":"ref43","article-title":"Theorem prover as a judge for synthetic data generation","author":"Ong Jun Leang","year":"2025","journal-title":"arXiv:2502.13137"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/6287639\/11323511\/11575577.pdf?arnumber=11575577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T19:50:49Z","timestamp":1783367449000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11575577\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":43,"URL":"https:\/\/doi.org\/10.1109\/access.2026.3706430","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]}}}