<div dir="ltr">Dear all,<div><br></div><div><div>We look forward to seeing you<b> </b><b>this Tuesday (4/18)</b> from <b><font color="#ff0000">1</font></b><font color="#ff0000"><b>2:00-1:00 PM (U.S. Eastern time)</b></font> for the next talk of this semester's <b>CMU AI Seminar</b>, sponsored by <a href="https://sambanova.ai/" target="_blank">SambaNova Systems</a>. The seminar will be held in GHC 6115 <b>with pizza provided </b>and will<b> </b>be streamed on Zoom. <b>Note: the speaker will be remote.</b></div><div><br></div><div>To learn more about the seminar series or to see the future schedule, please visit the <a href="http://www.cs.cmu.edu/~aiseminar/" target="_blank">seminar website</a>.</div><div><br></div><font color="#0b5394"><span style="background-color:rgb(255,255,0)">This Tuesday (4/18), <u>Sayan Mitra</u></span><b style="background-color:rgb(255,255,0)"> </b><span style="background-color:rgb(255,255,0)">(UIUC) will be giving a talk titled </span><b style="background-color:rgb(255,255,0)">"</b><span style="background-color:rgb(255,255,0)"><b>Assuring Safety of Learning-Enabled Systems with Perception Contracts</b></span><b style="background-color:rgb(255,255,0)">".</b></font></div><div><font color="#0b5394"><span style="background-color:rgb(255,255,0)"><br></span><b>Title</b>: Assuring Safety of Learning-Enabled Systems with Perception Contracts<br><br></font><div><font color="#0b5394"><b>Talk Abstract</b>: Formal verification of deep learning models remains challenging, and yet they are becoming integral in many safety-critical autonomous systems. We present an invariance and abstraction-based method for reasoning about end-to-end safety of such learning-enabled systems. The method constructs approximations of the DNN or perception models, called perception contracts, using system-level safety requirements and program analysis. Mathematically proving that a given perception model conforms to a contract remains a challenge, and may well be impractical, but empirical measures of conformance can provide confidence to safety claims. The resulting contracts are low-dimensional, intelligible, and can be used to verify end-to-end safety. We will discuss vision-based lane keeping and several other ongoing applications of this method and related future research challenges.</font><div><div><font color="#0b5394"><br></font></div><div><font color="#0b5394"><b>Speaker Bio:</b> Sayan is a Professor and John Bardeen Faculty Scholar of ECE at UIUC. Sayan received his PhD from MIT and his research is on formal verification and safe autonomy. His group is well-known for developing algorithms for data-driven verification and synthesis, some of which are being commercialized. His textbook on verification of cyber-physical systems was published in 2021.  Former PhD students from his group are now professors at Vanderbilt, NC Chapel Hill, MIT, and WashU. The group's work has been recognized with ACM Doctoral Dissertation Award, NSF CAREER Award, AFOSR YIP,  and several best paper awards.</font></div><div><br></div><div><font color="#0b5394"><b>In person: </b>GHC 6115</font></div><div><font color="#0b5394"><b>Zoom Link</b>:  <a href="https://cmu.zoom.us/j/99510233317?pwd=ZGx4aExNZ1FNaGY4SHI3Qlh0YjNWUT09" target="_blank">https://cmu.zoom.us/j/99510233317?pwd=ZGx4aExNZ1FNaGY4SHI3Qlh0YjNWUT09</a></font></div></div></div></div><div><br></div><div>Thanks,</div><div>Asher Trockman</div></div>