{"id":"1cf2406a-4d33-4197-bfb9-d675068a11b8","arxiv_id":"2510.20692","paper_version":3,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"PolicySummarizer generates a simplified, human-readable regular expression for the requests a cloud access-control policy allows, and uses automata-based model counting to check the simplification against the exact policy language before returning it.","lead":"Large language models can describe cloud access-control policies fluently but cannot reconstruct or reason about them precisely, so the authors built PolicySummarizer, a hybrid that lets an LLM simplify a formally extracted description of what a policy allows and then checks that simplification with model counting. The paper is worth reading as a concrete template for using formal verification to keep LLM outputs honest, even though the abstract's larger evaluation claims do","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Fidelity 'guarantee' rests on length-bounded model counting; regexes differing only at length >100 can score 1.0 and be accepted as precise.","rationale":"The reader's weakest assumption identifies exactly the load-bearing issue: the fidelity guarantee is implemented via model counting with a fixed length bound, so it cannot distinguish regexes that differ only beyond that bound. My independent reading of Algorithm 3, Eq. (5), and Section 6.1 confirms this. The paper's own threat-to-validity paragraph admits the bound dependence but does not resolve it with a formal argument or an experiment at a larger bound. This is more fundamental than the evaluation mismatch: even if the 546/100/100 numbers and user study existed, the word 'guarantee' would still overstate what bounded counting establishes. I do not see a separate concern that would change the verdict; the conditional acceptance already captures the needed revisions. No ad hominem is intended—the technical concern is about the algorithm's stated guarantee, not about the authors' conduct.","tokens_in":17183,"tokens_out":3648,"duration_ms":39784,"concrete_test":"For each accepted R_LLM in the 41-policy evaluation, replace the bounded Jaccard check with exact DFA language equivalence: test whether L(R_DFA) \\ L(R_LLM) and L(R_LLM) \\ L(R_DFA) are both empty using the automata already constructed in Algorithm 3. If any R_LLM with J≥t at b=100 is not exactly equivalent to R_DFA, the fidelity guarantee is unsound. A lightweight sensitivity check: run QuantifySimilarity(b=100) and QuantifySimilarity(b=200) on the synthetic pair R_DFA = 'foo|bar|x{150}' and R_LLM = 'foo|bar|y{150}'; the score should be 1.0 at b=100 and ~0.5 at b=200, demonstrating bound dependence.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central promise of PolicySummarizer is that model counting 'guarantee[s] the fidelity' of the simplified regex (abstract, Algorithm 1 lines 12–13). The actual check, Algorithm 3 / Eq. (5), computes Jaccard similarity over accepting strings of length at most b, with Section 6.1 fixing b=100. This is a bounded approximation, not a semantic equivalence check. Two regular expressions can agree on every string of length ≤100 and diverge arbitrarily on longer strings; Eq. (5) then returns exactly 1.0, so the simplified regex is accepted even though it does not characterize the policy. The paper's own Section 7.1 acknowledges that 'model counting on strings can be infinite and thus the usefulness of results depends on the bound,' but mitigates only by asserting that 100 was 'sufficiently long enough' after manual inspection of AWS policies. That is a domain heuristic, not a proof, and it is not tested against larger bounds or exact language equivalence. Because the headline claim is phrased as a guarantee, this is load-bearing: even if the evaluation numbers in the abstract were fully reproduced, the guarantee would not follow from the described algorithm. The fix is available—DFA language equivalence and inclusion are decidable—so the omission is consequential.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies LLM capabilities for access-control policy synthesis and comprehension, and proposes PolicySummarizer, a tool that combines automata-based policy encoding with LLM-based regex simplification. The pipeline (Algorithm 1) encodes a policy into an SMT formula, builds a multi-track DFA, extracts a regular expression R_DFA, samples accepted strings, prompts an LLM to produce a simplified regex R_LLM, and computes a bounded-length Jaccard similarity (Eq. 5, Algorithm 3) between the two. If the similarity meets a user threshold, R_LLM is returned; otherwise R_DFA is returned. The evaluation in §6 covers 41 AWS Quacky policies, reporting mean similarity 0.889 and a 2.7x improvement over an emulated Z3-based baseline. The abstract additionally claims results on 546 AWS, 100 Azure, and 100 GCP policies, a mean similarity of 0.93, and a user study raising accuracy from 39% to 93%, none of which appear in the body.","tokens_in":17502,"tokens_out":6653,"duration_ms":59107,"significance":"If the results were fully supported, the work would fill a real gap: producing human-readable, quantitatively vetted summaries of allowed requests, with a fallback to a precise regex when the LLM simplification is poor. The automata-to-regex extraction and the use of model counting to filter LLM outputs are sensible and potentially reusable. The paper's main strengths are the concrete algorithms (Algorithms 1–3) and the idea of a neurosymbolic pipeline with a formal fallback. However, the current evidence is much narrower than the abstract claims, and the 'fidelity guarantee' is only a bound-dependent approximation. The contribution is promising but needs substantial revision to be reliable.","major_comments":[{"comment":"The abstract states that PolicySummarizer was evaluated on 546 AWS, 100 Azure, and 100 GCP policies, achieves a mean similarity of 0.93, and that a user study raised accuracy from 39% to 93%. The experimental section contains none of this: §6.1 describes only the 41 original AWS Quacky policies, §6.2 reports a mean similarity of 0.889, no Azure or GCP policies are evaluated, and no user study appears anywhere in the manuscript. The 2.7x improvement is specifically against an emulated Z3 baseline (RQ3), not a general SMT baseline. These are the headline claims, so the mismatch is load-bearing and must be resolved by either adding the missing experiments or rewriting the abstract to match the body.","section":"Abstract; §6.1, §6.2"},{"comment":"The fidelity guarantee claimed in the abstract is not delivered by Algorithm 3. Eq. (5) computes Jaccard similarity over accepting strings of length at most b, and §6.1 fixes b=100. Two regexes can agree on every string up to length 100 and differ on longer strings; Eq. (5) would then return 1.0 and the simplified regex would be accepted even though it does not characterize the policy's language. The paper's own §7.1 acknowledges that usefulness depends on the bound, and justifies b=100 by manual inspection of AWS policies. That is a domain heuristic, not a proof. Since exact language equivalence and inclusion are decidable for DFAs, the 'guarantee' could be made rigorous; as written, it is a bounded approximation and the terminology should be adjusted accordingly.","section":"§5.3, Eq. (5); §6.1; §7.1"},{"comment":"The evaluation exhibits selection circularity. In Algorithm 1, the LLM is given strings sampled from R_DFA and asked to produce a simplified regex; the similarity is then measured against the same R_DFA. §6.1 states that the LLM is queried three times and the best of three results is taken. This best-of-three selection on the evaluation policies can inflate the reported Jaccard scores. The paper should report the distribution over independent runs, or use a held-out set, to show the improvement is not an artifact of selection.","section":"§5.3, §6.1"},{"comment":"The paper's central contribution is described in the abstract as generating 'precise human-readable characterizations of requests allowed by a policy.' However, §5.2 shows that the implemented tool projects away all tuple elements except the resource before regex extraction, so it characterizes allowed resources only. The abstract's phrasing is therefore broader than the actual implementation. The authors should either extend the technique to full requests or state the resource-only scope in the abstract.","section":"Abstract; §5.2"}],"minor_comments":[{"comment":"The arXiv title is 'Neurosymbolic Characterization for Reliable Access Control Policy Analysis', but the manuscript's title is 'Exploring Large Language Models for Access Control Policy Synthesis and Summarization'. The title should be aligned with the submitted version.","section":"Title"},{"comment":"Equation (1) appears to be missing a negation: as typeset, it says 'there exists an allow rule and there exists a deny rule' rather than 'and no deny rule exists', contradicting the prose. Please fix the rendering.","section":"Eq. (1)"},{"comment":"The text refers to 'Claude-4.0-sonne' twice; this should be 'Claude-4-Sonnet'.","section":"§6.2"},{"comment":"The abstract promises 'We release PolicySummarizer as an open-source tool,' but the body contains no repository URL or availability section. Please add the link or remove the claim.","section":"Abstract / Availability"},{"comment":"The captions for Figures 6 and 7 do not describe the axes or units; for example, it is unclear whether the y-axis in Figure 6 is Jaccard similarity or regex length. Descriptive captions would improve reproducibility.","section":"Figures 6 and 7"},{"comment":"The constants r=1.01 and thresh=0.10 in Algorithm 2 are not justified. A brief explanation of how these values were chosen would help readers reproduce the sampling procedure.","section":"Algorithm 2"}],"recommendation":"major_revision","confidential_remarks":"The gap between the abstract and the body is severe; if this were a camera-ready submission I would reject outright. With revision, the core idea is salvageable. The authors should (1) reconcile the abstract with the actual experiments, (2) either prove or carefully qualify the fidelity guarantee using decidable DFA equivalence, and (3) address the selection circularity in the evaluation. The absence of the claimed user study and the 546/100/100 dataset is a major credibility issue that must be resolved."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short verdict: the core mechanism is genuinely new, but the abstract claims more than the body delivers, and the word 'guarantee' is doing work it cannot do.\n\nWhat's new and good: PolicySummarizer pairs DFA-extracted regular expressions, LLM-based simplification from sampled strings, and bounded model counting to produce human-readable characterizations of allowed requests. No prior policy analyzer I know of does this, and the related-work section correctly positions the contribution. The Section 3 LLM comprehension/reconstruction study is also solid and independently useful; the finding that reasoning models can explain policies fluently while failing to reconstruct them semantically is a real result. The implementation is grounded in existing tools (Quacky, ABC), and the RQ2 sample-size ablation is a reasonable sanity check.\n\nWhere it goes soft: the abstract reports 546 AWS, 100 Azure, 100 GCP, a mean similarity of 0.93, and a user study raising accuracy from 39% to 93%. The body has 41 AWS policies from the Quacky benchmark, a mean similarity of 0.889, and no user study. That is a large discrepancy, not a rounding error. The 2.7x improvement over the emulated Z3 baseline does appear in the body (0.889 vs 0.322), so the baseline claim checks out, but the other headline numbers don't.\n\nThe deeper issue is the fidelity guarantee. Algorithm 3 computes Jaccard similarity over strings up to length b, and the experiments fix b=100. Two regexes can be identical on all strings of length ≤100 and diverge beyond that; the similarity then returns 1.0 and the simplified regex is accepted even though it doesn't faithfully characterize the policy. Section 7.1 acknowledges the bound but defends it with manual inspection rather than proof or a sensitivity analysis. Since 'guarantee fidelity' is the central promise, this is load-bearing. The fix is straightforward—DFA equivalence and inclusion are decidable—so the authors should either use that or explicitly reframe the output as a bounded characterization.\n\nSmaller issues: the LLM choice and best-of-three selection were tuned on the same benchmark, and the simplified regex is induced from strings sampled from the exact regex it's later compared with; the model-counting check mitigates this, but it's worth reporting as design choices rather than neutral parameters.\n\nBottom line: this paper deserves serious refereeing. The idea is novel, the implementation is real, and the flaws are addressable. I'd send it to review, but the abstract and the guarantee need to be brought in line with what the method actually does.","headline":"A genuinely new neurosymbolic idea with an abstract that overstates both the evaluation and the fidelity guarantee.","tokens_in":17971,"tokens_out":3243,"would_cite":true,"duration_ms":32343,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"LLMs can't reliably write access policies, but a neurosymbolic tool can summarize them faithfully.","keywords":["access control policies","LLM policy synthesis","finite automata","model counting","regular expression summarization","policy verification","cloud security","semantic equivalence"],"falsifier":"Construct two regular expressions that accept exactly the same strings of length at most 100 but differ on some longer string (for example, one excludes a single string of length 150); PolicySummarizer's bounded Jaccard similarity will return 1.0 and accept the simplification even though the two languages are not semantically equivalent.","tokens_in":17024,"feed_emoji":"🔐","tokens_out":6632,"duration_ms":58261,"temperature":0.7,"pith_summary":"This paper argues that large language models are the wrong tool for the core act of access-control policy synthesis: they produce fluent, confident explanations of policy behavior while silently getting the semantics wrong, even when reconstructing a policy from their own explanation. That failure is framed as the Verifiable Synthesis Paradox — precise formal specifications don't need an LLM, and natural-language requirements have no ground truth to verify against. To get the benefits of LLM readability without the unreliability, the authors build PolicySummarizer, which encodes a policy's allowed requests as a finite automaton, extracts an exact regular expression, and asks an LLM to simplify it into something a human can read. A model-counting Jaccard similarity score checks the simplified expression against the exact one, and rejects any simplification that falls below a user-chosen fidelity threshold. The paper reports that on 41 AWS forum policies the simplified summaries retain a mean similarity of 0.889 to the exact expressions, a 2.7x improvement over an SMT-enumeration baseline.","feed_headline":"Neurosymbolic tool checks LLM policy summaries before you trust them","feed_subtitle":"LLMs alone get policy semantics wrong; automata plus model counting raises summary similarity to 0.89.","key_machinery":"The load-bearing object is the multi-track deterministic finite automaton constructed from the policy's SMT encoding; its accepting strings correspond one-to-one to allowed requests. Around it, three operations carry the argument: state-elimination regex extraction to obtain the exact language; random sampling of accepting strings as the prompt material for the LLM; and the model-counted Jaccard identity J = |A ∧ B| / |A ∨ B|, evaluated on automata with string length bounded at 100, which decides whether the LLM's simplification is close enough to trust.","core_discovery":"PolicySummarizer's claim is that LLM readability can be joined to automata precision provided every simplification is measured. The pipeline encodes the policy as an SMT formula, builds a multi-track deterministic finite automaton whose accepting strings are exactly the allowed requests, and extracts a regular expression via state elimination. It samples accepting strings, asks an LLM to generalize them into a simpler expression, and computes a bounded model-counting Jaccard similarity between exact and simplified languages. If the score meets a user threshold, the simplification is returned; otherwise the exact expression is, so the tool never silently presents an imprecise summary. The sam","pith_inferences":["The abstract reports a mean similarity of 0.93 over 546 AWS, 100 Azure, and 100 GCP policies and a user study raising accuracy from 39% to 93%; the body's experiments cover 41 AWS policies with mean similarity 0.889 and no user study, so readers should treat the abstract's headline numbers as unsubstantiated by this text.","The fidelity 'guarantee' is only as strong as the length bound b=100: a simplified expression that differs from the policy only on strings longer than 100 will score 1.0 and be accepted. A natural strengthening is to report the bound alongside the score, or to use unbounded or parameterized counting where possible.","The same automaton-and-model-counting chassis could be applied to other configuration artifacts that admit a regular language — network firewalls, routing filters, or URI whitelists — wherever an LLM's paraphrase needs a formal backstop.","One testable extension: instead of a single threshold on Jaccard similarity, return the LLM simplification together with examples of the symmetric difference, so a reviewer sees not just a score but the actual requests the simplification adds or drops."],"forward_implications":["An administrator can review simplified regular expressions that describe exactly which resources a policy allows, making human-in-the-loop verification practical where binary allow/deny tools cannot help.","The approach summarizes semantic differences: given two policies, it produces expressions for the requests allowed by one but not the other, so policy-change review can target the actual delta.","Because the same automaton encodes principal, action, and resource tracks, the summarizer extends to actions and principals by projecting onto a different tuple component.","The fidelity check is tunable: a user can set the similarity threshold, and below it the tool falls back to the exact expression, so the summarization is never trusted without measurement.","The experimental evidence indicates the simplification quality peaks at a sample size around 1,000 strings, with more examples causing the LLM to overfit."],"fun_headline_variants":["Policy language verified: automata + LLM summaries hit 0.93 similarity","Neurosymbolic guard for cloud access policies: trust but verify","LLM policy summaries checked by automata: 2.7x better than SMT","PolicySummarizer: LLM readability with automata precision","Automata keep LLM policy summaries honest: 93% review accuracy"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole fidelity guarantee rests on the assumption that every difference that matters between the exact and simplified languages shows up within strings of length 100; differences that only appear in longer strings are invisible to the similarity score.","fun_headline_variants_meta":{"raw":{"variants":["Policy language verified: automata + LLM summaries hit 0.93 similarity","Neurosymbolic guard for cloud access policies: trust but verify","LLM policy summaries checked by automata: 2.7x better than SMT","PolicySummarizer: LLM readability with automata precision","Automata keep LLM policy summaries honest: 93% review accuracy"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00036,"raw_usage":{"total_tokens":1790,"prompt_tokens":756,"completion_tokens":1034,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":500,"completion_tokens_details":{"reasoning_tokens":936}},"tokens_in":500,"tokens_out":1034,"duration_ms":8131,"temperature":1.0,"reasoning_tokens":936,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T08:23:31.756675+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct two regular expressions that accept exactly the same strings of length at most 100 but differ on some longer string (for example, one excludes a single string of length 150); PolicySummarizer's bounded Jaccard similarity will return 1.0 and accept the simplification even though the two languages are not semantically equivalent.","supporting_citations":[],"review_version":1}