Mayank Keoliya

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.

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.

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.

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.

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.