BEGIN:VCALENDAR
PRODID:-//planitpurple.northwestern.edu//iCalendar Event//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
CLASS:PUBLIC
BEGIN:VTIMEZONE
TZID:America/Chicago
TZURL:http://tzurl.org/zoneinfo-outlook/America/Chicago
X-LIC-LOCATION:America/Chicago
BEGIN:DAYLIGHT
TZOFFSETFROM:-0600
TZOFFSETTO:-0500
TZNAME:CDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0500
TZOFFSETTO:-0600
TZNAME:CST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SEQUENCE:0
DTSTART;TZID=America/Chicago:20261005T120000
DTEND;TZID=America/Chicago:20261005T130000
DTSTAMP:20260706T122742Z
SUMMARY:CS Seminar: Formal Relational Equivalence for SQL\, GenAI\, and Beyond (Brian Suchy)
UID:642868@northwestern.edu
TZID:America/Chicago
DESCRIPTION:Monday / CS Seminar October 5 / 12:00 PM Hybrid / Mudd 3514  Speaker Brian Suchy\, Software Engineer Google DeepMind  Talk Title Formal Relational Equivalence for SQL\, GenAI\, and Beyond  Abstract Verifying that complex query rewrites from database optimizers or AI-driven generators preserve exact bag semantics under three-valued logic is an NP-hard challenge. To address this\, we present an MLIR-native compiler framework that formally reasons about relational algebra. By decoupling query semantics from specific execution engines and lowering queries into a unified Relational Algebra Intermediate Representation\, our language-agnostic methodology definitively proves semantic equivalence across all possible database states.  The core of the presentation will deep-dive into our multi-tiered proving architecture\, which synthesizes several advanced academic methodologies. First\, we utilize E-Graphs and Equality Saturation to rapidly explore the equivalence space and detect structural congruence between query abstract syntax trees using fast\, algebraic rewrite rules. Second\, we employ Semiring Arithmetic\, treating relational algebra as expressions over K-relations to leverage algebraic simplification and canonical forms under semiring laws. Finally\, we implement a First-Order Logic and SMT translation path\, lowering Relational Algebra into Relational Calculus and then into First-Order Logic to evaluate constraints and domain-specific axioms using parallel solvers like Z3 and CVC5\, which either formally proves equivalence or synthesizes concrete counter-examples.  Finally\, we will discuss the practical implications of combining these formal mathematical methods with modern compiler design. Attendees will leave with a comprehensive understanding of how bridging database theory\, equality saturation\, and SMT solving can create robust solutions for verifying query optimizers\, enforcing semantic correctness\, and validating automated SQL generation at scale.  Biography Brian Suchy is a Software Engineer within Google DeepMind. In his time at Google he has worked on F1 Query (Google's internal SQL query engine)\, hardware development\, and (of course) AI. Prior to joining Google\, Brian received his PhD student at Northwestern University\, advised by Peter Dinda\, with a focus on hardware/software codesign and memory management.  Research Interests: Artificial Intelligence\, Query Processing and Formal Logic  --- Zoom Link Panopto Link
LOCATION:Mudd Hall ( formerly Seeley G. Mudd Library)\, 3514\, 2233 Tech Drive\, Evanston\, IL 60208
TRANSP:OPAQUE
URL:https://planitpurple.northwestern.edu/event/642868
CREATED:20260622T050000Z
STATUS:CONFIRMED
LAST-MODIFIED:20260622T161041Z
PRIORITY:0
BEGIN:VALARM
TRIGGER:-PT10M
ACTION:DISPLAY
DESCRIPTION:Reminder
END:VALARM
END:VEVENT
END:VCALENDAR