#50 Dr. CHRISTIAN SZEGEDY - Formal Reasoning, Program Synthesis

Описание: Dr. Christian Szegedy from Google Research is a deep learning heavyweight. He invented adversarial examples, one of the first object detection algorithms, the inceptionnet architecture, and co-invented batchnorm. He thinks that if you bet on computers and software in 1990 you would have been as right as if you bet on AI now. But he thinks that we have been programming computers the same way since the 1950s and there has been a huge stagnation ever since. Mathematics is the process of taking a fuzzy thought and formalising it. But could we automate that? Could we create a system which will act like a super human mathematician but you can talk to it in natural language? This is what Christian calls autoformalisation. Christian thinks that automating many of the things we do in mathematics is the first step towards software synthesis and building human-level AGI. Mathematics ability is the litmus test for general reasoning ability. Christian has a fascinating take on transformers too.


With Yannic Lightspeed Kilcher and Dr. Mathew Salvaris


Whimsical Canvas with Tim's Notes:
https://whimsical.com/mar-26th-christ...

Pod version: https://anchor.fm/machinelearningstre...

Tim Introducton [00:00:00]
Show Kick-off [00:09:12]
Why did Christian pivot from vision to reasoning? [00:12:07]
Autoformalisation [00:12:47]
Kepler conjecture [00:17:30]
What are the biggest hurdles you have overcome? [00:20:11]
How does something as fuzzy as DL come into mathematical formalism? [00:23:05]
How does AGI connect to autoformalisation? [00:30:32]
Multiagent systems used in autoformalisation? Create an artificial scientific community of AI agents! [00:36:42]
Walid Saba -- the information is not in the data [00:41:58]
Is generalization possible with DL? What would Francois say? [00:45:02]
What is going on in a neural network? (Don't Miss!) [00:47:59]
Inception network [00:52:42]
Transformers negate the need for architecture search? [00:55:58]
What do you do when you get stuck in your research? [00:58:08]
Why do you think SGD is not the path forward? [00:59:59]
Is GPT-3 on the way to AGI [01:02:01]
Is GPT-3 a hashtable or a learnable program canvas? [01:05:01]
What worries Christian about the research landscape? [01:07:14]
The style that research is conducted [01:11:10]
Layerwise self supervised training [01:13:59]
Community Questions: The problem of reality in AI ethics [01:15:33]
Community Questions: Internal covariate shift and BatchNorm [01:20:03]
Community Questions: What is so special about attention? [01:23:08]
Jürgen Schmidhuber [01:24:18]
Community Question: Data efficiency and is it possible to "learn" inductive biases? [01:27:13]
Francois's ARC challenge, is inductive learning still relevant? [01:31:13]


A Promising Path Towards Autoformalization and General Artificial Intelligence [Szegedy]
https://link.springer.com/chapter/10....


Learning to Reason in Large Theories without Imitation [Bansal/Szegedy]
https://arxiv.org/pdf/1905.10501.pdf


MATHEMATICAL REASONING VIA SELF-SUPERVISED SKIP-TREE TRAINING [Rabe .. Szegedy]
https://openreview.net/pdf?id=YmqAnY0...


LIME: LEARNING INDUCTIVE BIAS FOR PRIMITIVES OF MATHEMATICAL REASONING [Wu..Szegedy]
https://arxiv.org/abs/2101.06223v1


DEEP LEARNING FOR SYMBOLIC MATHEMATICS [Lample]
https://arxiv.org/pdf/1912.01412.pdf


It’s Not What Machines Can Learn, It’s What We Cannot Teach [Yehuda]
https://arxiv.org/pdf/2002.09398.pdf


Investigating the Limitations of Transformers with Simple Arithmetic Tasks [Nogueira]
https://arxiv.org/pdf/2102.13019.pdf


Provable Bounds for Learning Some Deep Representations [Arora]
https://arxiv.org/pdf/1310.6343.pdf


Neural nets learn to program neural nets with fast weights [Schmidhuber]
https://people.idsia.ch/~juergen/fast...


How does Batch Normalization Help Optimization? [Ilyas]
https://gradientscience.org/batchnorm/


How to Train Your ResNet 7: Batch Norm
https://myrtle.ai/learn/how-to-train-...


Training a ResNet to 94% Accuracy on CIFAR-10 in 26 Seconds on a Single GPU – [KUHN]
https://efficientdl.com/how-to-train-...


https://en.wikipedia.org/wiki/HOL_Light
https://en.wikipedia.org/wiki/Coq
https://en.wikipedia.org/wiki/Kepler_...
https://en.wikipedia.org/wiki/Feit%E2...


We used a few clips from the ScaleAI interview with Christian -    • Interview with Christian Szegedy