Monday / CS Seminar

October 5 / 12:00 PM

Hybrid / Mudd 3514

Speaker

Brian Suchy, Software Engineer Google DeepMind

Talk Title

Google Relational Modeling Framework: Proving Relational Equivalence at Scale

Abstract

GenAI is accelerating computer science in nearly every way. From development and research to deployment, AI has the potential to enable huge sweeping changes to engineering workflows along the entire computing stack; however, to truly realize the potential for this, we must build the foundations for these workflows to be able to operate autonomously with minimal human intervention.

One of these building blocks, Google Relational Modeling Framework (GRMF), generalizes relational logic, including GoogleSQL, Common Expression Language (CEL), Datalog, and (conditionally) NumPy/Pandas, into a unified Relational Algebra-based Dialect. In this talk, we dive into one of GRMF's use cases of enabling sound, deterministic verification by formally proving equivalence between relational statements.

We examine the inner workings of multi-layered formal proving methods (ranging from e-graphs and $k$-semirings to SMT solvers like Z3/CVC5) and detail real-world production use cases. Finally, we explore future applications of GRMF, including automated cross-engine query migration (e.g., BigQuery $\leftrightarrow$ F1), JIT compilation of SQL queries, execution of NumPy programs via F1/Voxel, and its potential as a general MLIR query optimizer

Biography

Brian Suchy is a Senior Software Engineer at Google DeepMind. He works in several areas including: hardware development, formal verification, and (of course) AI.

Brian graduated with his PhD from Northwestern in 2017. He worked in the Prescience Lab, led by Dr. Peter Dinda, with a focus on Software-based Memory Management

Research Interests: Databases, Architecture, Formal Logic