Publications

Introduces Generative Verification (GenV) to detect formal translations that produce the expected solver verdict while misrepresenting the intended problem. By learning from a Z3 equivalence oracle, GenV scores formalization faithfulness without a reference at inference time and improves downstream reasoning.

@misc{singh2026beyond,
  title={Beyond Solver Verdicts: Generative Reward Models for Autoformalization},
  author={Vikash Singh and Debargha Ganguly and Aman Goel and Ali Torkamani and Xiaoxue Han and Joseph Lilien and Ferhat Erata and Vipin Chaudhary},
  year={2026},
  eprint={2609.11085},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2609.11085v1},
  note={Under review at ACL Rolling Review - August 2026}
}

A benchmark of 450 graduate-level stochastic-processes problems formalized in Lean 4 and paired with natural-language sources. Covering topics from Markov chains and martingales to Brownian motion and stochastic calculus, StochBench tests formal theorem provers on specialized applied mathematics.

@inproceedings{davidovich2026stochbench,
  title={StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean},
  author={Idan Davidovich and Debargha Ganguly and Vikash Singh and Vipin Chaudhary},
  booktitle={The Sixth Workshop on Mathematical Reasoning and AI (MATH-AI) at NeurIPS 2026},
  note={Accepted},
  year={2026},
  eprint={2609.09264},
  archivePrefix={arXiv},
  primaryClass={cs.CL},
  url={https://arxiv.org/abs/2609.09264v1}
}

An evaluation framework for multilingual watermarking that separates detection calibration, text quality, and disparities across language families. Experiments across six watermarking schemes and eleven languages expose fairness gaps that English-only evaluation misses.

@inproceedings{nemecek2026watermarking,
  title={Auditing Cross-Lingual Fairness in Language Model Watermarking},
  author={Alexander Nemecek and Osama Zafar and Debargha Ganguly and Vikash Singh and Vipin Chaudhary and Erman Ayday},
  booktitle={The Fortieth Annual Conference on Neural Information Processing Systems, Evaluations and Datasets Track},
  note={Accepted as a poster},
  year={2026},
  eprint={2608.20047},
  archivePrefix={arXiv},
  url={https://arxiv.org/abs/2608.20047}
}

Counterfactual Realignment (CoRe) helps frozen vision-language-action policies recover from instruction changes and physical disruptions. It imagines a viable continuation, then realigns the robot and scene before returning control to the policy, without retraining or failure data.

@misc{zhang2026recovery,
  title={Imagining Recovery: Inference-Time Counterfactual Realignment for Vision-Language-Action Models},
  author={Yanyan Zhang and Disheng Liu and Kai Ye and Chaoda Song and Xinpeng Li and Mohsen Hariri and Vikash Singh and Yu Yin and Vipin Chaudhary},
  year={2026},
  eprint={2608.14822},
  archivePrefix={arXiv},
  url={https://arxiv.org/abs/2608.14822}
}

A framework for comparing sequential deliberation, candidate aggregation, and search over partial reasoning states. It aligns evaluation and compute accounting with the inference protocol, distinguishes exact replay from distributional reproducibility, and releases over 1.4 million sampled model attempts.

@misc{hariri2026scaling,
  title={Test-Time Scaling in Reasoning LLMs: Inference Regimes, Evaluation, and Reproducibility},
  author={Mohsen Hariri and Weicong Chen and Nahal Shahini and Vikash Singh and Kai Ye and Amirhossein Samandar and Debargha Ganguly and Sreehari Sankar and Yanyan Zhang and Shouren Wang and Jerry Peng and Biyao Zhang and Michael Hinczewski and Vipin Chaudhary},
  year={2026},
  eprint={2608.04001},
  archivePrefix={arXiv},
  url={https://arxiv.org/abs/2608.04001}
}

@inproceedings{chen2026k4serve,
  title={K4-Serve: Robust Streaming Log Anomaly Detection for HPC \& AI Infrastructure},
  author={Weicong Chen and Vikash Singh and Zahra Rahmani and Debargha Ganguly and Mohsen Hariri and Sean Maxwell and Sanjaya Gajurel and Hadrian Djohari and Vipin Chaudhary},
  year={2026},
  booktitle={Proceedings of the Practice and Experience in Advanced Research Computing 2026},
  url={https://doi.org/10.1145/3785462.3815821}
}

Trains reasoning agents to write SMT-LIB programs, consult Z3, and repair formalizations using executable evidence. Supervised learning from successful solver traces and preference optimization improve the consistency and grounding of model reasoning.

@misc{ganguly2026sequent,
  title={Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning},
  author={D. Ganguly and W. Chen and M. Hariri and Vikash Singh and S. Sankar and S. Wang and Y. Yang and B. Zhang and C. Song and A. Nemecek and K. Ye and O. Zafar and E. Ayday and J. Stubbs and S. Iyengar and V. Chaudhary},
  year={2026},
  url={https://openreview.net/pdf?id=DLMqDyHLTu}
}

Treatment effect estimation from observational data is fundamentally challenged when the underlying causal graph is unknown. We introduce CausalGuard, a framework that aggregates graph-conditional doubly robust estimates and applies a conformal calibration procedure to deliver distribution-free, finite-sample marginal coverage. The method generates candidate DAGs using LLM-derived priors, filters them via conditional-independence tests, and reweights using a Bayesian Information Criterion. Across multiple benchmarks, CausalGuard attains coverage above the nominal 90% level while producing tighter intervals than graph-agnostic alternatives, offering a principled route to reliable causal inference under structural uncertainty.

@misc{singh2026causalguardconformalinferencegraph,
  title={CausalGuard: Conformal Inference under Graph Uncertainty},
  author={Vikash Singh and Weicong Chen and Debargha Ganguly and Yanyan Zhang and Nengbo Wang and Sreehari Sankar and Mohsen Hariri and Alexander Nemecek and Chaoda Song and Shouren Wang and Biyao Zhang and Van Yang and Erman Ayday and Jing Ma and Vipin Chaudhary},
  year={2026},
  eprint={2605.21928},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2605.21928}
}

Retrieval-Augmented Generation (RAG) over sensitive corpora suffers from contextual data leakage that ordinary PII filters miss: combinations of attributes that, taken together, are re-identifying even when no single field is. We propose a Privacy Policy Enforcement (PPE) framework built on dual one-class density estimators trained on synthetic data spanning medicine, finance, and law. Our T3+OCSVM detector achieves strong leakage-detection performance with low latency and substantially fewer false positives than supervised baselines, enabling policy-aware guardrails for production RAG systems.

@inproceedings{zafar2026privacypolicyenforcementguardrails,
  title={Privacy Policy Enforcement Guardrails for Data-Sensitive Retrieval-Augmented Generation},
  author={Osama Zafar and Alexander Nemecek and Yiqian Zhang and Wenbiao Li and Debargha Ganguly and Vikash Singh and Vipin Chaudhary and Erman Ayday},
  booktitle={IEEE TPS 2026},
  year={2026},
  eprint={2605.17034},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2605.17034}
}

Continual test-time adaptation (CTTA) methods commonly rely on a frozen source checkpoint as an anchor. We identify a failure mode we call "blind anchoring": when the source model itself becomes unreliable on a drifting target stream, anchoring to it actively harms adaptation. We propose RMemSafe, which uses normalized predictive entropy as a reliability gate over source-dependent components and gracefully reduces reliance on the source as its reliability degrades. RMemSafe exhibits a 1.13x shallower harm slope than ROID+ASR under source degradation while preserving competitive accuracy on standard CTTA benchmarks.

@misc{singh2026reliabilitygatedsourceanchoringcontinual,
  title={Reliability-Gated Source Anchoring for Continual Test-Time Adaptation},
  author={Vikash Singh and Debargha Ganguly and Weicong Chen and Sabyasachi Sahoo and Sreehari Sankar and Biyao Zhang and Mohsen Hariri and Shouren Wang and Osama Zafar and Christian Gagné and Vipin Chaudhary},
  year={2026},
  eprint={2605.14063},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2605.14063}
}

Vision-Language-Action (VLA) models trained on single-frame observations are fundamentally "dynamics-blind": they cannot perceive temporal dynamics of the scene, leading to catastrophic failures when objects move during execution. We propose a training-free, inference-time correction that decomposes the corrective signal into two orthogonal components: a pace term that modulates execution speed along the planned trajectory and a path term that provides spatial adjustments orthogonal to the path. On our MoveBench diagnostic, the method delivers up to 28.8% improvement in dynamic-only scenarios and 25.9% in mixed settings over strong VLA baselines, with zero additional training.

@misc{zhang2026overcomingdynamicsblindnesstrainingfreepaceandpath,
  title={Overcoming Dynamics-Blindness: Training-Free Pace-and-Path Correction for VLA Models},
  author={Yanyan Zhang and Chaoda Song and Vikash Singh and Xinpeng Li and Kai Ye and Zhe Hu and Zhongzhu Pu and Yu Yin and Vipin Chaudhary},
  year={2026},
  eprint={2605.11459},
  archivePrefix={arXiv},
  primaryClass={cs.RO},
  url={https://arxiv.org/abs/2605.11459}
}

This survey takes a lifecycle perspective on agent skills for Large Language Models, organizing the rapidly fragmenting literature around how skills are constructed, acquired, distilled, evaluated, composed, and ultimately deployed within broader agent ecosystems. We synthesize advances in skill specification (e.g., SKILL.md-style schemas, MCP), acquisition (from demonstration, self-play, and curriculum), evaluation in realistic settings, and the emerging security threat model around shareable skills. The survey aims to give practitioners and researchers a unified map from per-skill design choices to system-level concerns of governance, reuse, and safety.

@article{yang2026agentskills,
  author = {Yang, Wang and Song, Chaoda and Li, Xinpeng and Wang, Shouren and Wang, Nengbo and Zhang, Yanyan and Ma, Chuang and Ganguly, Debargha and Singh, Vikash and Xu, Shuai and Ma, Jing and Yin, Yu and Chaudhary, Vipin and Han, Xiaotian},
  title = {A Survey on Agent Skills for LLMs: A Lifecycle Perspective from Construction to Ecosystems},
  year = {2026},
  month = {May},
  journal = {SSRN},
  url = {https://ssrn.com/abstract=6746498},
  doi = {10.2139/ssrn.6746498}
}

Hybrid-thinking language models use a single set of parameters to serve both an explicit "think" mode and a fast "no-think" mode, which causes reasoning behaviour to leak into responses that are meant to be direct. We propose Path-Lock Expert (PLE), an architectural fix that splits the feed-forward networks into per-mode experts while leaving the rest of the model shared. PLE preserves strong performance on the thinking path and yields a markedly stronger no-think path: more accurate, more concise, and far less prone to spurious reflection. On Qwen3-4B, PLE substantially reduces reflective tokens while improving accuracy across math and science benchmarks.

@misc{wang2026pathlockexpertseparatingreasoning,
  title={Path-Lock Expert: Separating Reasoning Mode in Hybrid Thinking via Architecture-Level Separation},
  author={Shouren Wang and Wang Yang and Chuang Ma and Debargha Ganguly and Vikash Singh and Chaoda Song and Xinpeng Li and Xianxuan Long and Vipin Chaudhary and Xiaotian Han},
  year={2026},
  eprint={2604.27201},
  archivePrefix={arXiv},
  primaryClass={cs.CL},
  url={https://arxiv.org/abs/2604.27201}
}

Vision-language models (VLMs) show promise in drafting radiology reports, yet they frequently suffer from logical inconsistencies, generating diagnostic impressions unsupported by their own perceptual findings or missing logically entailed conclusions. Standard lexical metrics heavily penalize clinical paraphrasing and fail to capture these deductive failures in reference-free settings. Toward guarantees for clinical reasoning, we introduce a neurosymbolic verification framework that deterministically audits the internal consistency of VLM-generated reports. Our pipeline autoformalizes free-text radiographic findings into structured propositional evidence, utilizing an SMT solver (Z3) and a clinical knowledge base to verify whether each diagnostic claim is mathematically entailed, hallucinated, or omitted. Evaluating seven VLMs across five chest X-ray benchmarks, our verifier exposes distinct reasoning failure modes, such as conservative observation and stochastic hallucination, that remain invisible to traditional metrics. On labeled datasets, enforcing solver-backed entailment acts as a rigorous post-hoc guarantee, systematically eliminating unsupported hallucinations to significantly increase diagnostic soundness and precision in generative clinical assistants.

@inproceedings{singh2026clinical,
  title={Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification},
  author={Vikash Singh and Debargha Ganguly and Haotian Yu and Chengwei Zhou and Prerna Singh and Brandon Lee and Vipin Chaudhary and Gourav Datta},
  booktitle={NeurIPS 2026 Workshop on Medical Reasoning with Vision Language Foundation Models (Med-Reasoner)},
  note={Accepted},
  year={2026},
  eprint={2602.24111},
  archivePrefix={arXiv},
  primaryClass={cs.CV},
  url={https://arxiv.org/abs/2602.24111}
}

Retrieval augmented generation (RAG) has enhanced large language models by enabling access to external knowledge, with graph-based RAG emerging as a powerful paradigm for structured retrieval and reasoning. However, existing graph-based methods often over-rely on surface-level node matching and lack explicit causal modeling, leading to unfaithful or spurious answers. Prior attempts to incorporate causality are typically limited to local or single-document contexts and also suffer from information isolation that arises from modular graph structures, which hinders scalability and cross-module causal reasoning. To address these challenges, we propose CausalRAG2, a framework that rethinks knowledge organization for graph-based RAG through causal gating across hierarchical modules. CausalRAG2 explicitly models causal relationships to suppress spurious correlations while enabling scalable reasoning over large-scale knowledge graphs. Extensive experiments demonstrate that CausalRAG2 consistently outperforms competitive graph-based RAG baselines across multiple datasets and evaluation metrics. Our work establishes a principled foundation for structured, scalable, and causally grounded RAG systems.

@misc{wang2026hugrag,
  title={CausalRAG2: Hierarchical Causal Knowledge Graph Design for RAG},
  author={Nengbo Wang and Tuo Liang and Vikash Singh and Chaoda Song and Van Yang and Yu Yin and Jing Ma and Jagdip Singh and Vipin Chaudhary},
  year={2026},
  eprint={2602.05143},
  archivePrefix={arXiv},
  primaryClass={cs.AI},
  url={https://arxiv.org/abs/2602.05143}
}

Current approaches to LLM safety fundamentally rely on a brittle cat-and-mouse game of identifying and blocking known threats via guardrails. We argue for a fresh approach: robust safety comes not from enumerating what is harmful, but from deeply understanding what is safe. We introduce Trust The Typical (T3), a framework that operationalizes this principle by treating safety as an out-of-distribution (OOD) detection problem. T3 learns the distribution of acceptable prompts in a semantic space and flags any significant deviation as a potential threat. Unlike prior methods, it requires no training on harmful examples, yet achieves state-of-the-art performance across 18 benchmarks spanning toxicity, hate speech, jailbreaking, multilingual harms, and over-refusal, reducing false positive rates by up to 40x relative to specialized safety models. A single model trained only on safe English text transfers effectively to diverse domains and over 14 languages without retraining. Finally, we demonstrate production readiness by integrating a GPU-optimized version into vLLM, enabling continuous guardrailing during token generation with less than 6% overhead even under dense evaluation intervals on large-scale workloads.

@misc{ganguly2026t3,
  title={Trust The Typical},
  author={Debargha Ganguly and Sreehari Sankar and Biyao Zhang and Vikash Singh and Kanan Gupta and Harshini Kavuru and A. Luo and Weicong Chen and Warren Morningstar and R. Machiraju and Vipin Chaudhary},
  year={2026},
  eprint={2602.04581},
  archivePrefix={arXiv},
  primaryClass={cs.CL},
  url={https://arxiv.org/abs/2602.04581}
}

Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. Our approach decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking to ensure logic-level alignment between candidates, eliminating the syntactic bias of surface-form metrics, (2) semantic routing that directs different claim types to appropriate verification strategies: symbolic solvers for logical claims and LLM ensembles for commonsense reasoning, and (3) precise logical error localization via Minimal Correction Subsets (MCS), which pinpoint the exact subset of claims to revise, transforming binary failure signals into actionable feedback. Our framework classifies claims by their logical status and aggregates multiple verification signals into a unified score with variance-based penalty. The system iteratively refines answers using structured feedback until acceptance criteria are met or convergence is achieved. This hybrid approach delivers formal guarantees where possible and consensus verification elsewhere, advancing trustworthy AI. With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.

@inproceedings{singh2026verge,
  booktitle={Findings of the Association for Computational Linguistics: EMNLP 2026},
  title={VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning},
  author={Vikash Singh and Darion Cassel and Nathaniel Weir and Nick Feng and Sam Bayless},
  year={2026},
  eprint={2601.20055},
  archivePrefix={arXiv},
  primaryClass={cs.CL},
  url={https://arxiv.org/abs/2601.20055}
}

Hybrid reasoning language models are commonly controlled through high-level Think/No-think instructions to regulate reasoning behavior, yet we found that such mode switching is largely driven by a small set of trigger tokens rather than the instructions themselves. Through attention analysis and controlled prompting experiments, we show that a leading ``Okay''token induces reasoning behavior, while the newline pattern following ``''suppresses it. Based on this observation, we propose Mid-Think, a simple training-free prompting format that combines these triggers to achieve intermediate-budget reasoning, consistently outperforming fixed-token and prompt-based baselines in terms of the accuracy-length trade-off. Furthermore, applying Mid-Think to RL training after SFT reduces training time by approximately 15% while improving final performance of Qwen3-8B on AIME from 69.8% to 72.4% and on GPQA from 58.5% to 61.1%, demonstrating its effectiveness for both inference-time control and RL-based reasoning training.

@inproceedings{wang2026midthink,
  booktitle={Findings of the Association for Computational Linguistics: ACL 2026},
  doi={10.18653/v1/2026.findings-acl.299},
  pages={6024--6038},
  title={Mid-Think: Training-Free Intermediate-Budget Reasoning via Token-Level Triggers},
  author={Van Yang and Shouren Wang and Debargha Ganguly and Xinpeng Li and Chaoda Song and Vikash Singh and Vipin Chaudhary and Xiaotian Han},
  year={2026},
  eprint={2601.07036},
  archivePrefix={arXiv},
  url={https://arxiv.org/abs/2601.07036}
}

Training Large Language Models(LLMs) is one of the most compute-intensive tasks in high-performance computing. Predicting end-to-end training time for multi-billion parameter models distributed across hundreds of GPUs remains challenging due to complex interactions between transformer components, parallelism strategies(data, model, pipeline, tensor), and multi-tier communication. Learned models require costly sampling, while analytical models often struggle with real-world network and hardware complexities. We address this by decomposing LLMs into core computational primitives and modeling them with: (1) operator-level decomposition for fine-grained analysis; (2) lightweight sampling based hardware-aware prediction models for key operations; (3) an end-to-end prediction system integrating these components across complex parallelization strategies. Crucially, our methodology has been validated on two large-scale HPC systems. Our framework achieves low average prediction errors-4.98\% on Perlmutter(A100) and 9.38\% on Vista(GH200)-for models up to 20B parameters across 128 GPUs. Importantly, it runs entirely on CPUs, enabling rapid iteration over hardware configurations and training strategies without costly on-cluster experimentation.

@misc{zhang2025,
  title={Efficient Fine-Grained GPU Performance Modeling for Distributed Deep Learning of LLM},
  author={Biyao Zhang and Mingkai Zheng and Debargha Ganguly and Xuecen Zhang and Vikash Singh and Vipin Chaudhary and Zhao Zhang},
  year={2025},
  eprint={2509.22832},
  archivePrefix={arXiv},
  url={https://arxiv.org/abs/2509.22832}
}

Existing Log Anomaly Detection (LogAD) methods are often slow, dependent on error-prone parsing, and use unrealistic evaluation protocols. We introduce $K^4$, an unsupervised and parser-independent framework for high-performance online detection. $K^4$ transforms arbitrary log embeddings into compact four-dimensional descriptors (Precision, Recall, Density, Coverage) using efficient k-nearest neighbor (k-NN) statistics. These descriptors enable lightweight detectors to accurately score anomalies without retraining. Using a more realistic online evaluation protocol, $K^4$ sets a new state-of-the-art (AUROC: 0.995-0.999), outperforming baselines by large margins while being orders of magnitude faster, with training under 4 seconds and inference as low as 4 $\mu$s.

@misc{chen2025,
  title={K4: Online Log Anomaly Detection Via Unsupervised Typicality Learning},
  author={Weicong Chen and Vikash Singh and Zahra Rahmani and Debargha Ganguly and Mohsen Hariri and Vipin Chaudhary},
  year={2025},
  eprint={2507.20051},
  archivePrefix={arXiv},
  primaryClass={cs.LG},
  url={https://arxiv.org/abs/2507.20051}
}

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic guarantees. This paper addresses this epistemological gap by comprehensively investigating failure modes and uncertainty quantification (UQ) in LLM-generated formal artifacts. Our systematic evaluation of five frontier LLMs reveals Satisfiability Modulo Theories (SMT) based autoformalization's domain-specific impact on accuracy (from +34.8% on logical tasks to -44.5% on factual ones), with known UQ techniques like the entropy of token probabilities failing to identify these errors. We introduce a probabilistic context-free grammar (PCFG) framework to model LLM outputs, yielding a refined uncertainty taxonomy. We find uncertainty signals are task-dependent (e.g., grammar entropy for logic, AUROC>0.93). Finally, a lightweight fusion of these signals enables selective verification, drastically reducing errors (14-100%) with minimal abstention, transforming LLM-driven formalization into a reliable engineering discipline.

@misc{ganguly2025,
  title={Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks},
  author={Debargha Ganguly and Vikash Singh and Sreehari Sankar and Biyao Zhang and Xuecen Zhang and Srinivasan Iyengar and Xiaotian Han and Amit Sharma and S. Kalyanaraman and Vipin Chaudhary},
  year={2025},
  eprint={2505.20047},
  archivePrefix={arXiv},
  primaryClass={cs.CL},
  url={https://arxiv.org/abs/2505.20047}
}