U-Define

Christine P. Lee, Xinyu Jessica Wang, Aws Albarghouthi, David Porfirio, and Bilge Mutlu. arXiv preprint, 2026. Paper

U-Define lets people state their own constraints in natural language and mark each one as hard or soft. Hard rules are checked with model checking, and soft preferences are rated by an LLM judge. Try it on the family vacation task from the paper.

The LLM's plans and ratings are scripted for this demo, and model checking runs live in your browser.

The task: a family trip to Venice

You are a parent in a family of four: Mom, Dad, Bob (8), and Susan (3). You are planning a trip to Venice, Italy, and want an itinerary that works for everyone. Some needs are firm, like floatation devices for the children during water activities or a reminder for Dad's diabetes medication at meals. Others are preferences, like Mom's love of museums or a relaxed pace for the kids.

Ask the planner for a 2-day itinerary.

Hard rulesMust never be broken. Checked by model checking against every step of the plan.
Soft preferencesFlexible. Rated from one to five stars by an LLM judge.

Drag to pan. Ctrl + scroll to zoom.