arXiv subjects

William Eiers

Publications and source records attributed to William Eiers.

13 recordsLinked to original sources

arXiv2026

Autoformalization for Ambiguous Inputs: Precision, Coverage, and Cost across SQL and Logical Forms

Agentic systems translate natural-language requests into executable artifacts while managing ambiguity and inference cost. We evaluate seven autoformalization workflows on SQL and first-order logic benchmarks for ambiguous inputs. Across five SQL workflows, the raw model leads with F1 of 53.35% on AMBROSIA and 60.85% on AmbiQT. On AmP, DRIFT gains 15.98 F1 points over the raw model at 2.03 times its token cost, whereas LoC uses 18.65 times the raw model's tokens with lower F1. Within AutoCedar, structured interpretation lowers F1 by 6.44-6.95 points and raises AMBROSIA token use 2.2-fold. Paired reviewer comparisons show modest Kimi K3 gains of 1.93 points on AMBROSIA and 2.04 on AmbiQT. Clear-ambiguous AMBROSIA analysis shows greater relative stability for AutoCedar, with a smaller F1 drop than the raw model (11.46 vs. 16.68 points), alongside lower aggregate F1 (50.16% vs. 53.35%). Autoformalization alone does not guarantee robustness to ambiguity: the tested additions offer no uniformly effective remedy, making accuracy, ambiguity handling, and inference cost joint design requirements.

cs.SE↗

arXiv2026

VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims

Large Language Models (LLMs) are being adopted in financial workflows, where accuracy and reliability are critical. One such application is financial question answering over public company filings. However, LLMs struggle with quantitative financial reasoning, including identifying financial facts, interpreting reporting periods and units, and determining appropriate metrics, leading to incorrect answers. Recent RAG-based methods have improved financial question answering but do not ensure factual and numerical correctness. LLM-based verifiers may also accept incorrect numerical claims. To address this, we introduce VeriFin, a neurosymbolic framework for verifying LLM generated numerical financial claims. Given a question and a generated answer, VeriFin retrieves filing evidence, grounds values in XBRL facts, and establishes the required formula independently of the answer. It then uses the Z3 SMT solver to check the resulting arithmetic constraints. VeriFin accepts consistent claims, rejects inconsistent claims, and abstains when required facts or formulas cannot be established. To evaluate VeriFin, we constructed XBRLFiling, a dataset of 600 numerical questions from corporate filings, and selected 67 and 403 questions from FinanceBench and TAT-DQA, respectively. Across six answer models and three datasets, VeriFin achieves 100% observed precision among accepted answers with known correctness. For Qwen3-30B on XBRLFiling, VeriFin accepts 304 correct answers compared to 166 for an LLM judge, while reducing false accepts from 87 to 0. We release our benchmark to support research on reliable financial question answering.

cs.CE↗

arXiv2026

Bellman Language Models: Solving the Recurring Decisions of LLM Agents

A general observation in agentic workflows, especially bounded ones, is that the decision space of the LLM, when we separate a decision from generation, starts approaching saturation: the agent meets the same states again and again, and after enough conversations it stops meeting new ones. LLMs generally don't treat these decisions as an optimization problem and instead re-derive them from their context/prompt on every turn. We show that treating decision making within reasonable bounds as an optimization problem, solving it once, and reusing the solved decisions can often make an agent faster, cheaper and more reliable. Our approach, which we call Discretize, Then Decide, starts from data such as the workflow's own logs or, when none exists, runs of the LLM agent itself. It reads each conversation into discrete states and estimates the probability of each outcome and the cost of each move, until no new states appear and the probabilities stop changing. It then solves the resulting Markov decision process. The solution runs as a controller around the model, sending moves whose content is fixed in the state, such as a tool call or a templated reply, and any state it hasn't seen is sent back to the LLM. We call an LLM run this way a Bellman language model (BLM), after Richard Bellman's equation for the best move in each state. On $τ^2$-bench telecom, the controller with no model solves 79% of tasks. As a BLM, Qwen3.8-27B, an open model, goes from 29% to 96% with 93% fewer model calls. For Claude Opus 5.5, which solves 96% of tasks on its own, running it as a BLM cuts model calls and cost per task by about 98% and lets it solve 2 more tasks. On InventoryBench, the solved policy with no model beats every published method. Where the hard part is writing content rather than choosing moves, such as resolving SymPy issues, few decisions can be solved in advance, and a BLM helps little.

cs.AI↗

arXiv2026

Compression Footprints as Security Signals for Model-Poisoning Defense in Federated Learning

