# Neurosymbolic Characterization for Reliable Access Control Policy Analysis

arXiv: https://arxiv.org/abs/2510.20692 · HTML: https://mlsanity.com/paper/2510.20692/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 44 references that are in the map.
- First posted on arXiv 23 Oct 2025.

## Builds on (most cited first, 7 of 7)

- [Large Language Models for Software Engineering: A Systematic Literature Review](https://mlsanity.com/paper/2308.10620/) (2023)
- [Using an LLM to Help With Code Understanding](https://mlsanity.com/paper/2307.08177/) (2023)
- [DePLOI: Applying NL2SQL to Synthesize and Audit Database Access Control](https://mlsanity.com/paper/2402.07332/) (2024)
- [Synthesizing Access Control Policies using Large Language Models](https://mlsanity.com/paper/2503.11573/) (2025)
- [InfeRE: Step-by-Step Regex Generation via Chain of Inference](https://mlsanity.com/paper/2308.04041/) (2023)
- [SoK: Access Control Policy Generation from High-level Natural Language Requirements](https://mlsanity.com/paper/2310.03292/) (2023)
- [OSTRICH2: Solver for Complex String Constraints](https://mlsanity.com/paper/2506.14363/) (2025)

## Abstract (arXiv)

Access control policies are reliability-critical configuration artifacts in cloud systems, yet administrators frequently struggle to verify that a policy permits exactly what they intend. This verification gap cannot be remedied by using LLMs to synthesize policies: we find that reasoning and non-reasoning LLMs fluently explain policy behavior but cannot reason about policy semantics with reliability-grade precision, even when the specification is the LLM's own explanation. We formulate this impasse as the Verifiable Synthesis Paradox: the verification gap persists regardless of how the policy was authored. To remedy this, we introduce PolicySummarizer, a neurosymbolic tool that pairs finite-state automata with an LLM-based simplification to generate precise human-readable characterizations of requests allowed by a policy. PolicySummarizer uses model counting to guarantee the fidelity of the generated characterization by rejecting characterizations that fall below a user-configured threshold in favor of the formally derived one. On 546 AWS, 100 Microsoft Azure, and 100 Google Cloud Platform policies, PolicySummarizer achieves a mean similarity score of 0.93 and a 2.7x improvement over an SMT-based baseline. In a user study, PolicySummarizer raised policy-change-review accuracy from 39% to 93% on the hardest sub-task while reducing self-reported mental demand. We release PolicySummarizer as an open-source tool.