{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T12:04:45Z","timestamp":1784203485447,"version":"3.55.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,7]]},"abstract":"<jats:p>Acquiring correct action theories from informal specifications remains a central challenge in KR. Large Language Models can generate plausible domain models from natural language, but the resulting theories frequently contain missing preconditions, incorrect effects, or superfluous actions. Existing refinement approaches either require human experts to correct these errors or assume that the input specification is itself correct. We present a fully automated framework that iteratively refines LLM-generated action theories using formal explanations grounded in SAT-based verification. Each candidate theory is encoded as a bounded SAT problem and tested against solvable tasks, which must admit a valid plan, and unsolvable tasks, which must be correctly rejected. When a test fails, we extract a formal explanation that pinpoints the specific theory constraints responsible for the failure, and feed this explanation back to the LLM to guide its next revision. Our initial evaluation across six planning domains shows that our framework can converge to correct theories.<\/jats:p>","DOI":"10.24963\/kr.2026\/108","type":"proceedings-article","created":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:15:53Z","timestamp":1784200553000},"page":"1153-1158","source":"Crossref","is-referenced-by-count":0,"title":["Extracting Verified Action Theories from Informal Specifications via Explanation-Guided Refinement"],"prefix":"10.24963","author":[{"given":"Stylianos Loukas","family":"Vasileiou","sequence":"first","affiliation":[{"name":"New Mexico State University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Minh","family":"Nguyen","sequence":"additional","affiliation":[{"name":"New Mexico State University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tran Cao","family":"Son","sequence":"additional","affiliation":[{"name":"New Mexico State University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huiping","family":"Cao","sequence":"additional","affiliation":[{"name":"New Mexico State University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrico","family":"Pontelli","sequence":"additional","affiliation":[{"name":"New Mexico State University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"10584","event":{"name":"23nd International Conference on Principles of Knowledge Representation and Reasoning {KR-2026}","theme":"Artificial Intelligence","location":"Lisbon, Portuagal","acronym":"KR-2026","number":"23","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","European Association for Artificial Intelligence"],"start":{"date-parts":[[2026,7,20]]},"end":{"date-parts":[[2026,7,18]]}},"container-title":["Proceedings of the TwentyThird International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:16:22Z","timestamp":1784200582000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2026\/108"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2026\/108","relation":{},"subject":[],"published":{"date-parts":[[2026,7]]}}}