- talks - lists.cs.princeton.edu

Joey Dodds will present his pre-FPO on November 11 at 9am in Room 402.
by Nicki Gotsis 10 Nov '14

10 Nov '14

Joey Dodds will present his pre-FPO on Tuesday, November 11 at 9am in Room 402. The members of his committee are: Andrew Appel (advisor); David Walker and Jesper Bengtson, I.T. University of Copenhagen (readers); Sharad Malik and Aarti Gupta, NEC Labs America (nonreaders). Everyone is invited to attend his talk. The talk title and abstract follow below: "Symbolic Execution of C Programs by Computational Reflection" Verified Software Toolchain (VST) is a system for proving functional properties about C programs. It is completely implemented and proved correct in the Coq interactive proof assistant. VST is composed of a logic which allows a user to specify and reason about C programs, and Floyd, a proof automation system that allows forward symbolic execution of programs with their specifications. Floyd is implemented in Coq's tactic language, Ltac. There are two major problems with Ltac: as automation built in Ltac proceeds, Coq keeps a record of the steps that have been taken, called proof objects, that allow proofs to be checked once they are complete. These proofs can be large and very complex, causing Ltac automation to be both slow and memory hungry. The second problem with Ltac is that the flexibility of the language can lead to poor practices and slow execution. The Ltac match statement is the main cause of this issue. It allows matches against expressions of arbitrary type, and it allows backtracking when the body of a match fails. These combine to lead to confusing control flows, and slower execution than would be expected for a typed match with no backtracking. Fortunately, a technique known as computational reflection solves the problems associated with Ltac automation. Computational reflection allows automation without storing proof objects, greatly increasing speed while decreasing required memory. It also allows for principled and predictable implementations of algorithms that can be more robust and efficient than their Ltac counterparts. This thesis solves the problems with ltac by implementing reflective automation in two ways. The first is small-scale reflection. Small-scale reflection is built into the logic of VST, and uses computation to specify and check properties of programs within the logic rules. This has benefits regardless of the automation used because no proof objects need to be built about them because the computation itself is the proof. Large-scale reflection replaces the Ltac implementation of Floyd with symbolic execution by reflection. This is done using the MirrorCore library of Malecha et al. MirrorCore presents a general syntax capable of representing any Coq term, allowing computational reasoning where it would normally be impossible. Small-scale and large-scale reflection interact nicely because a well-designed large-scale reflection library will immediately be able to make use of the computation that is done as part of small-scale reflection.

1 0

Colloquium Speaker Greg Corrado today 4:30pm
by Nicole E. Wagenblast 10 Nov '14

10 Nov '14

Google Strength Neural Networks Greg Corrado, Research at Google Monday, November 10, 4:30pm Computer Science 105 Industrial scale applications of machine learning are surprisingly important in the products and services we enjoy today. Over the last few years classical artificial neural networks have reemerged as one of the most powerful, practical machine learning tools available. More than it was driven by algorithmic advances, this “deep learning” renaissance has been fueled by the availability of ever larger data stores and clever use of vast computational resources. Greg will describe Google's large scale distributed neural network framework and the applications of neural networks to the domains of image recognition, speech recognition, and text understanding. Greg Corrado is a senior research scientist at Google working in artificial intelligence, computational neuroscience, and scalable machine learning. He has worked for some time on brain inspired computing, and most recently has served as one of the founding members and a technical lead on Google's large scale deep learning project. Before coming to Google, he worked at IBM Research on the SyNAPSE neuromorphic silicon chip. He did his graduate work in Neuroscience and in Computer Science at Stanford University, and his undergraduate in work Physics at Princeton University.

1 0

Colloquium Speaker Greg Corrado Mon Nov 10, 4:30pm
by Nicole E. Wagenblast 09 Nov '14

09 Nov '14

