[Colloquium] REMINDER: 10/29 TTIC Colloquium: Christian Szegedy, Google

[Mary Marre via Colloquium]

*When:    *  Monday, October 29th at 11:00 am

*Where:     *TTIC, 6045 S. Kenwood Avenue, 5th Floor, Room 526



*Who:        *Christian Szegedy, Google


*Title:     *    Deep Learning for Formal Reasoning

*Abstract:* In the past few years, deep learning has been instrumental for
breakthrough results in various machine perception and natural language
processing tasks, including computer vision, speech understanding and
synthesis as well as in automated translation. Convolutional neural
networks were the key components for super-human computer go systems. In
this talk, I will present our recent work on proof automation in the
HOL-light higher order interactive theorem prover, where we utilized
current deep learning techniques. Also I will talk about our first attempts
at creating semantically more meaningful text embeddings that seem to be
helpful for reading comprehension from large, unstructured knowledge bases.
Automating mathematics is a tough, long term research goal and here I will
present our two-pronged approach: Strong automated theorem proving lacks
training data, because most of mathematics is present only in informal
natural language literature. Our plan is to attack both automated formal
theorem proving and automated formalization at the same time with the
vision of creating an artificial mathematician that is capable of reading
and arguing about mathematics at a human level, while being able to
communicate in natural language.

Host: David McAllester <mcallester at ttic.edu>

For more information on the colloquium series or to subscribe to the
mailing list, please see http://www.ttic.edu/colloquium.php

Mary C. Marre
Administrative Assistant
*Toyota Technological Institute*
*6045 S. Kenwood Avenue*
*Room 517*
*Chicago, IL  60637*
*p:(773) 834-1757*
*f: (773) 357-6970*
*mmarre at ttic.edu <mmarre at ttic.edu>*


On Sun, Oct 28, 2018 at 5:26 PM Mary Marre <mmarre at ttic.edu> wrote:

> *When:    *  Monday, October 29th at 11:00 am
>
> *Where:     *TTIC, 6045 S. Kenwood Avenue, 5th Floor, Room 526
>
>
>
> *Who:        *Christian Szegedy, Google
>
>
> *Title:     *    Deep Learning for Formal Reasoning
>
> *Abstract:* In the past few years, deep learning has been instrumental
> for breakthrough results in various machine perception and natural language
> processing tasks, including computer vision, speech understanding and
> synthesis as well as in automated translation. Convolutional neural
> networks were the key components for super-human computer go systems. In
> this talk, I will present our recent work on proof automation in the
> HOL-light higher order interactive theorem prover, where we utilized
> current deep learning techniques. Also I will talk about our first attempts
> at creating semantically more meaningful text embeddings that seem to be
> helpful for reading comprehension from large, unstructured knowledge bases.
> Automating mathematics is a tough, long term research goal and here I will
> present our two-pronged approach: Strong automated theorem proving lacks
> training data, because most of mathematics is present only in informal
> natural language literature. Our plan is to attack both automated formal
> theorem proving and automated formalization at the same time with the
> vision of creating an artificial mathematician that is capable of reading
> and arguing about mathematics at a human level, while being able to
> communicate in natural language.
>
> Host: David McAllester <mcallester at ttic.edu>
>
> For more information on the colloquium series or to subscribe to the
> mailing list, please see http://www.ttic.edu/colloquium.php
>
>
>
> Mary C. Marre
> Administrative Assistant
> *Toyota Technological Institute*
> *6045 S. Kenwood Avenue*
> *Room 517*
> *Chicago, IL  60637*
> *p:(773) 834-1757*
> *f: (773) 357-6970*
> *mmarre at ttic.edu <mmarre at ttic.edu>*
>
>
> On Mon, Oct 22, 2018 at 5:20 PM Mary Marre <mmarre at ttic.edu> wrote:
>
>> *When:    *  Monday, October 29th at 11:00 am
>>
>> *Where:     *TTIC, 6045 S. Kenwood Avenue, 5th Floor, Room 526
>>
>>
>>
>> *Who:        *Christian Szegedy, Google
>>
>>
>> *Title:     *    Deep Learning for Formal Reasoning
>>
>> *Abstract:* In the past few years, deep learning has been instrumental
>> for breakthrough results in various machine perception and natural language
>> processing tasks, including computer vision, speech understanding and
>> synthesis as well as in automated translation. Convolutional neural
>> networks were the key components for super-human computer go systems. In
>> this talk, I will present our recent work on proof automation in the
>> HOL-light higher order interactive theorem prover, where we utilized
>> current deep learning techniques. Also I will talk about our first attempts
>> at creating semantically more meaningful text embeddings that seem to be
>> helpful for reading comprehension from large, unstructured knowledge bases.
>> Automating mathematics is a tough, long term research goal and here I will
>> present our two-pronged approach: Strong automated theorem proving lacks
>> training data, because most of mathematics is present only in informal
>> natural language literature. Our plan is to attack both automated formal
>> theorem proving and automated formalization at the same time with the
>> vision of creating an artificial mathematician that is capable of reading
>> and arguing about mathematics at a human level, while being able to
>> communicate in natural language.
>>
>> Host: David McAllester <mcallester at ttic.edu>
>>
>> For more information on the colloquium series or to subscribe to the
>> mailing list, please see http://www.ttic.edu/colloquium.php
>>
>>
>>
>> Mary C. Marre
>> Administrative Assistant
>> *Toyota Technological Institute*
>> *6045 S. Kenwood Avenue*
>> *Room 517*
>> *Chicago, IL  60637*
>> *p:(773) 834-1757*
>> *f: (773) 357-6970*
>> *mmarre at ttic.edu <mmarre at ttic.edu>*
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20181029/a6fd8a2c/attachment-0001.html>