arXiv subjects

Adiel Ashrov

Publications and source records attributed to Adiel Ashrov.

3 recordsLinked to original sources

arXiv2025

Exploring and Evaluating Interplays of BPpy with Deep Reinforcement Learning and Formal Methods

We explore and evaluate the interactions between Behavioral Programming (BP) and a range of Artificial Intelligence (AI) and Formal Methods (FM) techniques. Our goal is to demonstrate that BP can serve as an abstraction that integrates various techniques, enabling a multifaceted analysis and a rich development process. Specifically, the paper examines how the BPpy framework, a Python-based implementation of BP, is enhanced by and enhances various FM and AI tools. We assess how integrating BP with tools such as Satisfiability Modulo Theory (SMT) solvers, symbolic and probabilistic model checking, and Deep Reinforcement Learning (DRL) allow us to scale the abilities of BP to model complex systems. Additionally, we illustrate how developers can leverage multiple tools within a single modeling and development task. The paper provides quantitative and qualitative evidence supporting the feasibility of our vision to create a comprehensive toolbox for harnessing AI and FM methods in a unified development framework.

cs.SE↗

arXiv2025

Statistical Runtime Verification for LLMs via Robustness Estimation

Adversarial robustness verification is essential for ensuring the safe deployment of Large Language Models (LLMs) in runtime-critical applications. However, formal verification techniques remain computationally infeasible for modern LLMs due to their exponential runtime and white-box access requirements. This paper presents a case study adapting and extending the RoMA statistical verification framework to assess its feasibility as an online runtime robustness monitor for LLMs in black-box deployment settings. Our adaptation of RoMA analyzes confidence score distributions under semantic perturbations to provide quantitative robustness assessments with statistically validated bounds. Our empirical validation against formal verification baselines demonstrates that RoMA achieves comparable accuracy (within 1\% deviation), and reduces verification times from hours to minutes. We evaluate this framework across semantic, categorial, and orthographic perturbation domains. Our results demonstrate RoMA's effectiveness for robustness monitoring in operational LLM deployments. These findings point to RoMA as a potentially scalable alternative when formal methods are infeasible, with promising implications for runtime verification in LLM-based systems.

cs.LG↗

arXiv2023

Enhancing Deep Learning with Scenario-Based Override Rules: a Case Study

Deep neural networks (DNNs) have become a crucial instrument in the software development toolkit, due to their ability to efficiently solve complex problems. Nevertheless, DNNs are highly opaque, and can behave in an unexpected manner when they encounter unfamiliar input. One promising approach for addressing this challenge is by extending DNN-based systems with hand-crafted override rules, which override the DNN's output when certain conditions are met. Here, we advocate crafting such override rules using the well-studied scenario-based modeling paradigm, which produces rules that are simple, extensible, and powerful enough to ensure the safety of the DNN, while also rendering the system more translucent. We report on two extensive case studies, which demonstrate the feasibility of the approach; and through them, propose an extension to scenario-based modeling, which facilitates its integration with DNN components. We regard this work as a step towards creating safer and more reliable DNN-based systems and models.

cs.SE↗