arXiv subjects

Manish Acharya

Publications and source records attributed to Manish Acharya.

5 recordsLinked to original sources

arXiv2026

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

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 benchmark 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. Artifacts are available on GitHub.

cs.LG↗

arXiv2026

STA-FEM: Exact Streaming Assembly for Preplanned Dynamic Tetrahedral Topology Edits

Dynamic tetrahedral simulation pipelines rebuild topology-dependent solver state after every fracture, refinement, or merge event - discarding structural continuity that survives each edit and spending global work on what are often local changes. We present STA-FEM, a streaming assembly method for simulations with topologically-dynamic tetrahedral meshes operating on a fixed superset mesh: when the candidate element pool is preallocated and the per-frame edit stream is exposed, the surrounding solver, preconditioner, and time-stepping layers stay unchanged while the per-frame assembly step is replaced with persistent incremental updates that match a full-rebuild approach exactly at every frame. Across various three-dimensional examples with up to 460k elements, the method delivers end-to-end speedups of 1.37x to 1.61x over full-rebuild with orders-of-magnitude reductions in matrix update cost, preserving exact matrix parity in all tested frames against a stronger exact local recomputation baseline. We test our algorithm in realistic fracture simulation pipelines and observe up to 76% speedups in fracture frame time with exact equivalence to a ground-truth full-rebuild algorithm. These results establish exact streaming assembly as a potentially practical approach for simulating tetrahedral meshes with dynamic topology.

cs.GR↗

arXiv2025

Efficient Sliced Wasserstein Distance Computation via Adaptive Bayesian Optimization

The sliced Wasserstein distance (SW) reduces optimal transport on $\mathbb{R}^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.

cs.LG↗

arXiv2025

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

Optimizing software performance through automated 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 enabling 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 optimized 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.

cs.SE↗

arXiv2024

An Application of Large Language Models to Coding Negotiation Transcripts

In recent years, Large Language Models (LLM) have demonstrated impressive capabilities in the field of natural language processing (NLP). This paper explores the application of LLMs in negotiation transcript analysis by the Vanderbilt AI Negotiation Lab. Starting in September 2022, we applied multiple strategies using LLMs from zero shot learning to fine tuning models to in-context learning). The final strategy we developed is explained, along with how to access and use the model. This study provides a sense of both the opportunities and roadblocks for the implementation of LLMs in real life applications and offers a model for how LLMs can be applied to coding in other fields.

cs.CL↗