publications

2026

1. 

   VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

   Manish Acharya , Zhenyu Liao, Yueke Zhang, and 3 more authors

   Accepted at the AI4MATH Workshop, 43rd International Conference on Machine Learning (ICML 2026),

   Abs HTML PDF

   LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot framework that routes every verifier signal back into proof search through a two-phase protocol: Best-of-N sampling first, then a critic-guided MCTS pass that ingests Phase 1 failures as explicit negative examples. The protocol preserves every theorem solved by its own Phase 1 sweep, so Phase 2’s additional solves are attributable to feedback- driven exploration. VERITAS reaches 40.6% on miniF2F (vs. an independently run Best-of-5 at 36.9%, Portfolio 26.2%) and 7.3% on VERITAS- CombiBench, a 55-theorem combinatorics bench- mark we release on which Best-of-5 (1.8%) falls below Portfolio (3.6%), exposing that unguided sampling hurts when correct lemma names must be recovered iteratively from verifier feedback.

2025

1. 

   Efficient Sliced Wasserstein Distance Computation via Adaptive Bayesian Optimization

   Manish Acharya , and David Hyde

   Accepted at the 14th International Conference on Learning Representations (ICLR 2026),

   Abs HTML PDF Poster

   The sliced Wasserstein distance (SW) reduces optimal transport on ℝ^d to a sum of one-dimensional projections, and thanks to this efficiency, it is widely used in geometry, generative modeling, and registration tasks. Recent work shows that quasi-Monte Carlo constructions for computing SW (QSW) yield direction sets with excellent approximation error. This paper presents an alternate, novel approach: learning directions with Bayesian optimization (BO), particularly in settings where SW appears inside an optimization loop (e.g., gradient flows). We introduce a family of drop-in selectors for projection directions: BOSW, a one-shot BO scheme on the unit sphere; RBOSW, a periodic-refresh variant; ABOSW, an adaptive hybrid that seeds from competitive QSW sets and performs a few lightweight BO refinements; and ARBOSW, a restarted hybrid that periodically relearns directions during optimization. Our BO approaches can be composed with QSW and its variants (demonstrated by ABOSW/ARBOSW) and require no changes to downstream losses or gradients. We provide numerical experiments where our methods achieve state-of-the-art performance, and on the experimental suite of the original QSW paper, we find that ABOSW and ARBOSW can achieve convergence comparable to the best QSW variants with modest runtime overhead.

2024

1. 

   Optimizing Code Runtime Performance through Context-Aware Retrieval-Augmented Generation

   Manish Acharya^* , Yifan Zhang^*, Yu Huang, and 1 more author

   Accepted at the 33rd IEEE/ACM International Conference on Program Comprehension (ICPC 2025 ERA),

   Abs HTML PDF Code

   Optimizing software performance through auto- mated code refinement offers a promising avenue for enhancing execution speed and efficiency. Despite recent advancements in LLMs, a significant gap remains in their ability to perform in- depth program analysis. This study introduces AUTOPATCH, an in-context learning approach designed to bridge this gap by en- abling LLMs to automatically generate optimized code. Inspired by how programmers learn and apply knowledge to optimize software, AUTOPATCH incorporates three key components: (1) an analogy-driven framework to align LLM optimization with human cognitive processes, (2) a unified approach that integrates historical code examples and CFG analysis for context-aware learning, and (3) an automated pipeline for generating opti- mized code through in-context prompting. Experimental results demonstrate that AUTOPATCH achieves a 7.3% improvement in execution efficiency over GPT-4o across common generated executable code, highlighting its potential to advance automated program runtime optimization.

2. 

   An Application of Large Language Models to Coding Negotiation Transcripts

   Ray Friedman, Jaewoo Cho,  Manish Acharya , and 55 more authors

   HTML PDF Website