Mayank Keoliya

Hi! I’m Mayank, a third-year PhD student at the University of Pennsylvania. I work with Mayur Naik and Rajeev Alur on trustworthy AI for clinical-decision making. I’m currently looking for opportunities to work on trustworthy AI for healthcare in summer 2026 – hit me up if you’re working on something similar!

present

I’m currently working on projects to build foundation models for early predicton of disease in ICUs, and causal learning for precision oncology. I closely collaborate with cardiologists and oncologists at Penn Medicine to make that happen. More broadly, I’m interested in building models that can be trusted to make decisions in high-stakes settings, and can reason over several data sources (EHR data, video, imaging, and genomics).

papers

KardiaLM: A Foundation Model For ECG Comprehension

Mayank Keoliya*, Seewon Choi*, Alaia Solko-Breslin*, and 4 more authors

Under submission, 2025

Abs

Electrocardiograms (ECG) are central to the detection and diagnosis of cardiac conditions, and analyzing them is a great potential application of the emerging multimodal AI techniques. Current approaches primarily target 12-lead, 10-second recordings and often fail to generalize to longer duration settings and reduced-lead recordings. To address these limitations, we introduce KardiaLM, a lead-agnostic and duration-flexible foundation model for ECG waveform comprehension. KardiaLM combines an ECG encoder with a large language model (LLM), enabling generation, prediction, and reasoning. Through this design, KardiaLM captures both global and fine-grained aspects of ECG data, extending applicability beyond conventional settings. We propose a novel training algorithm for aligning ECG signals with text and demonstrate that KardiaLM achieves strong performance across three tasks: signal completion, classification, and report generation.
Stable Prediction of Adverse Events in Medical Time-Series Data

Mayank Keoliya*, Seewon Choi*, Eric Wong, and 2 more authors

Under submission, 2025

Abs PDF

Early event prediction (EEP) systems continuously estimate a patient’s imminent risk to support clinical decision-making. For bedside trust, risk trajectories must be accurate and temporally stable, shifting only with new, relevant evidence. However, current benchmarks (a) ignore stability of risk scores and (b) evaluate mainly on tabular inputs, leaving trajectory behavior untested. To address this gap, we introduce CAREBench, an EEP benchmark that evaluates deployability using multi-modal inputs-tabular EHR, ECG waveforms, and clinical text-and assesses temporal stability alongside predictive accuracy. We propose a stability metric that quantifies short-term variability in per-patient risk and penalizes abrupt oscillations based on local-Lipschitz constants. CAREBench spans six prediction tasks such as sepsis onset and compares classical learners, deep sequence models, and zero-shot LLMs. Across tasks, existing methods, especially LLMs, struggle to jointly optimize accuracy and stability, with notably poor recall at high-precision operating points. These results highlight the need for models that produce evidence-aligned, stable trajectories to earn clinician trust in continuous monitoring settings.
ESCA: Contextualizing Embodied Agents via Scene-Graph Generation

Jiani Huang, Amish Sethi, Mayank Keoliya, and 5 more authors

Conference on Neural Information Processing Systems, 2025

Spotlight Paper

Abs PDF

Multi-modal large language models (MLLMs) are making rapid progress toward general-purpose embodied agents. However, current training pipelines primarily rely on high-level vision-sound-text pairs and lack fine-grained, structured alignment between pixel-level visual content and textual semantics. To overcome this challenge, we propose ESCA, a new framework for contextualizing embodied agents through structured spatial-temporal understanding. At its core is SGClip, a novel CLIP-based, open-domain, and promptable model for generating scene graphs. ESCA is trained on 87K+ open-domain videos via a neurosymbolic learning pipeline, which harnesses model-driven self-supervision from video-caption pairs and structured reasoning, thereby eliminating the need for human-labeled scene graph annotations. We demonstrate that ESCA supports both prompt-based inference and task-specific fine-tuning, excelling in scene graph generation and action localization benchmarks. ESCA with SGClip consistently improves both open-source and commercial MLLMs, achieving state-of-the-art performance across two embodied environments. Notably, it significantly reduces agent perception errors and enables open-source models to surpass proprietary baselines.
Synthesizing Faithful Explanations for Treatment Effect Estimation

Yinjun Wu*, Mayank Keoliya*, Mayur Naik, and 2 more authors

International Conference on Machine Learning, 2024

Spotlight Paper

Abs PDF

