Persistence of Reason

Research

Abstract

I study how to make machine reasoning checkable. That means pairing language models with formal tools, so what a model produces can be verified instead of trusted, and then using the verifier's feedback to make the model better.

My current work applies this to access-control policy synthesis. The broader question is how learning and proof can work together.

1Interests

Language models, Formal verification, Reinforcement learning, Deep learning, Mathematics.

2Papers

arXiv preprint, 2026 RAISE: Reinforcing Access Control Policy Synthesis in LLMs via Symbolic Evaluation Reinforcement learning from a formal verifier trains a 9B model to beat zero-shot frontier models at writing correct Cedar policies. arXiv preprint, 2026 AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis Fix the intended meaning first, then let a verifier steer the model to a provably correct policy. Converges on all 221 CedarBench tasks. ISSRE 2026 Neurosymbolic Characterization for Reliable Access Control Policy Analysis Automata and model counting keep LLM policy summaries faithful. Raised change-review accuracy from 39 to 93 percent in a user study. NLBSE @ ICSE 2025 Synthesizing Access Control Policies Using Large Language Models Zero-shot LLMs write valid cloud policies, and only precise, structured specifications make them correct.

3References

google scholar
  1. Yingming Zhou, Adarsh Vatsa, William Eiers. RAISE: Reinforcing Access Control Policy Synthesis in LLMs via Symbolic Evaluation. arXiv preprint, 2026.
    abstract

    Translating natural-language access-control requirements into policies requires careful reasoning about permissions, constraints, and exceptions, and even frontier LLMs often produce policies that violate the intended authorization semantics. We construct CedarInstruct, a dataset of 5,800 scenarios across 44 domains with verified target policies, and introduce RAISE, which trains policy synthesizers from formal verification in two stages. Verified supervised fine-tuning is followed by a reinforcement learning stage that learns from verifier signal. With about 5.4K verified scenarios and LoRA fine-tuning, RAISE-OC trains Qwen3.5-9B to surpass much larger zero-shot frontier models in semantic success on held-out scenarios, and training transfers to the independently constructed CedarBench.

    pdf arxiv
  2. Adarsh Vatsa, Sachi Shome, Yingming Zhou, William Eiers. AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis. arXiv preprint, 2026.
    abstract

    Large language models are increasingly used to turn natural-language requirements into code. In access control, that shortcut is dangerous, because a generated policy can compile and read correctly while granting access that no one approved. The difficulty is not only writing policy code. It is fixing what the requirements mean before code is written, and then checking that the final policy actually satisfies them. AutoCedar is an agentic framework that pins down intent first and lets a verifier guide synthesis from there.

    pdf arxiv
  3. Adarsh Vatsa, Bethel Hall, William Eiers. Neurosymbolic Characterization for Reliable Access Control Policy Analysis. ISSRE 2026, 2026.
    pdf arxiv
  4. Adarsh Vatsa, P. Patel, William Eiers. Synthesizing Access Control Policies Using Large Language Models. NLBSE @ ICSE 2025, 2025.
    pdf arxiv