Google Strength Neural Networks Greg Corrado, Research at Google Monday, November 10, 4:30pm Computer Science 105 Industrial scale applications of machine learning are surprisingly important in the products and services we enjoy today. Over the last few years classical artificial neural networks have reemerged as one of the most powerful, practical machine learning tools available. More than it was driven by algorithmic advances, this “deep learning” renaissance has been fueled by the availability of ever larger data stores and clever use of vast computational resources. Greg will describe Google's large scale distributed neural network framework and the applications of neural networks to the domains of image recognition, speech recognition, and text understanding. Greg Corrado is a senior research scientist at Google working in artificial intelligence, computational neuroscience, and scalable machine learning. He has worked for some time on brain inspired computing, and most recently has served as one of the founding members and a technical lead on Google's large scale deep learning project. Before coming to Google, he worked at IBM Research on the SyNAPSE neuromorphic silicon chip. He did his graduate work in Neuroscience and in Computer Science at Stanford University, and his undergraduate in work Physics at Princeton University.

1 0

Colloquium Speaker Ryan Adams Thurs Nov 13, 4:30pm
by Nicole E. Wagenblast 07 Nov '14

07 Nov '14

Better Science Through Better Bayesian Computation Ryan Adams, Harvard University Thursday, November 13, 4:30pm Computer Science 105 As we grapple with the hype of "big data" in computer science, it is important to remember that the data are not the central objects: we collect data to answer questions and inform decisions in science, engineering, policy, and beyond. In this talk, I will discuss my work in developing tools for large-scale data analysis, and the scientific collaborations in neuroscience, chemistry, and astronomy that motivate me and keep this work grounded. I will focus on two lines of research that I believe capture an important dichotomy in my work and in modern probabilistic modeling more generally: identifying the "best" hypothesis versus incorporating hypothesis uncertainty. In the first case, I will discuss my recent work in Bayesian optimization, which has become the state-of-the-art technique for automatically tuning machine learning algorithms, finding use across academia and industry. In the second case, I will discuss scalable Markov chain Monte Carlo and the new technique of Firefly Monte Carlo, which is the first provably correct MCMC algorithm that can take advantage of subsets of data. Ryan Adams is an Assistant Professor of Computer Science at Harvard University, in the School of Engineering and Applied Sciences. He leads the Harvard Intelligent Probabilistic Systems group, whose research focuses on machine learning and computational statistics, with applied collaborations across the sciences. Ryan received his undergraduate training in EECS at MIT and completed his Ph.D. in Physics at Cambridge University as a Gates Cambridge Scholar under David MacKay. He was a CIFAR Junior Research Fellow at the University of Toronto before joining the faculty at Harvard. His Ph.D. thesis received Honorable Mention for the Leonard J. Savage Award for Bayesian Theory and Methods from the International Society for Bayesian Analysis. Ryan has won paper awards at ICML, AISTATS, and UAI, and received the DARPA Young Faculty Award.

1 0

Colloquium Speaker Matthew Green Wed Nov 5, 4:30pm
by Nicole E. Wagenblast 05 Nov '14

05 Nov '14

Decentralized Anonymous Credentials and Electronic Payments from Bitcoin Matthew Green (Johns Hopkins University) Wednesday, November 5, 2014 - 4:30pm to 5:30pm Computer Science 105 Traditionally, making statements about identity on the Internet, whether literal assertions of identity or statements about one’s identity, requires centralized providers who issue credentials attesting to the user’s information. These organizations, which include Certificate Authorities, DNS maintainers, or login providers like Google and Facebook, play a large role in securing internet infrastructure, email, and financial transactions. Our increasing reliance on these providers raises concerns about privacy and trust. Anonymous credentials represent a powerful solution to this privacy concern: they deprive even colluding credential issuers and verifiers of the ability to identify and track their users. Although credentials may involve direct assertions of identity, they may also be used for a large range of useful assertions, such as “my TPM says my computer is secure”, “I have a valid subscription for content”, or “I am eligible to vote.” Anonymous credentials can also be used as a basis for constructing untraceable electronic payment systems, or “e-cash". Unfortunately most existing anonymous credential and e-cash systems have a fundamental limitation: they require the appointment of a central, trusted party to issue credentials or tokens. This issuer represents a single point of failure and an obvious target for compromise. In distributed settings such as ad hoc or peer-to-peer networks, it may be challenging even to identify parties who can be trusted to play this critical role. In this talk I will discuss new techniques for building anonymous credentials and electronic cash in a fully decentralized setting. The basic ingredient of these proposals is a "distributed public append-only ledger", a technology which has most famously been deployed in digital currencies such as Bitcoin. This ledger can be employed by individual nodes to make assertions about a user’s attributes in a fully anonymous fashion — without the assistance of a credential issuer. One concrete result of these techniques is a new protocol named “Zerocash”, which adds cryptographically unlinkable electronic payments to the Bitcoin currency. Prof. Matthew Green is a Research Professor at the Johns Hopkins University Information Security Institute. His research focus is on cryptographic techniques for maintaining users’ privacy, and on technologies that enable the deployment of privacy-preserving protocols. From 2004-2011, Green served as CTO of Independent Security Evaluators, a custom security evaluation firm with a global client base. Along with a team at Johns Hopkins and RSA Laboratories, he discovered flaws in the Texas Instruments Digital Signature Transponder, a cryptographically-enabled RFID device used in the Exxon Speedpass payment system and in millions of vehicle immobilizers. Nicole Wagenblast Computer Science Department Princeton University 35 Olden Street Princeton, NJ 08540 609-258-4624

