7 papers
Classifying Capabilities (Extended Version)
Cao Nguyen Pham, Oliver BraÄevac, Yichen Xu +2
Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kin…
System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)
Yichen Xu, Oliver BraÄevac, Cao Nguyen Pham +2
Substructural type systems give strong static control over aliasing. Examples include uniqueness, separation, and borrowing. How can such control be brought to established language…
Libretto: Giving LLM Agents a Sense of Musical Structure
Yichen Xu
Generative music systems can now produce impressive audio from text prompts, but audio outputs are difficult to inspect, edit, and diagnose as musical structure. We introduce Libre…
LACUNA: Safe Agents as Recursive Program Holes
Yaoyu Zhao, Yichen Xu, Oliver BraÄevac +3
LLM agents increasingly act by writing code, yet a split persists between the runtime that drives the agent and the code the model writes. The runtime owns the loop, context, and c…
Tracking Capabilities for Safer Agents
Martin Odersky, Yaoyu Zhao, Yichen Xu +2
AI agents that interact with the real world through tool calls pose fundamental safety challenges: agents might leak private information, cause unintended side effects, or be manip…
Agentic Proof Automation: A Case Study
Yichen Xu, Martin Odersky
Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language model…