ai.bythebay.io: Francois Chollet, Advances in Deep Learning for Mathematical Theorem Proving
you [Music] hello everyone some France why do depending research on Google and I'll be talking about applying deep yearning to mathematical reasoning so hopefully it will be interesting to at least some of you so I'd like to start with a question which I think the question has been asked around a lot at this conference so at the most important research problem in the eye today so as you know depending is pretty mature technology now we can solve many many problems that seem impossible just 10 years ago it's basically you know come to vision mission perception but at the same time we're still very very far from a human level aii right there are still many more things about intelligence that we do not understand and things that we do in the same so the question is what what's next where is going to be the next big stepping stone wet way I so I'll give you my answer which may not be the right answer or may not be the only answer I think the biggest and sole problem today Nia is abstraction and reasoning so that makes me a big bag so I'm gonna do my best to convey exactly what I mean by that essentially I think today all machine learning algorithms and including deep learning are only just doing pattern matching that's not necessarily a bad thing there's one thing that's wrong with better measuring which is that just like scaling up better measuring by just adding more layers you know building more powerful models and exposing them to more data just by scaling up pattern matching you will not get to true AI you will not get human level intelligence so sometimes this is an arguments being made I just you know by that we're on track to getting to human de valera we just need to keep doing what you're already doing and just you know use bigger GPS and add more layers that's not actually the case so there's one fundamental distinction between pattern matching so our current approach and intelligence and the difference is the power of generalization so pattern matching almost by definition can only generalize there locally that's why it's it's better matching and so that's why's that big state means if you're doing that imagine you are you have some input space X you have some target space Y and you're trying to learn a mapping from X to Y and this is going to require essentially a dance sampling of the X cross Y space so that's why you need to train your deep learning models with lots of training examples with lots of data so on the other hand if you look at humans they can learn new concepts from very few examples we can generalize in a very powerful way from very cool data and that allows people in humans to do things like long term planning and formal reasoning which are very much out of reach for machinery items and the reason why is basically because intelligent beings like humans they work by developing and manipulating abstract models of the situation that they're faced with so that's different from just learning and mapping from X to Y so to kind of try to make things more concrete and give you a better idea of this distinction between para matching and abstract reasoning I will give you a couple examples so first example imagine you're trying to get a rocket to the moon so you're trying to figure out the right design for a rocket and trying to figure out proper launch parameters so you could try to solve this problem with deep learning essentially you would start out by hard coding the problem setting you know the concept of a rocket and you would parameterize this problem you would figure out a set of parameters to optimize and then you would try to learn the relationship between between these input parameters and the outcome of your you know whether or not you get to the moon and this would require essentially to attend sampling of the data manifold that you're trying to learn so whether or not you're approaching the problem with supervisor or you could have seen you know try rent first million in any case even in many many training examples so we need to launch thousands of rockets and do great and ascend until you figure out a design hierarchy that works and and launch by meters at work so that's very much unlike the way a human would approach the problem how you know society is whole so what we would do is actually come up with an abstract formal model of the problem in other laws of physics engineering and so on and then we we use this abstract model to derive an exact solution like exact huge bad news and we will validate our assumptions so very little model using very few trials and so we're able to get a rocket on the moon using very few rapid waves to try so it's much more economical so that's the fundamental distinction between pattern matching where you just have you know some input parameters you want to get to some targets you're just trying lots of things you're trying to learn the relationship between your inputs and your outputs in a very empirical fashion you cannot enter things that you directly experience and the human approach so the more abstract approach where you come up with a model and you use very very few trials to refine your model so that's why essentially abstract reasoning gives you this extreme jurisdiction power compared to pattern matching which can only do local generalization so another example learning to act in a way that the child you you do not get hit by car learn avoidance behaviors when you're not in a risky situation when when you got it when you have a car coming at you so if you have a deep learning model and that could be a supervised model it will be a reinforcement learning model which we need to do is essentially a mapping between your policy space you know the actions you can take and the outcome so dying are not done that will be like your reward function and so that would require you to actually die many many times experience there's many many times in order to to learn kind of the data manifold the relationship between behavior and outcome and humans on the other hand remarkably they typically manage to learn to not get hit by car to avoid cards without having to die you know even once and there are many factors at play but essentially it boils down to the fact that humans make abstract models of the surrounding which allowed them to learn from more than their own experience you don't need to experiment by car to imagine what getting hit by car which feel like would be like they can learn from what other people tell them they can learn just from predicting what will happen you know if you see a car hitting something you can probably predict with what will happen if you waiting you you can learn from reading things and so on so you can learn from many different sorts of information other than direct experience and the reason it's possible is because you're manipulating abstract models instead of just you know learning a direct mapping between what you are feeling what you're seeing and what you're doing that's the difference between better matching and abstract reason so it may seem a bit like I'm bashing I'm shooting and deepening well actually I really don't want to downplay the significance of deep learning I think being good at pattern matching is usually important so deep learning valkira is extremely important because it makes pattern matching much easier like a few years ago if you were to several problems machine learning not only was better matching the only approach you had available you had actually to do half of the work yourself I feel better much of the better matching work you said you had to hand engineer features and deep learning that make actually this panamath approach much easier to deploy because it automates the learning of features but there is a one thing to keep in mind is that just by doing more of what we're currently doing just by scaling up deep learning which is a pattern matching approach you are not going to get to human level intelligence to get to amenable intelligence you need reasoning and obstruction you know the concept is an abstract model that you're manipulating with formal rules and that was actually the very first approach to AI that people had you know many decades ago and currently this is not an approach that's being much investigated by anymore it's really fallen out of favor and I feel like maybe we've we've thrown out the baby with the bathwater when when adoptions burning and and you know suddenly forgetting about the case of that previous research I feel like a symbolic way I might I might actually make a comeback in next few years and one thing you should keep in mind is that if you ever see instances of deep learning models that look like they are doing reasoning that look that they are doing long-term planning like that you play the main playing abstract models and understanding something like understanding language actually they are not is just a bunch of magic tricks what they're actually doing is better matching but because it's it's better measuring train on a very large data sets typically it can somewhat generalize it can locally generalize so things like if you see a deplaning model able of generating captions for a scene for an image for a video it's actually just matching you know parents textures shapes in frames of your video or your image to blobs of English language it's not actually understanding the contents of the scene it's not doing any sort of reasoning or the content is just locally generalizing from data it's been exposed to it's just doing pattern matching and when when you're dealing with modern systems like some question-answering systems digital assistants they seemed like they are really understanding the questions you're asking so actually typically this is solely with hard-coded rules so in this case there is an abstract model but it's actually models being has been provided by human programmers and the anime engines human designers so it doesn't learn you know any form of model for me in creating English language and sometimes these these art credit systems are augmented with deep learning to solve very specific problems like speech recognition for instance ok so deep learning does not actually do reasoning if you see people pretending like it does that typically just leveraging the fact that pattern matching because it can locally generalize can give you the illusion that is doing reasoning it's actually not and the reason you know it's not doing any sort of real reasoning is because this generalization is a local so the systems are going to break down in horrible ways very very easy like captioning systems for instance and on the other hand humans are able to generalize on an extreme levels from just a few data points it can make very long-term very complex predictions so by this point I hope you're convinced that resigning an abstraction of big problems in AI and you're convinced that our current approach machine learning deep learning do not stack all deeply do not attack oil abstraction and reasoning at all so question is how do we move forward how do we tackle reasoning abstraction so we need to find essentially a playground to test new ideas and new approaches and I think a good playground is mathematics so why first because it's a significant problem it's not a toy problem it's not trivial it's also pretty useful and it's useful for beyond just helping mathematicians or automating the job as mathematicians it's useful for more than mathematics in particular if you're able to do formal mathematical reasoning you can probably also do programming so you can start generating correct software and so problems you can also start verifying the correctness of existing software so you can automate the job of software engineers so that's very variable also because it's a purely symbolic problem so there is no perception component so why that's important is because if you're dealing with systems that require reasoning but that also have a perception component a captioning for instance are in a main pivoting language the problem that sometimes you can get better but you're not sure if it's if it's because you're getting better at perception so which is essentially that I'm matching or because you're getting better at reasoning so it's actually much easier to tell if you're doing progress if you just get perception out of the picture entirely and another geared property of mathematics is that it's progressive and by that I mean that you can start out with very simple problems and then you can gradually scale them up get to more more complex problems you know in a very incremental fashion and so that's good for experimentation that's good for learning so just a few words about where we currently stand is regard to artificial reasoning and systems that can do that can process mathematics so we have essentially two branches we have systems that work with humans so ITP is interactive theorem provers and then we have completely automated systems atps which try to automate the job of mathematicians essentially so 90p is typically processing higher-order logic so in in a second I will go over what exactly higher-order logic is and it's used by mathematicians so the mathematician is interacting with the system to prove new serums and in an ATP you're actually feeding into an algorithm a bunch of statements that you know to be true and then you're feeding a conjecture that you want to prove and you leave the algorithm alone trying to figure out a truth in our case we'll be more interested in in atps which primarily work with first-order logic so and ha ha these systems like IQ peas and ATP is a project pardon is essentially just brute force right so in serum proving you're starting from statements that you know are true specifying first order logic or higher their logic and you want to get to a target statement right and the way you do it is by combining existing statements that you know are true and getting out new statements that are also true you know and you do this essentially until you found the statement we're looking for and of course this is combinatorial it's a combinatorial search process essentially and the only way we have to solve it is very done which is do brute force search and here's here's one way I think we can attack all mathematical reasoning and this can actually be used as a template as a blueprint to generally you know solve reasoning so the abstract modeling at least at least in the short term it's to take an existing formal reasoning system so something that does explicit search does formal reasoning and to augment it with an intuition module and this intuition module would be implemented using pattern matching for using essentially machine learning and deep learning so essentially you take a symbolic AI but then you mix it up with machine learning and deep learning to essentially give the system some intuition about the meaning of the symbols that it's manipulating right and this meaning come will come from other matching century you know analogies things like that so augmenting symbolic AI with an intuition module provided by depending and so I will present a project that we did it at Google with colleagues so in particular Christians agree draw free anything Alex Ali me sir hollows and Nicholas and and also Youssef el band with not a Googler it's from the Czech Technical Institute in in Prague is one of the experts on on atps so it's a big mass project which is essentially about taking this approach so demanding a formal reasoning system with an intuition module provided by deep learning and use it to prove theorems so to augment an existing ATP with deep learning so we call it dicknuts so as you know if you're doing deep learning you can name your projects as either and you know deep something or something that so we are in stating that Natan did not went with deep math like you know you know wavenet deep wave deep voice voice net whatever okay and so to add either power and first of all we need a data set and we'll benchmark to tell that we are making progress to tell that we're beating some state of the art and so we picked the misura mathematical library so this means our library is a set of statements written in first order logic so we'll see in a bit with fuzzy logic is we have 58 thousand statements they are written by humans but they are also formally verified so formal verification if you come from a programming background it's it's like a very strong form of unit testing it's just to where to guarantee that the statements are true and it's commonly used as a benchmark for automated theorem provers for ATP's and so among these 58,000 serums you have many well-known serums including cauchy-riemann include the Jordan theorem and many others less well known so just a few words about what first-order logic and the higher the logic look like so visually that's what they look like yeah you got first a logic high order logic so the way to think about it is basically with a programming analogy if you can think of first order logic as like the assembly of formal reasoning whereas high order logic is more like a fully fledged programming language a functional programming language with pure functions and types so it's it's higher level it's more flexible more powerful more expressive it's also more difficult to manipulate and so did mass projects essentially consisted in taking an ATP so in our case it was an atypical called improver and to help it in its route for search process using deep learning and essentially the process of following so if you have a statement you want to prove the conjecture you want to prove first you start with a fairly large set of statements that you know are true the first thing you need to do is selecting among the statement that you know are true the statements are going to be useful in your proof and you use these statements as a starting point in the brute-force search process so this is called premise selection so premise is what you start from it's your you know logical starting point and currently the state-of-the-art is to use a very basic form of machine learning on top of handcrafted heuristics to do this premise selection to select the starting point to give to to approval and security this is done with zucchinis neighbors on top of handcrafted mystics and the assumption that we can do better using deep learning and by also completely removing and craft and crafted features so you can think of the task of premise selection as essentially the very first step that a mathematics term would would go through and trying to prove a theorem is it's like selecting limits or selecting axioms that are going to be important in proving this theorem and so when the mathematician does it is not actually formally inferring anything it's naturally you know applying formal logic it's just using its own intuition or her own intuition to select the right premises so the way we solve the problem of primate selection with busy planning essentially with this network architecture well where we have two branches so one branch will be used to turn conjecture so the theorem you're trying to prove into a dense embedding so into a vector and the other branch does the same thing with a candidate premise and then you can combine both embeddings and train a classifier to output like a score of whether or not the premise is useful to prove the conjecture and you can render to network on all available premises and and then you attack you know the first top ten master event premises the point where master and premises and so on and you feed that into your ATP as the starting point to try to prove a theorem and you see if it managed it manages to get somewhere so this work was presented in in a newspaper deep not deep sequence model supremacy selection so work done with many colleagues colleagues at Google including also one non-googlers as a turbine so we tried many many different variants of this set up we try different networks for embedding the statements we tried different ways of fitting the statements into the system and different classifiers as well and essentially what we found out was that tricular networks do not perform very well 1d cabinets are from best we used to try different things for fitting the data into networks so you can either take a very naive approach and look at first-order logic statements and fit them into a network as a sequence of characters you can also try to tokenize them into tokens that make sense and try to do one heart including other tokens for instance feed that into a network but this approach is actually they vary in age and they did not work very well compared to our baseline because our baseline used handcrafted features that were pretty advanced and here we're just starting from characters of tokens we're not going very far so one thing we found that was pretty clever and that work really well was to essentially embed tokens into some embedding space and we come to this embedding space by first training a model so this type of model is essentially on on statements and could the sequences of characters right and then when you have a token you feed it into the embed our network so train on using using this architecture and and you essentially converts your sequence of tokens into a sequence of embedding vectors each embedding vector coming from the first-order logic statement that defines the token that you're dealing with because when you're dealing with Fasulo logic every token you manipulating has itself a first-order logic definition so it's a way to leverage the regressivity of the solar logic a century to an award it's a little bit with innovating space so it turns out this approach works well so this is like a summary of our results we have character level approaches token level approaches or world level approaches and then this definition embedding setup and then we have different network architectures so cnn's in see I'm an SEM essentially types of networks that we use to encode to embed the statements so as you can see just using a character level CNN or our CNN lsdm was actually even worse just guy Tyler Wilson does not outperform the Kenan baseline on top of pretty advanced and crafted features but if you use definition embeddings then we start significantly outperforming to baseline so this beats the state-of-the-art we can prove more theorems that could be proven entirely automatically before in particular we can provide automated proofs for serums that we are never proved by an ATP before we already add proofs of these theorems with the way human generated proofs so one thing you can do to go even further is a closed selection so as as I was explaining when you're trying to prove a theorem you're starting from a set of segments that are known to be true and you are combining them together right and when you're combining statements together you're creating new statements and then you're adding them to like a bucket of closes so close it's just a statement and at the next step what you're going to do is essentially select one of your dissing clauses which are statement that are known to be true and that are known to be basically that can be inferred from your initial axioms and you are going to combine it combine 1 Clause with other existing closets to generate new clauses right and the problem of closed selection is knowing which clauses should be selected right so it's very similar to premise selection the difference is that in premise selection you are selecting a starting point with closed selection you are trying to rank your unprocess closes at every inference step so it's it's much it's it's like a continuous process instead of just meeting the providing the ATP with the starting point you are continuously guide units so this is work that was presented in and an airport paper deep network ID proof search it sanaka I can check it out and to do that with deep learning again we use very similar architecture as we did with the initial thickness paper so we have a true branch and building network that ends with a classifier and so my colleagues tried many different architectures including the activities that worked well for a premise selection and it turned out the best performing architectures we are also similar to word quick deaths for premise selection it's 1d cabinets turns out also that using dieted care notes in your 1d ComNet works better so which is which we call wave nets in a wave net with deepmind paper about a generative model for voice and sound so it was just essentially a onesie ComNet with dilated channels so there's just one problem with this setup which is speed if you're using this network to evaluate a clothes it's roughly 1,000 times slower so it takes 1,000 times more time then combining the clothes you're trying to evaluate with all available process right so it's it's dramatically slower than brute force so the way to think about it is that this deep learning model provides you with much higher quality search process like a much wiser search process you are selecting your closest in a very smart way but at the same time you are moving very very slowly right and the way to to deal with it is essentially with which we came up with the two-phase process so first we leverage both our deep networks and existing heuristics to get a pretty smart search process and when we get closer to a solution so we are more advanced in the improve process we actually drop the really slow network evaluation and we just keep the us sticks so essentially we have a trade-off between speed and search quality and when you are early in the search process it's better to privilege search quality because essentially yours your your search space is community older so it's it's a good idea to make smart choice in the beginning and when you get closer to the end then brute force is an increasingly valid approach and so that's why you can actually drop this this higher search quality module this intuition module so this is where the results here we are comparing management architectures so surprisingly tree networks 3r SEM did not work very well the networks that work best were actually the one he ComNet so just like a premise selection just like the math one and one way to get even better results was actually to use larger convolution windows we studied can also the so called weight net and the good thing is that these two approaches did not one so using deep learning to sort premise selection and read math to using deep learning to soar close selection there are complementary approaches so you can actually run them together you can select both the starting-point feel for your ATP and then you can guide the ATP during the proof search process which is a two-phase hybrid approach where you start by essentially guiding at the network guiding the the ATP 50 percent of time and when you get closer to the solution use dangerous rely on brute force so by leveraging both approaches the same time we end up proving many more theorems so in bangla when the proving many theorems that before did not have any ATP generated proof and only had a human journey pose so this is still a very very basic very premium very preliminary approach this is essentially just taking a listing deep learning sequence processing models applying them to trust our logic statement sequence data getting scores out of them this is otherwise smart so I think if we want to carry on in this direction we need to move to higher order logic so again the programming analogy between first order logic and higher order logic that first ala logic is closer to like the assembly of formal reasoning and higher the logic is market programming language so in order to try to speed things up try to catalyze research around using machine learning for high order logic so improving we released data sets called whole step so hold for higher the logic so that wasn't an eye clear paper holds that machine in this set for biologics are improving we can check it out on our card you can also download the data so it's a data set of triplets our fire the logic statements so in one triplets you have essentially one conjecture so something that you're trying to prove you have one statement that is a proof step that turned out to be useful it turned out to be included in the final proof to prove the conjecture and you have one negative example which is essentially a harder logic statement that was generated during the proof search but that turned out to not be useful to not be included in final proof so of course if you can tell the difference between a useful statement with regard to conjecture and a non useful statement and you can be very very good at at cross selection and you can also be very good at that premise selection obviously because it's a very similar problem to cross selection and you can do even even more you can also try to reverse a problem like even some proof steps what should be the conjecture so you do things like here conjecturing and you can also try to not just try to rank existing statements but try to generate statements try to predict where the next Pro step should be so many many tasks that you can try it's it's very amenable to machine learning so you can search for it download it publish papers about it alright so to wrap up my talk which you should take away is that one big and sort problem in AI today is abstraction and reasoning and our current approach with deep learning machining is regis doing pattern matching so it's not attacking abstraction or easing at all but attacking these problems is going to be usually important on the way to AI and we think that mathematics is a great playground to try new approaches to tackle obstruction reasoning and there is nowhere to do well with essentially just pattern matching when you are when you are thinking and I'm Alex and we are proposing like a template for in general leveraging abstraction and reasoning in in mathematical problems which is to take an existing formal reasoning system and existing proof search system and to augment it with an intuition module provided by deep learning so provided by pattern matching so essentially you take symbolic AI but you give the symbolic AI system some intuition with regard to the meaning of the symbols it's my EP rating and so this intuition and meaning it's all it's all better matching so read the combination of abstract models with intuition and of course that's a very very permanent preliminary step in the future you can imagine that AI will will be able to come up with its own formal reasoning systems with its own search strategies with his own abstract models but for now we just take hard-coded abstract models of mundane with intuition and so our deep mass project was pretty successful we managed to prove a significant number of new serums so not serums that we're not proven before but terms that we are not proven automatically before but we're only proved environments and the next step is to go from just processing facility to processing higher logic this also has implications for artificial programming if you're good at passing high order logic you also going to be good at generating programs for instance and you can actually take part in this research because we made available this higher higher order logic proofs that data set whole step which you can download so that's it for me and I'll be taking a few questions [Applause] I first of all thank you very much for the talk it's incredibly interesting to give you a bit of background I work in automatic programming with deep learning and I was particularly interested to see the results on first order logic wavenet versus tree based LS teams because particularly as you start moving to more higher-order logic and taking back the analogy to source code where at the end you can bring everything back to abstract syntax trees why do you think wavenet outperforms versus tree based l STM's and you think it will continue to do so as you move more towards higher-order logic so I think so the statements were manipulating are fundamentally recursive and leveraging this recursive structure seems hugely important but in practice we found so far that's trying to leverage it has not worked it does not mean it's not important it's just we have not currently managed to make it work I do believe that we should keep investigating tree tree shaped networks I do believe we need to take into account recursively so currently I think the reason is just that as a patch image as a better matching system for long sequences wavenet just works better but it's it seems to be more like a technical issue intuitively like conceptually it's very clear that the leveraging like Yosemite is a right way to approach this do one more question I have a question right here do you have any plans for participating in any theorem prover Corporation's sorry what do you have any plans for participating in one of the theorem prover competitions theorem blowing competitions oh yeah possibly yes it's not it's not a priority our priority is just to explore this space come up with interesting approaches the thing is sir improving competitions or not it's it's very niche right so it's not going to be interesting to a lot of people and people that will be interested in it are not actually people who would say share our vision of trying to leverage gee planning for improving [Applause]