1 2

Colloquium Speaker Greg Corrado Mon Nov 10, 4:30pm
by Nicole E. Wagenblast 04 Nov '14

04 Nov '14

Google Strength Neural Networks Greg Corrado, Research at Google Monday, November 10, 4:30pm Computer Science 105 Industrial scale applications of machine learning are surprisingly important in the products and services we enjoy today. Over the last few years classical artificial neural networks have reemerged as one of the most powerful, practical machine learning tools available. More than it was driven by algorithmic advances, this “deep learning” renaissance has been fueled by the availability of ever larger data stores and clever use of vast computational resources. Greg will describe Google's large scale distributed neural network framework and the applications of neural networks to the domains of image recognition, speech recognition, and text understanding. Greg Corrado is a senior research scientist at Google working in artificial intelligence, computational neuroscience, and scalable machine learning. He has worked for some time on brain inspired computing, and most recently has served as one of the founding members and a technical lead on Google's large scale deep learning project. Before coming to Google, he worked at IBM Research on the SyNAPSE neuromorphic silicon chip. He did his graduate work in Neuroscience and in Computer Science at Stanford University, and his undergraduate in work Physics at Princeton University.

1 0

Colloquium Speaker Daniel Lee Monday Nov 3 4:30pm
by Nicole E. Wagenblast 03 Nov '14

03 Nov '14

Machine Learning for Robots: Perception, Planning and Motor Control Daniel Lee, University of Pennsylvania Monday, November 3, 2014 - 4:30pm to 5:30pm Computer Science 105 Machines today excel at seemingly complex games such as chess and Jeopardy, yet still struggle with basic perceptual, planning, and motor tasks in the physical world. What are the appropriate representations needed to execute and adapt robust behaviors in real-time? I will present some examples of learning algorithms from my group that have been applied to robots for monocular visual odometry, high-dimensional trajectory planning, and legged locomotion. These algorithms employ a variety of techniques central to machine learning: dimensionality reduction, online learning, and reinforcement learning. I will show and discuss applications of these algorithms to autonomous vehicles and humanoid robots. Daniel Lee is the Evan C Thompson Term Chair, Raymond S. Markowitz Faculty Fellow, and Professor in the School of Engineering and Applied Science at the University of Pennsylvania. He received his B.A. summa cum laude in Physics from Harvard University in 1990 and his Ph.D. in Condensed Matter Physics from the Massachusetts Institute of Technology in 1995. Before coming to Penn, he was a researcher at AT&T and Lucent Bell Laboratories in the Theoretical Physics and Biological Computation departments. He is a Fellow of the IEEE and has received the National Science Foundation CAREER award and the University of Pennsylvania Lindback award for distinguished teaching. He was also a fellow of the Hebrew University Institute of Advanced Studies in Jerusalem, an affiliate of the Korea Advanced Institute of Science and Technology, and organized the US-Japan National Academy of Engineering Frontiers of Engineering symposium. As director of the GRASP Robotics Laboratory and co-director of the CMU-Penn University Transportation Center, his group focuses on understanding general computational principles in biological systems, and on applying that knowledge to build autonomous systems.

