7 papers
BRIDGE: Building Representations In Domain Guided Program Synthesis
Robert Joseph George, Carson Eisenach, Udaya Ghai +3
Large language models can generate plausible code, but remain brittle for formal verification in proof assistants such as Lean. A central scalability challenge is that verified syn…
The Bicameral Model: Bidirectional Hidden-State Coupling Between Parallel Language Models
Cedric Flamant, Udaya Ghai, Kanna Shimizu
Existing multi-model and tool-augmented systems communicate by generating text, serializing every exchange through the output vocabulary. Can two pretrained language models instead…
Intent-aligned Formal Specification Synthesis via Traceable Refinement
Zhe Ye, Aidan Z. H. Yang, Huangyuan Su +6
Large language models are increasingly used to generate code from natural language, but ensuring correctness remains challenging. Formal verification offers a principled way to obt…
Learning Adaptive LLM Decoding
Chloe H. Su, Zhe Ye, Samuel Tenka +3
Decoding from large language models (LLMs) typically relies on fixed sampling hyperparameters (e.g., temperature, top-p), despite substantial variation in task difficulty and uncer…
A shared-revenue Bertrand game
Raj Pabari, Udaya Ghai, Dominique Perrault-Joncas +6
We introduce and analyze a variation of the Bertrand game in which the revenue is shared between two players. This game models situations in which one economic agent can provide go…
Outbound Modeling for Inventory Management
Riccardo Savorgnan, Udaya Ghai, Carson Eisenach +1
We study the problem of forecasting the number of units fulfilled (or ``drained'') from each inventory warehouse to meet customer demand, along with the associated outbound shippin…