9 papers
BEAVER: An Efficient Deterministic LLM Verifier
Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee +1
As large language models (LLMs) transition from research prototypes to production systems, practitioners often need reliable methods to verify model outputs and characterize tail r…
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh
Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, causing three key limitations: transformers cann…
SEVerA: Verified Synthesis of Self-Evolving Agents
Debangshu Banerjee, Changming Xu, Eugene Ie +4
Recent advances have shown the effectiveness of self-evolving LLM agents on tasks such as program repair and scientific discovery. In this paradigm, a planner LLM synthesizes an ag…
DafnyPro: LLM-Assisted Automated Verification for Dafny Programs
Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche
We present DafnyPro, an inference-time framework that enhances LLMs for generating verification annotations in Dafny. DafnyPro comprises three key components: a diff-checker that p…
Why DPO is a Misspecified Estimator and How to Fix It
Aditya Gopalan, Sayak Ray Chowdhury, Debangshu Banerjee
Direct alignment algorithms such as Direct Preference Optimization (DPO) fine-tune models based on preference data, using only supervised learning instead of two-stage reinforcemen…
CRANE: Reasoning with constrained LLM generation
Debangshu Banerjee, Tarun Suresh, Shubham Ugare +2
Code generation, symbolic math reasoning, and other tasks require LLMs to produce outputs that are both syntactically and semantically correct. Constrained LLM generation is a prom…