Lossy compression is widely used in Federated Learning (FL) but is generally treated as an error source, while conventional poisoning defenses inspect update geometry. In this work, we instead treat the compressor's response as a security signal: the input-dependent distortion and payload behavior induced by lossy compression can expose differences between honest and attack-generated updates. We introduce the concept of a \emph{compression footprint}: the low-dimensional collection of reconstruction, directional, sparsity, and payload statistics induced by a lossy compressor. We characterize sufficient conditions under which compression footprints separate honest and malicious updates, and operationalize our findings in the CRAFT (\emph{Compression-guided Robust Aggregation via Footprint Trust}) server-side robust aggregation method. Crucially, under a strict honest-majority assumption, CRAFT uses server-verifiable footprints, requires no client-side metadata nor knowledge of the number of malicious clients, and adds no communication beyond the compressed FL pipeline. Moreover, while CRAFT assumes a strict honest majority, it does not require the number of malicious clients to be known in advance. We observe that error-bounded lossy compressor (EBLC) footprints provide stronger separation than Top-K footprints and that footprint trust suppresses malicious influence. We evaluate CRAFT under IID client data with 36\% malicious participation across six standard model-poisoning attacks, three datasets, and six robust aggregation baselines, finding that CRAFT consistently achieves the best accuracy in 7 out of 18 settings and within 1.7 percentage points of the best in the others. Our results show that lossy compression can serve as both a communication mechanism and a security signal for robust aggregation in FL.

cs.LG↗

arXiv2026

RAISE: Reinforcing Access Control Policy Synthesis in LLMs via Symbolic Evaluation

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, to our knowledge the first dataset that supports both training and semantic evaluation for formally verifiable Cedar policy synthesis. It contains 5,800 scenarios across 44 domains and 1,408 representing a single synthetic organization, each with a verified target policy and an executable verification plan. On this data we introduce RAISE, which trains policy synthesizers from formal verification in two stages, verified supervised fine-tuning (SFT) followed by a reinforcement learning (RL) stage that learns from verifier signal. We find that SFT succeeds largely by letting models express authorization logic they already have, since untrained models rarely write valid Cedar but often reason correctly when they do. After SFT, how the verifier's information is used matters more than how much of it is used. Of six RL instantiations that consume progressively richer verifier signal, only RAISE-OC improves meaningfully on SFT; it turns failed checks and symbolic counterexamples into guided exploration and learns from the result with off-context GRPO. With about 5.4K verified scenarios and LoRA fine-tuning, RAISE-OC trains Qwen3.5-9B to surpass zero-shot GPT-6 Astra and Claude Opus 5 by 13.33 and 16.26 percentage points in semantic success on held-out scenarios, and training transfers to the independently constructed CedarBench.

cs.SE↗

arXiv2026

AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis

Large Language Models are increasingly used to turn natural-language requirements into code. In access control, that shortcut is dangerous: 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 that intent. We present AutoCedar, a verifier-guided system that first turns natural-language access-control requirements into a reviewed, checkable target, and then synthesizes Cedar policies against that target. AutoCedar decomposes schema and policy authoring into small intent atoms: reviewable claims about vocabulary and behavior. Once those atoms pass mechanical validation and human intent review, the model proposes a candidate policy, the verifier checks it against the approved target, and each failure is turned into a repair signal that tells the model whether to broaden, narrow, or restructure the policy without changing the target. Because the model's work is split into small problems, each grounded in reviewed intent and backed by verifier feedback, end-to-end policy authoring becomes tractable. AutoCedar converges on all 221 tasks of CedarBench, our benchmark of authorization tasks paired with executable semantic boundaries. Across three requirements-corpus case studies covering healthcare, education, and conference management, AutoCedar converts noisy prose and extracted access-control fragments into reviewed schemas, formal checks, and a globally verified Cedar policy store for each scenario.

cs.SE↗

arXiv2026

Neurosymbolic Characterization for Reliable Access Control Policy Analysis

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.

cs.SE↗

arXiv2026

Neurosymbolic Auditing of Natural-Language Software Requirements

Natural-language software requirements are often ambiguous, inconsistent, and underspecified; in safety-critical domains, these defects propagate into formal models that verify the wrong specification and into implementations that ship unsafe behavior. We show that large language models, equipped with an SMT solver, can audit such requirements: translating them into formal logic, detecting ambiguity through stochastic variation in the generated formalization, and exposing inconsistency, vacuousness, and safety violations through solver queries on the resulting specification. We present VERIMED, a neurosymbolic pipeline that operationalizes this idea for medical-device software requirements, and report two findings. First, stochastic variation across independent formalizations is a signal of ambiguity: requirements that admit multiple plausible interpretations produce SMT-inequivalent formalizations, and bidirectional SMT equivalence checking turns this disagreement into a solver-checkable test. Second, the usefulness of symbolic feedback depends on its granularity: in counterexample-guided repair on a hemodialysis question-answering benchmark, concrete SMT counterexamples raise verified accuracy from 55.4% to 98.5%. Over an extensive experimental evaluation on open-source hemodialysis safety requirements, we show that the LLM-based approach in VERIMED successfully reduces ambiguity-sensitive requirements and enables rigorous auditing of software requirements through SMT-based queries.

