arXiv subjects

Param Biyani

Publications and source records attributed to Param Biyani.

3 recordsLinked to original sources

arXiv2025

IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

Reliable autoformalization remains challenging even in the era of large language models (LLMs). The scarcity of high-quality training data is a major bottleneck. Expert annotation requires substantial time and deep expertise in both mathematics and theorem proving. We introduce IndiMathBench, a human-verified benchmark designed to evaluate mathematical theorem proving, curated using an AI-powered human-assisted pipeline for formalizing natural language problems in Lean. IndiMathBench is composed of 312 formal Lean 4 theorems paired with their corresponding informal problem statements, sourced from Indian Mathematics Olympiads. Through category-based retrieval, iterative compiler feedback, and multi-model ensembles, our pipeline generates candidate formalizations that experts efficiently validate via an interactive dashboard with automated quality summaries. Evaluation across multiple frontier models demonstrates that autoformalization remains challenging, with substantial gaps between syntactic validity and semantic correctness, while theorem proving success rates remain low even with iterative refinement, demonstrating that \benchmark~presents a challenging testbed for mathematical reasoning. IndiMathBench is available at https://github.com/prmbiy/IndiMathBench.

cs.AI↗

arXiv2025

Improving Language Agents through BREW: Bootstrapping expeRientially-learned Environmental knoWledge

Large Language Model (LLM)-based agents are increasingly capable of complex, multi-step tasks such as GUI automation, tool use, and data manipulation, yet they cannot learn from experience: each new session rediscovers solutions from scratch. We introduce BREW (Bootstrapping expeRientially-learned Environmental knoWledge), a framework that distills an agent's past interaction trajectories into a structured, retrievable knowledge base (KB) of natural-language recipes, concept-level procedural documents that capture what to do, when it applies, and what to watch out for. Drawing on the principle of library learning from program synthesis, BREW decomposes agent memory into modular, concept-localized documents and formalizes KB construction as a state-space search problem. To navigate this space, we introduce Expand-and-Gather Monte Carlo Tree Search (EG-MCTS), a reward-guided algorithm that jointly optimizes recipe accuracy and retrievability across parallel, per-concept search trees. We further adapt hindsight relabeling to convert near-miss trajectories into positive demonstrations, surfacing latent agent competencies as reusable knowledge. On three domain-grounded benchmarks, OSWorld, tau^2-Bench, and SpreadSheetBench, BREW achieves 10-20% gains in task success and 10-15% fewer execution steps over base agents, while consistently outperforming existing memory-augmented baselines that can degrade below memoryless performance. The resulting KB is inspectable, modular, and extensible, providing a transparent and controllable substrate for agent optimization.

cs.AI↗

arXiv2024

Exploring Interaction Patterns for Debugging: Enhancing Conversational Capabilities of AI-assistants

The widespread availability of Large Language Models (LLMs) within Integrated Development Environments (IDEs) has led to their speedy adoption. Conversational interactions with LLMs enable programmers to obtain natural language explanations for various software development tasks. However, LLMs often leap to action without sufficient context, giving rise to implicit assumptions and inaccurate responses. Conversations between developers and LLMs are primarily structured as question-answer pairs, where the developer is responsible for asking the the right questions and sustaining conversations across multiple turns. In this paper, we draw inspiration from interaction patterns and conversation analysis -- to design Robin, an enhanced conversational AI-assistant for debugging. Through a within-subjects user study with 12 industry professionals, we find that equipping the LLM to -- (1) leverage the insert expansion interaction pattern, (2) facilitate turn-taking, and (3) utilize debugging workflows -- leads to lowered conversation barriers, effective fault localization, and 5x improvement in bug resolution rates.

cs.HC↗