Extracting Verified Action Theories from Informal Specifications via Explanation-Guided Refinement

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.