Table of Contents
Fetching ...

Conflict-Free Policy Languages for Probabilistic ML Predicates: A Framework and Case Study with the Semantic Router DSL

Xunzhuo Liu, Hao Wu, Huamin Chen, Bowei He, Xue Liu

Abstract

Conflict detection in policy languages is a solved problem -- as long as every rule condition is a crisp Boolean predicate. BDDs, SMT solvers, and NetKAT all exploit that assumption. But a growing class of routing and access-control systems base their decisions on probabilistic ML signals: embedding similarities, domain classifiers, complexity estimators. Two such signals, declared over categories the author intended to be disjoint, can both clear their thresholds on the same query and silently route it to the wrong model. Nothing in the compiler warns about this. We characterize the problem as a three-level decidability hierarchy -- crisp conflicts are decidable via SAT, embedding conflicts reduce to spherical cap intersection, and classifier conflicts are undecidable without distributional knowledge -- and show that for the embedding case, which dominates in practice, replacing independent thresholding with a temperature-scaled softmax partitions the embedding space into Voronoi regions where co-firing is impossible. No model retraining is needed. We implement the detection and prevention mechanisms in the Semantic Router DSL, a production routing language for LLM inference, and discuss how the same ideas apply to semantic RBAC and API gateway policy.

Conflict-Free Policy Languages for Probabilistic ML Predicates: A Framework and Case Study with the Semantic Router DSL

Abstract

Conflict detection in policy languages is a solved problem -- as long as every rule condition is a crisp Boolean predicate. BDDs, SMT solvers, and NetKAT all exploit that assumption. But a growing class of routing and access-control systems base their decisions on probabilistic ML signals: embedding similarities, domain classifiers, complexity estimators. Two such signals, declared over categories the author intended to be disjoint, can both clear their thresholds on the same query and silently route it to the wrong model. Nothing in the compiler warns about this. We characterize the problem as a three-level decidability hierarchy -- crisp conflicts are decidable via SAT, embedding conflicts reduce to spherical cap intersection, and classifier conflicts are undecidable without distributional knowledge -- and show that for the embedding case, which dominates in practice, replacing independent thresholding with a temperature-scaled softmax partitions the embedding space into Voronoi regions where co-firing is impossible. No model retraining is needed. We implement the detection and prevention mechanisms in the Semantic Router DSL, a production routing language for LLM inference, and discuss how the same ideas apply to semantic RBAC and API gateway policy.
Paper Structure (42 sections, 2 theorems, 3 equations, 6 figures, 1 table)

This paper contains 42 sections, 2 theorems, 3 equations, 6 figures, 1 table.

Key Result

Theorem 1

Let $\phi_i, \phi_j$ be two policy conditions.

Figures (6)

  • Figure 1: The gap addressed by this work. Classical policy languages assume crisp predicates; ML routing systems lack formal policy semantics. ProbPol occupies the intersection.
  • Figure 2: Conflict taxonomy for probabilistic policy languages. Left: classical types, decidable via SAT/set algebra. Right: new types for probabilistic predicates, requiring geometric approximation or distributional knowledge.
  • Figure 3: Decidability hierarchy for probabilistic policy conflict. Voronoi normalization (§\ref{['sec:voronoi']}) converts classifier-level conflicts into the geometrically decidable case.
  • Figure 4: Independent thresholding creates overlapping activation regions (left); $q$ fires both signals. Voronoi normalization (right) partitions embedding space into disjoint regions; $q$ fires exactly one signal (science).
  • Figure 5: FDD-style decision tree encoding. Every path from root to leaf is disjoint. The math $\wedge$ science branch forces explicit handling of the physics-query overlap case.
  • ...and 1 more figures

Theorems & Definitions (5)

  • Theorem 1: Decidability hierarchy
  • proof : Proof sketch
  • Definition 1: Voronoi normalization
  • Theorem 2: Conflict elimination
  • proof