October 1, 2026 · NeurIPS 2026 Workshop
Stratified Consistency Distillation for Natural Language Formalization
Training a smaller open model to turn natural language into logic, using a frontier model's disagreement to decide what to teach it.
As AI agents take on more autonomy, controlling what they're allowed to do comes down to policy: authorization rules, compliance requirements, filesystem and network permissions. Policy formalization turns that natural language intent into a precise representation that a system can check.
There are several ways to express these rules. Cedar is the authorization policy language behind Amazon Verified Permissions. Dogwood combines Cedar policies with temporal conditions over an agent's actions. OpenShell uses YAML policies to describe filesystem and network access, while Common Expression Language (CEL) lets applications express and evaluate conditions. For reasoning directly with solvers and proof assistants, we can use SMT-LIB, the standard input language used by solvers such as Z3 and cvc5, or Lean.
NVIDIA's OpenShell write-up on formal methods and Z3 gives a concrete example: its policy prover checks whether a proposed policy stays within an approved access boundary. If it doesn't, the solver can produce a counterexample showing access that the proposed policy allows but the boundary forbids.
Once a policy is formal, we can check an agent's actions or an LLM's answers against the encoded rules. The bottleneck is getting the translation right. Frontier models can do this well with careful prompting, but repeated inference is expensive, and closed model weights limit how we can adapt them to a particular application.
Our approach, Stratified Consistency Distillation, tackles this for SMT-LIB. We sample multiple translations from a frontier model, use Z3 to cluster them by logical equivalence, and compute semantic entropy over the clusters. This measures disagreement about meaning: two translations that look different can still express the same rule.
We then choose the training target, or pseudo-label, according to how much the model disagrees with itself:
- Low entropy: choose a translation from the largest cluster—the majority vote.
- Medium entropy: ask an LLM judge to choose between the two leading clusters.
- High entropy: try to unify the leading translations, or leave the example out.
During his internship with the AWS Automated Reasoning group, Zhichao Hou turned this into a distillation pipeline for fine-tuning a small open model.
On FOLIO, SCD takes Qwen2.5-7B-Instruct from 21.9% to 55.2% Pass@10; ordinary distillation reaches 50.3%. Pass@10 measures whether at least one of ten generated translations is logically equivalent to the reference formula. These are the results in Table 1 of the paper. The paper also reports 5–20× lower inference cost than the frontier teacher.
The same idea could extend to other target languages, provided we have a suitable way to check semantic equivalence. The experiments here use SMT-LIB and Z3; applying the recipe to other policy languages would require implementing and evaluating those checks.
An early version of this work will appear at the AI for Verifiable Coding workshop at NeurIPS 2026. Great working with Zhichao Hou, Joe Lilien, and MohamadAli Torkamani on this.