cs.SE↗

arXiv2026

CloudFix: Automated Policy Repair for Cloud Access Control Policies Using Large Language Models

Access control policies are vital for securing modern cloud computing, where organizations must manage access to sensitive data across thousands of users in distributed system settings. Cloud administrators typically write and update policies manually, which can be an error-prone and time-consuming process and can potentially lead to security vulnerabilities. Existing approaches based on symbolic analysis have demonstrated success in automated debugging and repairing access control policies; however, their generalizability is limited in the context of cloud-based access control. Conversely, Large Language Models (LLMs) have been utilized for automated program repair; however, their applicability to repairing cloud access control policies remains unexplored. In this work, we introduce CloudFix, the first automated policy repair framework for cloud access control that combines formal methods with LLMs. Given an access control policy and a specification of allowed and denied access requests, CloudFix employs Formal Methods-based Fault Localization to identify faulty statements in the policy and leverages LLMs to generate potential repairs, which are then verified using SMT solvers. To evaluate CloudFix, we curated a dataset of 282 real-world AWS access control policies extracted from forum posts and augmented them with synthetically generated request sets based on real scenarios. Our experimental results show that CloudFix improves repair accuracy over a Baseline implementation across varying request sizes. Our work is the first to leverage LLMs for policy repair, showcasing the effectiveness of LLMs for access control and enabling efficient and automated repair of cloud access control policies. We make our tool Cloudfix and AWS dataset publicly available.

cs.DC↗

arXiv2025

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification

Formally verifying properties of software code has been a highly desirable task, especially with the emergence of LLM-generated code. In the same vein, they provide an interesting avenue for the exploration of formal verification and mechanistic interpretability. Since the introduction of code-specific models, despite their successes in generating code in Lean4 and Isabelle, the task of generalized theorem proving still remains far from being fully solved and will be a benchmark for reasoning capability in LLMs. In this work, we introduce a framework that generates whole proofs in a formal language to be used within systems that utilize the power of built-in tactics and off-the-shelf automated theorem provers. Our framework includes 3 components: generating natural language statements of the code to be verified, an LLM that generates formal proofs for the given statement, and a module employing heuristics for building the final proof. To train the LLM, we employ a 2-stage fine-tuning process, where we first use SFT-based training to enable the model to generate syntactically correct Isabelle code and then RL-based training that encourages the model to generate proofs verified by a theorem prover. We validate our framework using the miniF2F-test benchmark and the Isabelle proof assistant and design a use case to verify the correctness of the AWS S3 bucket access policy code. We also curate a dataset based on the FVEL\textsubscript{\textnormal{ER}} dataset for future training tasks.

cs.AI↗

arXiv2025

Synthesizing Access Control Policies using Large Language Models

Cloud compute systems allow administrators to write access control policies that govern access to private data. While policies are written in convenient languages, such as AWS Identity and Access Management Policy Language, manually written policies often become complex and error prone. In this paper, we investigate whether and how well Large Language Models (LLMs) can be used to synthesize access control policies. Our investigation focuses on the task of taking an access control request specification and zero-shot prompting LLMs to synthesize a well-formed access control policy which correctly adheres to the request specification. We consider two scenarios, one which the request specification is given as a concrete list of requests to be allowed or denied, and another in which a natural language description is used to specify sets of requests to be allowed or denied. We then argue that for zero-shot prompting, more precise and structured prompts using a syntax based approach are necessary and experimentally show preliminary results validating our approach.

cs.SE↗

arXiv2019

Attack Synthesis for Strings using Meta-Heuristics

Information leaks are a significant problem in modern computer systems and string manipulation is prevalent in modern software. We present techniques for automated synthesis of side-channel attacks that recover secret string values based on timing observations on string manipulating code. Our attack synthesis techniques iteratively generate inputs which, when fed to code that accesses the secret, reveal partial information about the secret based on the timing observations, leading to recovery of the secret at the end of the attack sequence. We use symbolic execution to extract path constraints, automata-based model counting to estimate the probability of execution paths, and meta-heuristic methods to maximize information gain based on entropy for synthesizing adaptive attack steps.

cs.SE↗

arXiv2019

Incremental Adaptive Attack Synthesis

Information leakage is a significant problem in modern software systems. Information leaks due to side channels are especially hard to detect and analyze. In this paper, we present techniques for automated synthesis of adaptive side-channel attacks that recover secret values. Our attack synthesis techniques iteratively generate inputs which, when fed to code that accesses the secret, reveal partial information about the secret based on the side-channel observations, reducing the remaining uncertainty about the secret in each attack step. Our approach is incremental, reusing results from prior iterations in each attack step to improve the efficiency of attack synthesis. We use symbolic execution to extract path constraints, automata-based model counting to estimate probabilities of execution paths, and meta-heuristics to maximize information gain based on entropy in order to minimize the number of synthesized attack steps.

cs.SE↗