<div dir="ltr">Dear all,<div><br></div><div><div>We look forward to seeing you<b> </b><b>this Tuesday (2/21)</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:</b> The speaker will be remote.</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 (2/21), <u>Chao Wang</u></span><b style="background-color:rgb(255,255,0)"> </b><span style="background-color:rgb(255,255,0)">(USC) will be giving a talk titled </span><b style="background-color:rgb(255,255,0)">"</b><b style="background-color:rgb(255,255,0)">Differential Verification of Deep Neural Networks</b><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>: Differential Verification of Deep Neural Networks<br><br></font><div><div><font color="#0b5394"><b>Talk Abstract</b>: Deep neural networks have become an integral component of many systems for which ensuring safety and robustness is crucial. In this talk, we present several abstract interpretation based methods for efficient verification of a class of safety properties called differential properties. While we focus on neural network equivalence as the canonical example, other interesting properties concerning input sensitivity and stability can also be cast as differential properties. Our key insight is in deriving sound abstractions that relate the intermediate computations of two structurally-similar neural networks, to accurately bound their maximum difference over all inputs. We also propose bound synthesis techniques for automatically generating linear abstractions of arbitrary nonlinear functions, to more efficiently handle architectures and activation functions beyond feed-forward ReLU networks. </font><div><div><font color="#0b5394"><br></font></div><div><font color="#0b5394"><b>Speaker Bio:</b> Chao Wang is an Associate Professor of Computer Science at the University of Southern California (USC). He develops formal verification and program synthesis techniques for principled design of systems to improve safety and security. He has published two books and more than 100 papers. The awards and recognition he received include a Young Investigator award from the U.S. Office of Naval Research (ONR), a CAREER award from the National Science Foundation (NSF), two ACM SIGSOFT Distinguished Paper awards, and a Best Journal Paper of the Year award from ACM Transactions on Design Automation of Electronic Systems.</font><br></div><div><br></div><div><font color="#0b5394"><b>In person:<span class="gmail-Apple-converted-space"> </span></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><div><br></div><div>Thanks,</div><div>Asher Trockman</div></div>