- talks - lists.cs.princeton.edu

Colloquium Speaker Dougal Maclaurin: Tuesday, Oct 15
by Emily C. Lawrence 09 Oct '19

09 Oct '19

CS Colloquium Speaker Dougal Maclaurin from Google Brain Tuesday, October 15 - 12:30pm Computer Science - Room 105 Host: Ryan Adams [ https://www.cs.princeton.edu/events/25877 | https://www.cs.princeton.edu/events/25877 ] JAX: Accelerated machine learning research via composable function transformations in Python JAX is a system for high-performance machine learning research. It offers the familiarity of Python+NumPy and the speed of hardware accelerators, and it enables the definition and the composition of function transformations useful for machine learning programs. In particular, these transformations include automatic differentiation, automatic batching, end-to-end-compilation (via XLA), and parallelizing over multiple accelerators. They are the key to JAX's power and to its relative simplicity. JAX had its initial open-source release in December 2018 (https://github.com/google/jax). It is currently being used by several groups of researchers for a wide range of advanced applications, from studying spectra of neural networks, to probabilistic programming and Monte Carlo methods, and scientific applications in physics and biology. Users appreciate JAX most of all for its ease of use and flexibility. Bio: Dougal Maclaurin is a research scientist at Google. He works on programming languages and systems for machine learning, particularly the Python library JAX. He started Autograd , a system for automatic differentiation in Python, which has inspired the design of several systems, including PyTorch , MinPy , Torch Autograd and Julia Autograd . He is a co-founder of Day Zero Diagnostics, a startup developing a sequencing-based diagnostic for drug-resistant infections. He received his Ph.D. from Harvard in 2016, working with Ryan Adams on the development of methods for machine learning. His work on scalable MCMC, "Firefly Monte Carlo", was recognized with the Best Paper award at UAI 2014.

1 0

Caroline Trippel will present her FPO, "Concurrency and Security Verification in Heterogeneous Parallel Systems" on Friday, 10/18/2019 at 9am in CS 105
by Nicki Mahler 08 Oct '19

08 Oct '19

Caroline Trippel will present her FPO, "Concurrency and Security Verification in Heterogeneous Parallel Systems" on Friday, 10/18/2019 at 9am in CS 105. The members of her committee are: Margaret Martonosi (Adviser); Readers: Aarti Gupta, Dan Lustig (NVIDIA), and Margaret Martonosi; Examiners: Andrew Appel, David Wentzlaff, and Margaret Martonosi. A copy of her thesis, is available upon request. Please email ngotsis(a)cs.princeton if you would like a copy of the thesis. Everyone is invited to attend her talk. The talk title and abstract follow below: To achieve performance scaling at manageable power and thermal levels, modern systems architects employ parallelism along with high degrees of hardware specialization and heterogeneity. Unfortunately, the power and performance improvements afforded by heterogeneous parallelism come at the cost of significantly increased design complexity, with different components being programmed differently and accessing shared resources differently. This design complexity in turn presents challenges for architects who need to devise mechanisms for orchestrating, enforcing, and verifying the correctness and security of executing applications. As it turns out, software-level correctness and security problems can result from problematic hardware event orderings and interleavings that take place when an application executes on a particular hardware implementation. Since hardware designs are complex, and since a single user-facing instruction can exhibit a variety of different hardware execution event sequences, analyzing and verifying systems for correct and secure orderings and interleavings of these events is challenging. To address this issue, this dissertation combines hardware systems architecture approaches with formal methods techniques to support the specification, analysis, and verification of implementation-aware event ordering scenarios. The specific goal here is enabling automatic synthesis of implementation-aware programs capable of violating correctness or security guarantees when such programs exist. First, this dissertation presents TriCheck, an approach and tool for conducting full-stack memory consistency model verification (from high-level programming languages down through hardware implementations). Using rigorous and ecient formal approaches, TriCheck identified flaws in the 2016 RISC-V memory model specification and two counterexamples to a previously proven-correct compiler mapping scheme from C11 onto Power and ARMv7. Second, after making the important observation that memory consistency model and security analyses are amenable to similar approaches, this thesis presents CheckMate, an approach and tool for conducting hardware security verification. CheckMate uses formal techniques to evaluate susceptibility of a hardware system design to formally-specified security exploit classes. When a design is susceptible, proof-ofconcept exploit codes are synthesized. CheckMate automatically synthesized programs representative of Meltdown and Spectre and new exploits, MeltdownPrime and SpectrePrime. Third, this dissertation presents approaches for handling memory model heterogeneity in hardware systems, focusing on correctness and highlighting applicability of the proposed techniques to security.

1 0

Olivier Savary Belanger will present his FPO "Verified Extraction for Coq" on Thursday, 10/17/2019 at 10:30am in CS 401
by Nicki Mahler 07 Oct '19

07 Oct '19

Olivier Savary Belanger will present his FPO "Verified Extraction for Coq" on Thursday, 10/17/2019 at 10:30am in CS 401. The members of his committee are: Andrew Appel (Adviser); Examiners: Zachary Kincaid, Lennart Beringer, and Andrew Appel; Readers: David Walker and John Gregory Morrisett (Cornell University) A copy of his thesis is available upon request. Please email [ mailto:ngotsis@cs.princeton | ngotsis(a)cs.princeton ] if you would like a copy of the thesis. Everyone is invited to attend his talk. The talk abstract follows below. Interactive theorem provers allow for the development, in the same environment, of programs and of proofs about them. The programmatic portion of the development can then be extracted to code which is then compiled into an executable. However, unless both the extraction and compilation processes are formally verified, one has no guarantees that the proofs developed still apply to the resulting executable. This thesis describes my work on CertiCoq, a verified extraction pipeline for the Coq theorem prover composing with the CompCert C verified compiler to achieve end-toend correctness guarantees. I present a proof framework to prove optimizations over the continuation-passing style (CPS) intermediate representation (IR) used in CertiCoq. This framework has been used by me and others to prove the correctness of nontrivial optimizations. I focus on a novel proof of correctness for a shrink reduction algorithm, a transformation combining in a single pass multiple optimizations which always result in smaller terms. I also present a verified code generation translating the CPS IR into Clight, a front-end language of CompCert. I show how it interfaces with a verified garbage collector and how its proof composes with the proof of correctness of CompCert. Taken together, this thesis shows how carefuly crafted intermediate languages facilitate verification e↵ort in the context of an optimizing compiler.

1 0

CS Colloquium Speaker: Alexa Meade, Monday, Oct 14 at 4:30pm
by Emily C. Lawrence 07 Oct '19

07 Oct '19

CS Colloquium Speaker Alexa Meade Monday, October 14 - 4:30pm James Stewart Theater Lewis Center for the Arts, 185 Nassau Street Hosts: Adam Finkelstein & Jeff Whetstone [ https://www.cs.princeton.edu/events/25887 | https://www.cs.princeton.edu/events/25887 ] Painting in More Dimensions Artist Alexa Meade paints on the human body and three-dimensional spaces, creating the illusion that our reality is a two-dimensional painting. She will discuss her artistic process and collaborations with mathematicians, magicians, and theoretical physicists. Bio: Alexa Meade has developed a style for painting on the human body and three-dimensional spaces, creating the illusion that our reality is a two-dimensional painting. Her groundbreaking work has been exhibited around the world at the Grand Palais in Paris, the United Nations in New York, the Smithsonian National Portrait Gallery in Washington, DC and Shibuya Crossing in Tokyo. Her solo show on Rodeo Drive in Beverly Hills was attended by forty-thousand people. She has created large scale interactive installations at Coachella, Cannes Lions, and Art Basel. Alexa has been commissioned by BMW, Sony, Adidas, and the San Francisco Symphony Orchestra. She painted pop star Ariana Grande for her iconic “God is a Woman” music video, which has about 250 million views. Alexa has lectured at TED, Apple, and Stanford and accepted an invitation to the White House under President Obama. She has been honored with the "Disruptive Innovation Award" by the Tribeca Film Festival and has been Artist-in-Residence at both Google and the Perimeter Institute for Theoretical Physics. InStyle has named Alexa among their "Badass Women."

1 0

Oct 9: Maximal Mutual Information Predictive Coding for Natural Language Processing, Karl Stratos (Rutgers)
by Danqi Chen 03 Oct '19

03 Oct '19

Location: CS 402 Date: Oct 9, 2019 Time: 3-4pm Title: Maximal Mutual Information Predictive Coding for Natural Language Processing Abstract: Neural predictive coding is an enormously successful approach to unsupervised representation learning in natural language processing. In this approach, a large-scale neural language model is trained to predict the missing signal (e.g., next word, next sentence) and the trained model is used in downstream tasks to produce useful text representations. While effective, it is computationally difficult to work with and yields uninterpretable representations. In this talk, I will present a new approach to neural predictive coding based on maximal mutual information (MMI). Instead of predicting the raw missing signal, we define a set of interpretable latent "codes" and directly predict the underlying code of the missing signal. The model is trained by maximizing the mutual information between the predicted codes. I will first present a simple and effective MMI predictive coding neural model that pushes the state-of-the-art performance in unsupervised part-of-speech tagging. I will next discuss an ongoing work on generalizing MMI predictive coding to structured representations. Bio: Karl Stratos is an assistant professor in the Computer Science Department at Rutgers University. His research centers on statistical approaches to unsupervised learning in natural language processing. He completed a PhD in computer science from Columbia University in 2016. During PhD, he was advised by Michael Collins and also worked closely with Daniel Hsu. After PhD, he was a senior research scientist at Bloomberg LP (2016-2017) and a research assistant professor at Toyota Technological Institute at Chicago (2017-2019). -- *Danqi Chen* http://www.cs.princeton.edu/~danqic/

1 0

Distinguished CS Colloquium Speaker Ramón Cáceres: Wednesday, Oct 16
by Emily C. Lawrence 02 Oct '19

02 Oct '19

Distinguished CS Colloquium Speaker Ramón Cáceres from Google Wednesday, October 16 - 1:30pm Computer Science - Room 105 Host: Margaret Martonosi [ https://www.cs.princeton.edu/events/25878 | https://www.cs.princeton.edu/events/25878 ] Zanzibar: Google’s Consistent, Global Authorization System Determining whether online users are authorized to access digital objects is central to preserving privacy. This talk presents the design, implementation, and deployment of Zanzibar, a global system for storing and evaluating access control lists. Zanzibar provides a uniform data model and configuration language for expressing a wide range of access control policies from hundreds of client services at Google, including Calendar, Cloud, Drive, Maps, Photos, and YouTube. Its authorization decisions respect causal ordering of user actions and thus provide external consistency amid changes to access control lists and object contents. Zanzibar scales to trillions of access control lists and millions of authorization requests per second to support services used by billions of people. It has maintained 95th-percentile latency of less than 10 milliseconds and availability of greater than 99.999% over 3 years of production use. Bio: Ramón Cáceres is a software engineer at Google. He was previously a researcher at AT&T Labs and IBM Research. His areas of focus include computer systems and networks, mobile computing services and applications, and location data analysis and modeling. He holds a PhD in Computer Science from the University of California at Berkeley. He is an IEEE Fellow and an ACM Distinguished Scientist.

1 0

EE Lunch Seminar - Thursday, October 17, 2019, 12:30 pm, E-Quad B205 - Mohsen Imani, University of California San Diego
by Emily Lawrence 02 Oct '19

02 Oct '19

Department of Electrical Engineering Seminar Speaker: Mohsen Imani, University of California San Diego Title: Towards Learning with Brain Efficiency Date: Thursday, October 17, 2019 Time: 12:30 pm (pizza will be served) Room: E-Quad, Room B205 Host: Prof. Niraj Jha Abstract: Modern computing systems are plagued with significant issues in efficiently performing learning tasks. In this talk, I will present a new brain-inspired computing architecture. It supports a wide range of learning tasks while offering higher system efficiency than the other existing platforms. I will first focus on HyperDimensional (HD) computing, an alternative method of computation which exploits key principles of brain functionality: (i) robustness to noise/error and (ii) intertwined memory and logic. To this end, we design a new learning algorithm resilient to hardware failure. We then build the architecture exploiting emerging technologies to enable processing in memory. I will also show how we use the new architecture to accelerate other brain-like computations such as deep learning and other big data processing. Bio: Mohsen Imani is a Ph.D. candidate in the Department of Computer Science and Engineering at UC San Diego. His research interests are in brain-inspired computing and computer architecture. He is an author of more than 85 publications at top tier conferences and journals. His contributions resulted in over $40M grants funded from multiple governmental agencies (NSF, SRC) and several companies including IBM, Intel, Micron, and Qualcomm. He has received the most prestigious awards from the UCSD school of engineering including the Gordon Engineering Leadership Award and the Outstanding Graduate Research Award. He also got several nominations for the best paper awards from multiple conferences. Mohsen will be in the academic job market this year.

1 0

Oct 2: Diverse Decoding from Neural Sequence Models, Ashwin Kalyan (Georgia Tech)
by Karthik Narasimhan 01 Oct '19

01 Oct '19

Location: CS 402 Date: Oct 2, 2019 Time: 3 - 4pm Title: Diverse Decoding from Neural Sequence Models Abstract: Consider assistive technology like Google’s auto response that suggests replies with multiple intents. The ability to produce multiple diverse outputs is an integral component of such assistive systems and further, the fundamental problem of producing diverse outputs shows up across domains. In this talk, I will first introduce Diverse Beam Search (DBS) — a modification to the popular Beam Search algorithm that encourages diversity in the sequences decoded from neural sequence models. Then, I will present 𝛁BS, a fully-differentiable variant that directly models sets of sequences while optimizing more general set-level metrics including diversity. While both algorithms are task-agnostic, I will discuss their effectiveness in the context of image captioning. Bio: Ashwin Kalyan is a PhD student at Georgia Tech advised by Prof. Dhruv Batra. He is interested in developing machine learning solutions for producing diverse outputs, developing fast and accurate reasoning systems and modeling human preferences — all essential components of effective assistive technology. During his PhD, he has interned at Microsoft Research and IBM. He is also a professional violinist specializing in Karnatic Classical Music.

1 1

FW: Kurt James Werner visiting electronic music circuit modeling lecture this Wednesday, Sept 25, 5pm
by Emily Lawrence 23 Sep '19

23 Sep '19

I'm excited to let people know about a talk being presented by a visitor on Wednesday, Sept 25, at 5pm, in the PLOrk studio (Effron Music Building). Kurt James Werner will be visiting and talking about his music and giving an introduction to the techniques he uses to model analog audio circuits digitally, Wave Digital Filters (WDF). All are welcome, it's FREE and open to the public. Hope to see you there! Jeff Snyder Director of Electronic Music Princeton University --- Details below: WHEN: Wednesday, Sept 25 5pm-7pm WHERE: PLOrk Studio on the Forum Level of the Effron Music Building (in the new Lewis Arts Complex) FREE and open to the public Title: Virtual Analog Modeling using Wave Digital Filters: a Tutorial Introduction Bio: Dr. Kurt James Werner conducts research related to virtual analog (especially Wave Digital Filters), the history of music technology, 1-bit music, computer modeling of circuit-bent instruments, & sound synthesis more broadly. As part of his Ph.D. in Computer-Based Music Theory and Acoustics from Stanford University's Center for Computer Research in Music and Acoustics (CCRMA), he wrote a doctoral dissertation “Virtual Analog Modeling of Audio Circuitry Using Wave Digital Filters.” This greatly expanded the class of circuits that can be modeled using the Wave Digital Filter approach, using the classic Roland TR-808 bass drum circuit as a case study. As a researcher, he has also worked on the history of analog drum machine circuits. As a composer, his music references elements of chiptunes, musique concrète, circuit bending, algorithmic/generative composition, & breakbeat. As a Lecturer in Audio, he was based out of the Sonic Arts Research Centre (SARC) of Queen's University Belfast for several years, and will soon (in 1 week!) start a new position as a Research Engineer at iZotope, Inc. in Cambridge, MA. Synopsis: In this tutorial, the basics of the "Wave Digital Filter" (WDF) approach to virtual analog modeling will be presented. The WDF concept was introduced as a generic digital filter design technique by Alfred Fettweis in the 1970s, and has been picked up slowly by the audio DSP community starting in the early 2000s. Today, WDFs are capable of modeling audio circuits with complex topologies (bridges, feedback, &c.) and multiple nonlinearities (diodes, transistors, &c.) and can be considered one of the main approaches to modeling audio circuits in software. A wide variety of audio circuits have been successfully modeled, including the Roland TR-808 bass drum, amplifier tone stacks, Ibanez Tube Screamer, OTA-based state variable filters, tone boosters, the Electro-Harmonix Big Muff Pi, the Korg MS-50 VCF, & Fender and Mesa Boogie preamplifiers. The main focus of the talk will be the basic mathematical concepts that underpin WDF modeling and tutorial examples, including a simple RC lowpass filter & the Hammond organ vibrato/chorus circuit. Some progress on modeling a mysterious analog filter from the Experimental Music Studios (EMS) of the University of Illinois at Urbana-Champaign (UIUC) will also be presented. -- Composer, musician, instrument designer scattershot.org <http://scattershot.org> * @snyderphonics

1 0

Reminder: Colloquium Speaker Muhammad Jehangir Amjad : TODAY at 1:30pm
by Emily C. Lawrence 18 Sep '19

18 Sep '19

Colloquium Speaker Muhammad Jehangir Amjad from Google Wednesday, September 18 - 1:30pm Computer Science - Room 105 Host: Jennifer Rexford [ https://www.cs.princeton.edu/events/25874 | https://www.cs.princeton.edu/events/25874 ] Challenges in Cloud Networking Google's products, e.g. Search, YouTube, Gmail, etc. are used by billions of people the world over. Google Cloud hosts some of the most popular services in the world. Building systems that scale to support all these applications is among the greatest challenges at the company. Underlying all these systems is the network which must enable low-latency, high throughput, high capacity, high availability and secure access to compute and storage. While Google has been enormously successful in achieving these goals, cloud networking faces exciting new challenges today. With the demise of Moore's Law and explosive data growth, the implications for the performance, reliability, predictability and cost efficiency on networking, from hardware to communication protocols, will be profound. This talk will focus on highlighting some of the challenges in networking alluded to above. Additionally, we will discuss the current and future challenges in network telemetry systems and Google's approach to overcoming these challenges via statistical inference which allows us to estimate that which cannot be measured. Bio: Muhammad Jehangir Amjad is a Software Engineer in the Network Infrastructure team at Google working on inference and statistical learning on data produced by network telemetry systems. He joined Google from MIT where he has an appointment as a Lecturer of Machine Learning in CSAIL. Jehangir received his PhD from the Operations Research Center (ORC) and Laboratory of Information and Decision Systems (LIDS) at MIT, under the supervision of Prof Devavrat Shah. He received his BSE in Electrical Engineering from Princeton University.

1 0