Designing faithful yet accurate AI models is challenging, particularly in the field of individual treatment effect estimation (ITE). ITE prediction models deployed in critical settings such as healthcare should ideally be (i) accurate, and (ii) provide faithful explanations. However, current solutions are inadequate: state-of-the-art black-box models do not supply explanations, post-hoc explainers for black-box models lack faithfulness guarantees, and self-interpretable models greatly compromise accuracy. To address these issues, we propose DISCRET, a self-interpretable ITE framework that synthesizes faithful, rule-based explanations for each sample. A key insight behind DISCRET is that explanations can serve dually as database queries to identify similar subgroups of samples. We provide a novel RL algorithm to efficiently synthesize these explanations from a large search space. We evaluate DISCRET on diverse tasks involving tabular, image, and text data. DISCRET outperforms the best self-interpretable models and has accuracy comparable to the best black-box models while providing faithful explanations.
Mostly Automated Proof Repair for Verified Libraries

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey

Proc. ACM Program. Languages (PLDI), Jun 2023

Distinguished Paper Award

Abs PDF Code Slides Video Website

The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair. One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness. In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing, enabled by the constructive nature of Coq’s proof certificates. We have implemented our approach in a mostly-automated proof repair tool called Sisyphus. Given an OCaml function verified in Coq and its unverified new version, Sisyphus produces a Coq proof for the new version, discharging most of the new proof goals automatically and suggesting high-confidence obligations for the programmer to prove for the cases when automation fails. We have evaluated Sisyphus on 10 OCaml programs taken from popular libraries, that manipulate arrays and mutable data structures, considering their verified original and unverified evolved versions. Sisyphus has managed to repair proofs for all those functions, suggesting correct invariants and generating a small number of easy-to-prove residual obligations.
Simulating Noisy Channels in DNA Storage

Mayank Keoliya, Puru Sharma, and Djordje Jevdjic

IEEE International Symposium on Performance Analysis of Systems and Software, May 2022

Abs PDF Full Report Slides Video

Compared to conventional storage mediums, DNA-based data storage offers benefits such as durability, high density and low energy consumption. With increased demand for DNA data storage, it has become important to quickly evaluate proposed approaches. However, experiments that involve reading and writing synthetic DNA are costly and time-consuming, thus requiring cheap and fast simulation prior to experimentation. DNA sequencing technologies such as Nanopore and Illumina have highly characteristic error profiles, and simulating them is challenging. We propose a DNA simulator for Nanopore data that improves on existing simulators by incorporating key parameters; our simulator better converges to error profiles of real data on most parameters. We show that the spatial distribution of errors within a strand is a key determinant of trace reconstruction accuracy; which is a factor that had not been considered by existing simulators.

past

Before sailing to Philadelphia, I read my bachelor’s at the National University of Singapore, where I studied computer science and a bunch of other things. I’ve worked on research spanning topics like software verification with Prof. Ilya Sergey, and DNA sequencing with Prof. Djordje Jevdjic. I also spent a summer at CVWO to build better systems for non-profits.

Before slinging to Singapore, I grew up in Calcutta, the most charming city in India. I’m a self-styled ambassador for the city, so if you’re heading there for a short trip, do let me know!

fun

I’ve officially taken the plunge into learning Chinese in 2024 (谢谢王老师!). When I’m not diving into Mandarin tones, I’ll be talking about history, stalking old architecture in Philly, playing table tennis, spending hours on Every Noise, reading, and daydreaming about Singaporean food.

projects

Translating C to Safe Rust

Mayank Keoliya, and Theodore Leebrant

Final Year Thesis, National University of Singapore, Apr 2023

Abs PDF Slides

This project addresses the challenge of safe and efficient memory management in systems pro- gramming and presents an approach for automatically translating Rust data structures from RefCell to GhostCell. RefCell provides interior mutability and safe mutation of immutable data structures but incurs performance overhead due to runtime borrow checking. GhostCell avoids this overhead by using compile-time borrow checking but requires significant code changes. We propose a translation framework that preserves the original code’s semantics while taking advantage of GhostCell’s compile-time borrow checking. To evaluate our approach, we conducted a benchmarking study comparing the perfor- mance of the translated code with the original and manually translated code. Our results demonstrate that our approach achieves performance improvements over RefCell. Our con- tribution is a practical solution for Rust programmers who wish to migrate their code from Re- fCell to GhostCell without the need for manual translation, enabling efficient and safe memory management in Rust code while maintaining ease of use and readability. This work opens up new avenues for research in automated migration of Rust code and provides valuable insights for programmers and language designers on the benefits and limitations of Rust’s memory management system.
Implementing MicroKanren in Haskell

Mayank Keoliya, and Theodore Leebrant

CS2104 (Intro. Programming Languages), National University of Singapore, Nov 2020

Abs PDF Slides

This paper discusses the miniKanren family of languages, and in particular, the implementation of a desugared subset, microKanren, in the Haskell programming language. A comprehensive explanation of the implementation is undertaken, and possible explorations for quines, SAT solvers and procedural- logic programming are further elaborated.