AgentCompiler: It's Not the Model, It's the Prompt

Source abstract

AI agents increasingly execute written instructions (SOPs, rulebooks, approval policies, or simply the prompt) to make consequential decisions at scale: a customer-service bot applies a reimbursement SOP; a clinical assistant executes a triage protocol. When two rules jointly create an impossible obligation, agents following them fail systematically. No alignment technique or behavioral monitor can fix a contradiction that lives in the instructions themselves. We present AGENTCOMPILER, a neuro-symbolic auditor that checks instructions before any agent executes them, a compile-time concer distinct from runtime compliance. An LLM extracts typed rules; deterministic detectors enumerate structural candidates; Lean 4 artifacts gate PROVEN verdicts; failures fall closed to human review. Extraction-dependent findings remain review hypotheses. We release a benchmark of 102 singleand 20 mixed-defect mutations over 48 public procedure documents with a 12-type taxonomy and independent construct audit. On the five formally verifiable defect classes, AGENTCOMPILER achieves F1 = 0.904 (P = 0.945, R= 0.867, FPR = 0.055), outperforming LLM baselines (F1 = 0.75–0.83, FPR up to 0.69), and reaches micro-F1 = 0.833 on mixed-defect documents. Detection is fully deterministic across repeated runs. Formal checking can make an extracted subclaim replayable; it cannot by itself certify the source procedure.