Author name cluster

Abhinav Verma

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

1 author row

AAAI Conference 2026 Conference Paper

Explanations for Sequential Decision-Making – an Overview

Hendrik Baier
Mark T. Keane
Sarath Sreedharan
Silvia Tulli
Abhinav Verma

In this paper, we highlight the field of explainable sequential decision making. We discuss how the problem of explaining sequential decisions gives rise to problems and challenges that are absent from scenarios that focus on explaining single-shot decision making. We provide a short survey of some of the more prominent subareas within explainable sequential decision-making and their unique focuses and blind spots. Here, we argue that we need to go beyond simply focusing on individual subareas like explainable planning, reinforcement learning, or robotics, and move towards studying and tackling the more general problem of explainable sequential decision-making. Such a holistic approach will not only allow us to identify previously ignored problems, but also provide us with the ability to transfer ideas and intuitions from one subarea of explainable sequential decision-making to another. We end the paper with a discussion on future directions and some of the most pressing open questions.

PDF Details DOI

AAAI Conference 2026 Short Paper

Robust Adaptive Multi-Step Predictive Shielding (Student Abstract)

Tanmay Ambadkar
Darshan Chudiwal
Greg Anderson
Abhinav Verma

Ensuring safety in deep reinforcement learning is challenging, as formal methods that provide strong guarantees often fail to scale to complex, high-dimensional systems. We introduce RAMPS, a scalable shielding framework that pairs a general-purpose, learned linear dynamics model with a robust, multi-step Control Barrier Function (CBF) for real-time safety interventions. Experiments show RAMPS significantly reduces safety violations in high-dimensional environments compared to state-of-the-art methods, without sacrificing task performance.

PDF Details DOI

TMLR Journal 2025 Journal Article

LTL-Constrained Policy Optimization with Cycle Experience Replay

Ameesh Shah
Cameron Voloshin
Chenxi Yang
Abhinav Verma
Swarat Chaudhuri
Sanjit A. Seshia

Linear Temporal Logic (LTL) offers a precise means for constraining the behavior of reinforcement learning agents. However, in many settings where both satisfaction and optimality conditions are present, LTL is insufficient to capture both. Instead, LTL-constrained policy optimization, where the goal is to optimize a scalar reward under LTL constraints, is needed. This constrained optimization problem proves difficult in deep Reinforcement Learning (DRL) settings, where learned policies often ignore the LTL constraint due to the sparse nature of LTL satisfaction. To alleviate the sparsity issue, we introduce Cycle Experience Replay (CyclER), a novel reward shaping technique that exploits the underlying structure of the LTL constraint to guide a policy towards satisfaction by encouraging partial behaviors compliant with the constraint. We provide a theoretical guarantee that optimizing CyclER will achieve policies that satisfy the LTL constraint with near-optimal probability. We evaluate CyclER in three continuous control domains. Our experimental results show that optimizing CyclER in tandem with the existing scalar reward outperforms existing reward-shaping methods at finding performant LTL-satisfying policies.

PDF Details

IJCAI Conference 2025 Conference Paper

RetroMoE: A Mixture-of-Experts Latent Translation Framework for Single-step Retrosynthesis

Xinjie Li
Abhinav Verma

Single-step retrosynthesis is a crucial task in organic synthesis, where the objective is to identify the reactants needed to produce a given product. In recent years, a variety of machine learning methods have been developed to tackle retrosynthesis prediction. In our study, we introduce RetroMoE, a novel generative model designed for the single-step retrosynthesis task. We start with a non-symmetric variational autoencoder (VAE) that incorporates a graph encoder to map molecular graphs into a latent space, followed by a transformer decoder for precise prediction of molecular SMILES strings. Additionally, we implement a simple yet effective mixture-of-experts (MoE) network to translate the product latent embedding into the reactant latent embedding. To our knowledge, this is the first approach that frames single-step retrosynthesis as a latent translation problem. Extensive experiments on the USPTO-50K and USPTO-MIT datasets demonstrate the superiority of our method, which not only surpasses most semi-template-based and template-free methods but also delivers competitive results against template-based methods. Notably, under the class-known setting on the USPTO-50K, our method achieves top-1 exact match accuracy comparable to the state-of-the-art template method, RetroKNN.

PDF Details DOI

NeurIPS Conference 2023 Conference Paper

Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees

Đorđe Žikelić
Mathias Lechner
Abhinav Verma
Krishnendu Chatterjee
Thomas Henzinger