1 2

Colloquium Speaker Ryan Adams Thurs Nov 13, 4:30pm
by Nicole E. Wagenblast 30 Oct '14

30 Oct '14

Better Science Through Better Bayesian Computation Ryan Adams , Harvard University Thursday, November 13, 4:30pm Computer Science 105 As we grapple with the hype of "big data" in computer science, it is important to remember that the data are not the central objects: we collect data to answer questions and inform decisions in science, engineering, policy, and beyond. In this talk, I will discuss my work in developing tools for large-scale data analysis, and the scientific collaborations in neuroscience, chemistry, and astronomy that motivate me and keep this work grounded. I will focus on two lines of research that I believe capture an important dichotomy in my work and in modern probabilistic modeling more generally: identifying the "best" hypothesis versus incorporating hypothesis uncertainty. In the first case, I will discuss my recent work in Bayesian optimization, which has become the state-of-the-art technique for automatically tuning machine learning algorithms, finding use across academia and industry. In the second case, I will discuss scalable Markov chain Monte Carlo and the new technique of Firefly Monte Carlo, which is the first provably correct MCMC algorithm that can take advantage of subsets of data. Ryan Adams is an Assistant Professor of Computer Science at Harvard University, in the School of Engineering and Applied Sciences. He leads the Harvard Intelligent Probabilistic Systems group, whose research focuses on machine learning and computational statistics, with applied collaborations across the sciences. Ryan received his undergraduate training in EECS at MIT and completed his Ph.D. in Physics at Cambridge University as a Gates Cambridge Scholar under David MacKay. He was a CIFAR Junior Research Fellow at the University of Toronto before joining the faculty at Harvard. His Ph.D. thesis received Honorable Mention for the Leonard J. Savage Award for Bayesian Theory and Methods from the International Society for Bayesian Analysis. Ryan has won paper awards at ICML, AISTATS, and UAI, and received the DARPA Young Faculty Award.

1 0

ORFE Miscellaneous Talk: Venkat Chandrasekaran, Thursday, Oct. 30th at 2:00pm, Sherrerd Hall, 101
by Nicole E. Wagenblast 23 Oct '14

23 Oct '14

=== ORFE Miscellaneous Talk Announcement === DATE: Thursday, October 30, 2014 TIME: 2:00pm LOCATION: Sherrerd Hall, 101 SPEAKER: Venkat Chandrasekaran, California Institute of Technology TITLE: Relative Entropy Relaxations for Signomial Optimization ABSTRACT: The relative entropy function plays a prominent role in a variety of contexts in information theory and statistics. In this talk, we discuss some of its beneficial computational properties that are a consequence of its joint convexity with respect to both its arguments. Signomial programs (SPs) are optimization problems specified in terms of signomials, which are weighted sums of exponentials composed with linear functionals of a decision variable. SPs are non-convex optimization problems in general, and families of NP-hard problems can be reduced to SPs. We describe a hierarchy of convex relaxations to obtain successively tighter lower bounds of the optimal value of SPs. This sequence of lower bounds is computed by solving increasingly larger-sized relative entropy optimization problems, which are convex programs specified in terms of linear and relative entropy functions. Our approach relies crucially on the observation that the relative entropy function provides a convex parametrization of certain sets of globally nonnegative signomials with efficiently computable nonnegativity certificates via the arithmetic-geometric-mean inequality. By appealing to representation theorems from real algebraic geometry, we show that our sequences of lower bounds converge to the global optima for broad classes of SPs. Finally, we also demonstrate the effectiveness of our methods via numerical experiments. (Joint work with Parikshit Shah) **********************************************************

1 0

Colloquium Speaker Yann LeCun Today, 4:30pm
by Nicole E. Wagenblast 22 Oct '14

22 Oct '14

