NeSyWikiCompiler: A Neural-Symbolic Compiler for Verifiable AI Knowledge Engineering

Abstract

Knowledge rules in AI engineering carry an awkward double duty. A clinician or a compliance officer has to be able to read and revise them, and a downstream system has to be able to execute and check them. Getting from the natural-language version of such a rule to a symbolic program is rarely the hard part; getting to one that is not merely runnable but logically sound is. We call this the compilation gap and attack it with NeSyWikiCompiler, a four-stage neural-symbolic pipeline. A language-model frontend reads each specification into NeSy-IR, an intermediate representation that holds onto exactly the details downstream code generation needs and that language models routinely drop: predicate types, the direction of numeric comparisons, the modality of each constraint, and a pointer back to the source text. From a single IR, deterministic compilers emit both a Prolog program and a Z3 program. The Z3 side is then checked with Clark’s completion, which surfaces a failure that, in our experiments, plain Prolog execution cannot see at all: rules whose violation condition can never be satisfied, so that the checker silently never fires. A repair loop that is CEGIS-informed but ultimately deterministic for structural errors handles the two kinds of failure differently: an LLM revision step targets semantic slips such as lost numeric thresholds and reversed arguments, while a deterministic reconstruction step—reached once the LLM rounds have failed—is the path taken for the structural contradictions, which the LLM step does not fix. In a cross-domain evaluation covering clinical decision rules, AI course knowledge, and legal compliance specifications—three representative domains rather than an exhaustive sample—all compiled programs achieve syntax validity across both backends. Formal verification exposes a class of structural contradictions that, in this pilot-scale benchmark, is concentrated in the legal specifications, where normative hedging constructs appear to induce rule-constraint conflicts. Deterministic repair recovers most structural failures while LLM-only repair consistently reproduces the same broken rule patterns. These findings characterise a previously unrecognised failure mode in LLM-to-logic compilation and demonstrate a practical engineering toolchain for producing verifiable knowledge-base programs from natural-language specifications. We present the domain-level rates as failure-mode discovery on a small corpus rather than as estimates that generalise without further study.