Reinforcement learning has shown promising results in learning neural network policies for complicated control tasks. However, the lack of formal guarantees about the behavior of such policies remains an impediment to their deployment. We propose a novel method for learning a composition of neural network policies in stochastic environments, along with a formal certificate which guarantees that a specification over the policy's behavior is satisfied with the desired probability. Unlike prior work on verifiable RL, our approach leverages the compositional nature of logical specifications provided in SpectRL, to learn over graphs of probabilistic reach-avoid specifications. The formal guarantees are provided by learning neural network policies together with reach-avoid supermartingales (RASM) for the graph’s sub-tasks and then composing them into a global policy. We also derive a tighter lower bound compared to previous work on the probability of reach-avoidance implied by a RASM, which is required to find a compositional policy with an acceptable probabilistic threshold for complex tasks with multiple edge policies. We implement a prototype of our approach and evaluate it on a Stochastic Nine Rooms environment.

PDF Details

NeurIPS Conference 2020 Conference Paper

Learning Differentiable Programs with Admissible Neural Heuristics

Ameesh Shah
Eric Zhan
Jennifer Sun
Abhinav Verma
Yisong Yue
Swarat Chaudhuri

We study the problem of learning differentiable functions expressed as programs in a domain-specific language. Such programmatic models can offer benefits such as composability and interpretability; however, learning them requires optimizing over a combinatorial space of program "architectures". We frame this optimization problem as a search in a weighted graph whose paths encode top-down derivations of program syntax. Our key innovation is to view various classes of neural networks as continuous relaxations over the space of programs, which can then be used to complete any partial program. All the parameters of this relaxed program can be trained end-to-end, and the resulting training loss is an approximately admissible heuristic that can guide the combinatorial search. We instantiate our approach on top of the A* and Iterative Deepening Depth-First Search algorithms and use these algorithms to learn programmatic classifiers in three sequence classification tasks. Our experiments show that the algorithms outperform state-of-the-art methods for program learning, and that they discover programmatic classifiers that yield natural interpretations and achieve competitive accuracy.

PDF Details

NeurIPS Conference 2020 Conference Paper

Neurosymbolic Reinforcement Learning with Formally Verified Exploration

Greg Anderson
Abhinav Verma
Isil Dillig
Swarat Chaudhuri

We present REVEL, a partially neural reinforcement learning (RL) framework for provably safe exploration in continuous state and action spaces. A key challenge for provably safe deep RL is that repeatedly verifying neural networks within a learning loop is computationally infeasible. We address this challenge using two policy classes: a general, neurosymbolic class with approximate gradients and a more restricted class of symbolic policies that allows efficient verification. Our learning algorithm is a mirror descent over policies: in each iteration, it safely lifts a symbolic policy into the neurosymbolic space, performs safe gradient updates to the resulting policy, and projects the updated policy into the safe symbolic subset, all without requiring explicit verification of neural networks. Our empirical results show that REVEL enforces safe exploration in many scenarios in which Constrained Policy Optimization does not, and that it can discover policies that outperform those learned through prior approaches to verified exploration.

PDF Details

NeurIPS Conference 2019 Conference Paper

Imitation-Projected Programmatic Reinforcement Learning

Abhinav Verma
Hoang Le
Yisong Yue
Swarat Chaudhuri

We study the problem of programmatic reinforcement learning, in which policies are represented as short programs in a symbolic language. Programmatic policies can be more interpretable, generalizable, and amenable to formal verification than neural policies; however, designing rigorous learning approaches for such policies remains a challenge. Our approach to this challenge - a meta-algorithm called PROPEL - is based on three insights. First, we view our learning task as optimization in policy space, modulo the constraint that the desired policy has a programmatic representation, and solve this optimization problem using a form of mirror descent that takes a gradient step into the unconstrained policy space and then projects back onto the constrained space. Second, we view the unconstrained policy space as mixing neural and programmatic representations, which enables employing state-of-the-art deep policy gradient approaches. Third, we cast the projection step as program synthesis via imitation learning, and exploit contemporary combinatorial methods for this task. We present theoretical convergence results for PROPEL and empirically evaluate the approach in three continuous control domains. The experiments show that PROPEL can significantly outperform state-of-the-art approaches for learning programmatic policies.

PDF Details

AAAI Conference 2019 Short Paper

Verifiable and Interpretable Reinforcement Learning through Program Synthesis

Abhinav Verma

We study the problem of generating interpretable and verifiable policies for Reinforcement Learning (RL). Unlike the popular Deep Reinforcement Learning (DRL) paradigm, in which the policy is represented by a neural network, the aim of this work is to find policies that can be represented in highlevel programming languages. Such programmatic policies have several benefits, including being more easily interpreted than neural networks, and being amenable to verification by scalable symbolic methods. The generation methods for programmatic policies also provide a mechanism for systematically using domain knowledge for guiding the policy search. The interpretability and verifiability of these policies provides the opportunity to deploy RL based solutions in safety critical environments. This thesis draws on, and extends, work from both the machine learning and formal methods communities.

PDF Details