Yann LeCun, Facebook AI Research and Center for Data Science, New York University The Unreasonable Effectiveness of Deep Learning Wednesday, October 22 , 4:30pm Computer Science 105 The emergence of large datasets, parallel computers, and new machine learning methods, have enabled the deployment of highly-accurate computer perception systems and are opening the door to a wide deployment of AI systems. A key component in AI systems is a module, sometimes called a feature extractor, that turns raw inputs into suitable internal representations. But designing and building such a module requires a considerable amount of engineering efforts and domain expertise. Deep Learning methods have provided a way to automatically learn good representations of data from labeled or unlabeled samples. Deep architectures are composed of successive stages in which data representations are increasingly global, abstract, and invariant to irrelevant transformations of the input. Deep learning enables end-to-end training of these architectures, from raw inputs to ultimate outputs. The convolutional network model (ConvNet) is a particular type of deep architecture somewhat inspired by biology, which consists of multiple stages of filter banks, interspersed with non-linear operators, and spatial pooling. ConvNets have become the record holder for a wide variety of benchmarks, including object detection, localization and recognition in image, semantic segmentation and labeling, face recognition, acoustic modeling for speech recognition, drug design, handwriting recognition, biological image segmentation, etc. The most recent systems deployed by Facebook, Google, NEC, IBM, Microsoft, Baidu, Yahoo and others for image understanding, speech recognition, and natural language processing use deep learning. Many of these systems use very large and very deep ConvNets with billions of connections, trained in supervised mode. But many new applications require the use of unsupervised feature learning. A number of such methods based on sparse auto-encoder will be presented. Several applications will be shown through videos and live demos, including a category-level object recognition system that can be trained on the fly, a scene parsing system that can label every pixel in an image with the category of the object it belongs to (scene parsing), an object localization and detection system, and several natural language processing systems. Specialized hardware architectures that run these systems in real time will also be described. Yann LeCun is Director of AI Research at Facebook, and Silver Professor of Data Science, Computer Science, Neural Science, and Electrical Engineering at New York University, affiliated with the NYU Center for Data Science, the Courant Institute of Mathematical Science, the Center for Neural Science, and the Electrical and Computer Engineering Department. He received the Electrical Engineer Diploma from Ecole Supérieure d'Ingénieurs en Electrotechnique et Electronique (ESIEE), Paris in 1983, and a PhD in Computer Science from Université Pierre et Marie Curie (Paris) in 1987. After a postdoc at the University of Toronto, he joined AT&T Bell Laboratories in Holmdel, NJ in 1988. He became head of the Image Processing Research Department at AT&T Labs-Research in 1996, and joined NYU as a professor in 2003, after a brief period as a Fellow of the NEC Research Institute in Princeton. From 2012 to 2014 he directed NYU's initiative in data science and became the founding director of the NYU Center for Data Science. He was named Director of AI Research at Facebook in late 2013 and retains a part-time position on the NYU faculty. His current interests include AI, machine learning, computer perception, mobile robotics, and computational neuroscience. He has published over 180 technical papers and book chapters on these topics as well as on neural networks, handwriting recognition, image processing and compression, and on dedicated circuits and architectures for computer perception. The character recognition technology he developed at Bell Labs is used by several banks around the world to read checks and was reading between 10 and 20% of all the checks in the US in the early 2000s. His image compression technology, called DjVu, is used by hundreds of web sites and publishers and millions of users to access scanned documents on the Web. Since the mid 1980's he has been working on deep learning methods, particularly the convolutional network model, which is the basis of many products and services deployed by companies such as Facebook, Google, Microsoft, Baidu, IBM, NEC, AT&T and others for image and video understanding, document recognition, human-computer interaction, and speech recognition. LeCun has been on the editorial board of IJCV, IEEE PAMI, and IEEE Trans. Neural Networks, was program chair of CVPR'06, and is chair of ICLR 2013 and 2014. He is on the science advisory board of Institute for Pure and Applied Mathematics, and Neural Computation and Adaptive Perception Program of the Canadian Institute for Advanced Research. He has advised many large and small companies about machine learning technology, including several startups he co-founded. He is the lead faculty at NYU for the Moore-Sloan Data Science Environment, a $36M initiative in collaboration with UC Berkeley and University of Washington to develop data-driven methods in the sciences. He is the recipient of the 2014 IEEE Neural Network Pioneer Award.

1 0