Re: A NN Solves and Generates Math Problems
Tim Daly <[email protected]> Mon, 10 Jan 2022 07:28:24 -0500
| Newsgroups | gmane.comp.mathematics.axiom.devel |
|---|---|
| Message-ID | <CAJn5L=Lo_O5SOJxGpJwWeeVemQZ17h3Zz305UXTt=f7ECgVq4w@mail.gmail.com> |
--000000000000c3745f05d5397925 Content-Type: text/plain; charset="UTF-8" Suppose the goal was to generate code from proofs. Suppose that certain tactics have "code-like" equivalents. Can we define such a restricted set of tactics? This would eliminate Coq's hammer tactic, for example. The definition of an axiom could include the text for the equivalent program, making them "effective theorems", or "fully constructive theorems". Given a proof of a theorem from this restricted set it should be (somewhat) easier to create equivalent programs. This amounts to "proving the theorem" by "writing the program", albeit in a tactic language. For example, a "reduce" tactic would apply a function to a set of numbers (symbolically), with the proof condition that the set is finite and the generated index decreases so we can know that "reduce" terminates. That would then be equivalent to the Lisp map operation. Tim On Sun, Jan 9, 2022 at 4:56 PM Tim Daly <[email protected]> wrote: > In general, I'm pretty skeptical of Neural Net generation of math, > but I'm following the literature quite closely. > > I recently spent time with an effort that tried to do integration. > It was interesting because they could "round trip" the solution by > differentiating the result. I worked with the authors, added some > of their results to Axiom, and suggested possible further work. But > the approach, while it looks impressive, has quite a few flaws. > > I have yet to "deep dive" into this paper. It is really interesting to > me that it claims to generate code. I would like to see a "round > trip" where some LEAN math was used to generate code and > then the code was proven using LEAN. Especially interesting > would be the question of how the definitions and axioms of the > original LEAN proof were used, if at all, in the proof of the code. > (Of course, LEAN doesn't seem to focus on proving code.) > > From an Axiom point of view, "proven code generation" from a > proven theorem is my holy grail. If there was a way to form a > one-to-one, onto mapping between theorems and code I'd be > rewriting all of Axiom using it. I doubt that a Neural Net can > achieve such a mapping. > > Given that Axiom is using first-class dependent types I'm not > at all clear how that could be possible using a Neural Net. > Can a Neural Net even infer the correct Types? I suppose, > for the simple case such as NAT, it could "learn" from the > definitions but cubical types might be a tad bit harder. > > Nor is it clear to me how you would generate code that was > sound but not complete. > > I just looked up Bartosz's body of work. It looks really interesting, > giving me much more to read. > > Tim > > > > On Sun, Jan 9, 2022 at 1:22 PM Jeremy Avigad <[email protected]> wrote: > >> Thanks for this! It seems to speak to the success of the OpenAI Codex >> more than anything else, but the results are impressive. >> >> Bartosz Piotrowski, a PhD student and author of one of the papers you >> cited, will be visiting Carnegie Mellon for a few months this spring. >> >> Best wishes, >> >> Jeremy >> >> On Thu, Jan 6, 2022 at 10:30 AM Tim Daly <[email protected]> wrote: >> >>> This is an interesting paper (especially given that it >>> is work under Gilbert Strang): >>> >>> A Neural Network Solves and Generates Mathematics >>> Problems by Progam Synthesis: Calculus, Differential >>> Equations, Linear Algebra, and More. >>> https://arxiv.org/pdf/2112.15594.pdf >>> >>> "This work shows that a neural network that generates >>> programs (i.e. program synthesis) is the key to solving >>> math and STEM courses at scale, as it turns question >>> answering into a programming task." >>> >>> This seems interesting from several aspects: >>> >>> 1) Can this be applied to logic systems? Can it help >>> generate "proven code" from a proof system? (LEAN) >>> >>> 2) Can it be applied in programs like NuPRL / RedPRL? >>> (Innovations in Computational Type Theory using Nuprl >>> Journal of Applied Logic 4 (2006) pp 428--469 >>> >>> https://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=C11F82ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0AC6724F&originRegion=us-east-1&originCreation=20220106150458 >>> >>> 3) Can the type of an object be inferred by casting it as a >>> question in mathematics? Is the generated program correctly >>> typed? >>> >>> 4) Can this be layered on MetaMath (LEAN) or FDL (Nuprl) >>> to generate logically equivalent code? >>> >>> 5) Can this be applied to gradual typing? >>> >>> In any case, this represents an interesting "interdisciplinary" >>> effort connecting the math department and CS. >>> >>> Tim >>> >>> >>> >>> There are various connections to Neural Networks and Math: >>> >>> @misc{Crou19, >>> author = "Crouse, Maxwell and Whitehead, Spencer and >>> Abdelaziz, Ibrahim and Makni, Bassem and >>> Cornelio, Cristina and Kapanipathi, Pavan and >>> Pell, Edwin and Srinivas, Kavitha and >>> Thost, Veronika and Witbrock, Michael and >>> Fokoue, Achille", >>> title = {{A Deep Reinforcement Learning Base Approach to Learning >>> Transferable Proof Guidance Strategies}}, >>> year = "2019", >>> linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}", >>> abstract = >>> "Traditional first-order logic (FOL) reasoning systems usually >>> rely on manual heuristics for proof guidance. We propose TRAIL: a >>> system that learns to perform proof guidance using reinforcement >>> learning. A key design principle of our system is that it is >>> general enough to allow transfer to problems in different domains >>> that do not share the same vocabulary of the training set. To do >>> so, we developed a novel representation of the internal state of a >>> prover in terms of clauses and inference actions, and a novel >>> neural-based attention mechanism to learn interactions between >>> clauses. We demonstrate that this approach enables the system to >>> generalize from training to test data across domains with >>> different vocabularies, suggesting that the nerual architecture in >>> TRAIL is well suited for representing and processing of logical >>> formalisms.", >>> paper = "Crou19.pdf" >>> } >>> >>> @misc{Crou19a, >>> author = "Crouse, Maxwell and Abdelaziz, Ibrahim and >>> Cornelio, Cristina and Thost, Veronika and >>> Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille", >>> title = {{Improving Graph Neural Network Representations of Logical >>> Formulae with Subgraph Pooling}}, >>> year = "2019", >>> linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}", >>> abstract = >>> "Recent advances in the integration of deep learning with >>> automated theorem proving have centered around the representation >>> of graph-structured representations, in large part driven by the >>> rapidly emerging body of research in geometric deep >>> learning. Typically, structure-aware neural methods for embedding >>> logical formulae have been variants of either Tree LSTMs or >>> GNNs. While more effective than character and token-level >>> approaches, such methods have often made representational >>> trade-offs that limited their ability to effectively represent the >>> global structure of their inputs. In this work, we introduce a >>> novel approach for embedding logical formulae using DAG LSTMs that >>> is designed to overome the limitations of both Tree LSTMs and >>> GNNs. The effectiveness of the proposed framework is demonstrated >>> on the tasks of premise selection and proof step classification >>> where it achieves the state-of-the-art performance on two standard >>> datasets.", >>> paper = "Crou19a.pdf" >>> } >>> >>> @misc{Gaut19, >>> author = "Gauthier, Thibault", >>> title = {{Deep Reinforcement Learning in HOL4}}, >>> year = "2019", >>> link = "\url{https://arxiv.org/pdf/1910.11797.pdf}", >>> abstract = >>> "The paper describes an implementation of deep reinforcement >>> learning through self-supervised learning within the proof >>> assistant HOL4. A close interaction between the machine learning >>> modules and the HOL4 library is achieved by the choice of tree >>> neural networks (TNNs) as machine learning models and the internal >>> use of HOL4 terms to represent tree structures of TNNs. Recursive >>> improvement is possible when a given task is expressed as a search >>> problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm >>> guided by a TNN can be used to explore the search space and >>> produce better examples for training the next TNN. As an >>> illustration, tasks over propositional and arithmetical terms, >>> representative of fundamental theorem proving techniques, are >>> specified and learned: truth estimation, end-to-end computation, >>> term rewriting and term synthesis.", >>> paper = "Gaut19.pdf" >>> } >>> >>> @misc{Lamp19, >>> author = "Lample, Guillaume and Charton, Francois", >>> title = {{Deep Learning for Symbolic Mathematics}}, >>> year = "2019", >>> link = "\url{https://arxiv.org/pdf/1912.01412.pdf}", >>> link = "\url{https://www.youtube.com/watch?v=O_sHHG5_lr8}", >>> abstract = >>> "Neural networks have a reputation for being better at solving >>> statistical or approximate problems than at performing >>> calculations or working with symbolic data. In this paper, we show >>> that they can be surprisingly good at more elaborated tasks in >>> mathematics, such as symbolic integration and solving differential >>> equations. We propose a syntax for representing mathematical >>> problems, and methods for generating large datasets that can be >>> used to train sequence-to-sequence models. We achieve results that >>> outperform commercial Computer Algebra Systems such as Matlab or >>> Mathematica.", >>> paper = "Lamp19.pdf", >>> keywords = "printed, DONE" >>> } >>> >>> @misc{Olsa19, >>> author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef", >>> title = {{Property Invariant Embedding for Automated Reasoning}}, >>> year = "2019", >>> link = "\url{https://arxiv.org/pdf/1911.12073.pdf}", >>> abstract = >>> "Automated reasoning and theorem proving have recently become >>> major challenges for machine learning. In other domains, >>> representations that are able to abstract over unimportant >>> transformations, such as abstraction over translations and >>> rotations in vision, are becoming more common. Standard methods of >>> embedding mathematical formulas for learning theorem proving are >>> however yet unable to handle many important transformations. In >>> particular, embedding previously unseen labels, that often arise >>> in definitional encodings and in Skolemizatin, has been very weak >>> so far. Similar problems appear when tranferring knowledge between >>> known symbols. >>> >>> We propose a novel encoding of formulas that extends existing >>> graph neural network models. This encoding represents symbols only >>> by nodes in the graph, without giving the network any knowledge of >>> the original labels. We provide additional links between such >>> nodes that allow the network to recover the meaning and therefore >>> correctly embed such nodes irrespective of the given labels. We >>> test the proposed encoding in an automated theorem prover based on >>> the tableaux connection calculus, and show that it improves on the >>> best characterizations used so far. The encoding is further >>> evaluated on the premise selection task and a newly introduced >>> symbol guessing task, and shown to correctly predict 65\% of the >>> symbol names.", >>> paper = "Olsa19.pdf" >>> } >>> >>> @misc{Piot19, >>> author = "Piotrowski, Bartosz and Brown, Chad E. and >>> Kaliszyk, Cezary", >>> title = {{Can Neural Networks Learn Symbolic Rewriting?}}, >>> year = "2019", >>> link = "\url{https://arxiv.org/pdf/1911.04783.pdf}", >>> abstract = >>> "This work investigates if the current neural architectures are >>> adequate for learning symbolic rewriting. Two kinds of data sets >>> are proposed for this research -- one based on automated proofs >>> and the other being a synthetic set of polynomial terms. The >>> experiments with use of the current neural machine translation >>> models are performed and its results are discussed. Ideas for >>> extending this line of research are proposed and its relevance is >>> motivated.", >>> paper = "Piot19.pdf" >>> } >>> >>> @misc{Sanc19, >>> author = "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence >>> and Lerner, Sorin", >>> title = {{Generating Correctness Proofs with Neural Networks}}, >>> year = "2019", >>> link = "\url{https://arxiv.org/pdf/1907.07794.pdf}", >>> abstract = >>> "Foundational verification allows programmers to build software >>> which has been empirically shown to have high levels of assurance >>> in a variety of important domains. However, the cost of producing >>> foundationally verified software remains prohibitively high for >>> most projects, as it requires significant manual effort by highly >>> trained experts. In this paper we present Proverbot9001 a proof >>> search system using machine learning techniques to produce proofs >>> of software correctness in interactive theorem provers. We >>> deomonstrate Proverbot9001 on the proof obligations from a large >>> practical proof project, the CompCert verified C compiler, and >>> show that it can effectively automate what was previously manual >>> proofs, automatically solving 15.77\% of proofs in our test >>> dataset. This corresponds to an over 3X improvement over the prior >>> state of the art machine learning technique for generating proofs >>> in Coq.", >>> paper = "Sanc19.pdf" >>> } >>> >>> @misc{Wang19a, >>> author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and >>> Urban, Josef", >>> title = {{Exploration of Neural Machine Translation in >>> Autoformalization of Mathematics in Mizar}}, >>> year = "2019", >>> link = "\url{https://arxiv.org/pdf/1912.02636.pdf}", >>> abstract = >>> "In this paper we share several experiments trying to >>> automatically translate informal mathematics into formal >>> mathematics. In our context informal mathematics refers to >>> human-written mathematical sentences in the LaTeX format; and >>> formal mathematics refers to statements in the Mizar language. We >>> conducted our experiments against three established neural >>> network-based machine translation models that are know to deliver >>> competitive results on translating between natural languages. To >>> train these models we also prepared four informal-to-formal >>> datasets. We compare and analyze our results according to whether >>> the model is supervised or unsupervised. In order to augment the >>> data available for auto-formalization and improve the results, we >>> develop a custom type-elaboration mechanism and integrate it into >>> the supervised translation.", >>> paper = "Wang19a.pdf" >>> } >>> >>> >>> >>> >>> >>> --000000000000c3745f05d5397925 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div>Suppose the goal was to generate code from proofs.</d= iv><div>Suppose that certain tactics have "code-like" equivalents= .</div><div>Can we define such a restricted set of tactics?</div><div>This = would eliminate Coq's hammer tactic, for example.</div><div><br></div><= div>The definition of an axiom could include the text for the</div><div>equ= ivalent program, making them "effective theorems",</div><div>or &= quot;fully constructive theorems".<br></div><div><br></div><div>Given = a proof of a theorem from this restricted set <br></div><div>it should be (= somewhat) easier to create equivalent programs.</div><div><br></div><div>Th= is amounts to "proving the theorem" by "writing the program&= quot;,</div><div>albeit in a tactic language.</div><div><br></div><div>For = example, a "reduce" tactic would apply a function to a</div><div>= set of numbers (symbolically), with the proof condition that</div><div>the = set is finite and the generated index decreases so we</div><div>can know th= at "reduce" terminates. That would then be</div><div>equivalent t= o the Lisp map operation.</div><div><br></div><div>Tim</div><div><br></div>= <div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class= =3D"gmail_attr">On Sun, Jan 9, 2022 at 4:56 PM Tim Daly <<a href=3D"mail= to:[email protected]">[email protected]</a>> wrote:<br></div><blockquo= te class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px = solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>In general, = I'm pretty skeptical of Neural Net generation of math,</div><div>but I&= #39;m following the literature quite closely.<br></div><div><br></div><div>= I recently spent time with an effort that tried to do integration.</div><di= v>It was interesting because they could "round trip" the solution= by</div><div>differentiating the result. I worked with the authors, added = some <br></div><div>of their results to Axiom, and suggested possible furth= er work. But <br></div><div>the approach, while it looks impressive, has qu= ite a few flaws.</div><div><br></div><div>I have yet to "deep dive&quo= t; into this paper. It is really interesting to</div><div>me that it claims= to generate code. I would like to see a "round</div><div>trip" w= here some LEAN math was used to generate code and</div><div>then the code w= as proven using LEAN. Especially interesting</div><div>would be the questio= n of how the definitions and axioms of the</div><div>original LEAN proof we= re used, if at all, in the proof of the code.</div><div>(Of course, LEAN do= esn't seem to focus on proving code.)<br></div><div><br></div><div>From= an Axiom point of view, "proven code generation" from a</div><di= v>proven theorem is my holy grail. If there was a way to form a</div><div>o= ne-to-one, onto mapping between theorems and code I'd be</div><div>rewr= iting all of Axiom using it. I doubt that a Neural Net can</div><div>achiev= e such a mapping.</div><div><br></div><div>Given that Axiom is using first-= class dependent types I'm not</div><div>at all clear how that could be = possible using a Neural Net.</div><div>Can a Neural Net even infer the corr= ect Types? I suppose,</div><div>for the simple case such as NAT, it could &= quot;learn" from the</div><div>definitions but cubical types might be = a tad bit harder.<br></div><div><br></div><div>Nor is it clear to me how yo= u would generate code that was</div><div>sound but not complete.</div><div>= <br></div><div>I just looked up Bartosz's body of work. It looks really= interesting,</div><div>giving me much more to read.</div><div><br></div><d= iv>Tim</div><div><br></div><div><br></div></div><br><div class=3D"gmail_quo= te"><div dir=3D"ltr" class=3D"gmail_attr">On Sun, Jan 9, 2022 at 1:22 PM Je= remy Avigad <<a href=3D"mailto:[email protected]" target=3D"_blank">avigad@= cmu.edu</a>> wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"= margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-lef= t:1ex"><div dir=3D"ltr">Thanks for this! It seems to speak to the success o= f the OpenAI Codex more than anything else, but the results are impressive.= <div><br></div><div>Bartosz Piotrowski, a PhD student and author of one of = the papers you cited, will be visiting Carnegie Mellon for a few months thi= s spring.</div><div><br></div><div>Best wishes,</div><div><br></div><div>Je= remy</div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gm= ail_attr">On Thu, Jan 6, 2022 at 10:30 AM Tim Daly <<a href=3D"mailto:ax= [email protected]" target=3D"_blank">[email protected]</a>> wrote:<br></= div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;bor= der-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div= >This is an interesting paper (especially given that it</div><div>is work u= nder Gilbert Strang):</div><div><br></div><div><div>A Neural Network Solves= and Generates Mathematics</div><div>Problems by Progam Synthesis: Calculus= , Differential</div><div>Equations, Linear Algebra, and More.</div><div><a = href=3D"https://arxiv.org/pdf/2112.15594.pdf" target=3D"_blank">https://arx= iv.org/pdf/2112.15594.pdf</a></div><div><br></div><div>"This work show= s that a neural network that generates</div><div>programs (i.e. program syn= thesis) is the key to solving</div><div>math and STEM courses at scale, as = it turns question</div><div>answering into a programming task."</div><= div><br></div><div>This seems interesting from several aspects:</div><div><= br></div><div>1) Can this be applied to logic systems? Can it help <br></di= v><div>generate "proven code" from a proof system? (LEAN)</div><d= iv><br></div><div>2) Can it be applied in programs like NuPRL / RedPRL?</di= v><div>(Innovations in Computational Type Theory using Nuprl</div><div>Jour= nal of Applied Logic 4 (2006) pp 428--469<br></div><div><a href=3D"https://= reader.elsevier.com/reader/sd/pii/S1570868305000704?token=3DC11F82ADA943900= 97338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0A= C6724F&originRegion=3Dus-east-1&originCreation=3D20220106150458" ta= rget=3D"_blank">https://reader.elsevier.com/reader/sd/pii/S1570868305000704= ?token=3DC11F82ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF102517732= 3CCD7B46510F77FFC4955D0AC6724F&originRegion=3Dus-east-1&originCreat= ion=3D20220106150458</a></div><div><br></div><div>3) Can the type of an obj= ect be inferred by casting it as a</div><div>question in mathematics? Is th= e generated program correctly</div><div>typed?</div><div><br></div><div>4) = Can this be layered on MetaMath (LEAN) or FDL (Nuprl)</div><div>to generate= logically equivalent code?</div><div><br></div><div>5) Can this be applied= to gradual typing?<br></div><div><br></div><div>In any case, this represen= ts an interesting "interdisciplinary"</div><div>effort connecting= the math department and CS.</div><div><br></div><div>Tim</div><div><br></d= iv><div><br></div><div><br></div><div>There are various connections to Neur= al Networks and Math:</div><div><br></div><div>@misc{Crou19,<br>=C2=A0 auth= or =3D "Crouse, Maxwell and Whitehead, Spencer and <br>=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 Abdelaziz, Ibrahim and Makni, Bassem and <br>= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Kapanipath= i, Pavan and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pell, Edwin and S= rinivas, Kavitha and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Ve= ronika and Witbrock, Michael and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 Fokoue, Achille",<br>=C2=A0 title =3D {{A Deep Reinforcement Learn= ing Base Approach to Learning<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0T= ransferable Proof Guidance Strategies}},<br>=C2=A0 year =3D "2019"= ;,<br>=C2=A0 linke =3D "\url{<a href=3D"https://arxiv.org/pdf/1911.020= 65.pdf" target=3D"_blank">https://arxiv.org/pdf/1911.02065.pdf</a>}",<= br>=C2=A0 abstract =3D <br>=C2=A0 =C2=A0 "Traditional first-order logi= c (FOL) reasoning systems usually<br>=C2=A0 =C2=A0 rely on manual heuristic= s for proof guidance. We propose TRAIL: a<br>=C2=A0 =C2=A0 system that lear= ns to perform proof guidance using reinforcement<br>=C2=A0 =C2=A0 learning.= A key design principle of our system is that it is<br>=C2=A0 =C2=A0 genera= l enough to allow transfer to problems in different domains<br>=C2=A0 =C2= =A0 that do not share the same vocabulary of the training set. To do<br>=C2= =A0 =C2=A0 so, we developed a novel representation of the internal state of= a<br>=C2=A0 =C2=A0 prover in terms of clauses and inference actions, and a= novel<br>=C2=A0 =C2=A0 neural-based attention mechanism to learn interacti= ons between<br>=C2=A0 =C2=A0 clauses. We demonstrate that this approach ena= bles the system to<br>=C2=A0 =C2=A0 generalize from training to test data a= cross domains with<br>=C2=A0 =C2=A0 different vocabularies, suggesting that= the nerual architecture in<br>=C2=A0 =C2=A0 TRAIL is well suited for repre= senting and processing of logical<br>=C2=A0 =C2=A0 formalisms.",<br>= =C2=A0 paper =3D "Crou19.pdf"<br></div><div>}</div><div><br></div= ><div>@misc{Crou19a,<br>=C2=A0 author =3D "Crouse, Maxwell and Abdelaz= iz, Ibrahim and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cris= tina and Thost, Veronika and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 W= u, Lingfei and Forbus, Kenneth and Fokoue, Achille",<br>=C2=A0 title = =3D {{Improving Graph Neural Network Representations of Logical<br>=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Formulae with Subgraph Pooling}},<br>=C2= =A0 year =3D "2019",<br>=C2=A0 linke =3D "\url{<a href=3D"ht= tps://arxiv.org/pdf/1911.06904.pdf" target=3D"_blank">https://arxiv.org/pdf= /1911.06904.pdf</a>}",<br>=C2=A0 abstract =3D <br>=C2=A0 =C2=A0 "= Recent advances in the integration of deep learning with<br>=C2=A0 =C2=A0 a= utomated theorem proving have centered around the representation<br>=C2=A0 = =C2=A0 of graph-structured representations, in large part driven by the<br>= =C2=A0 =C2=A0 rapidly emerging body of research in geometric deep<br>=C2=A0= =C2=A0 learning. Typically, structure-aware neural methods for embedding<b= r>=C2=A0 =C2=A0 logical formulae have been variants of either Tree LSTMs or= <br>=C2=A0 =C2=A0 GNNs. While more effective than character and token-level= <br>=C2=A0 =C2=A0 approaches, such methods have often made representational= <br>=C2=A0 =C2=A0 trade-offs that limited their ability to effectively repr= esent the<br>=C2=A0 =C2=A0 global structure of their inputs. In this work, = we introduce a<br>=C2=A0 =C2=A0 novel approach for embedding logical formul= ae using DAG LSTMs that<br>=C2=A0 =C2=A0 is designed to overome the limitat= ions of both Tree LSTMs and<br>=C2=A0 =C2=A0 GNNs. The effectiveness of the= proposed framework is demonstrated<br>=C2=A0 =C2=A0 on the tasks of premis= e selection and proof step classification<br>=C2=A0 =C2=A0 where it achieve= s the state-of-the-art performance on two standard<br>=C2=A0 =C2=A0 dataset= s.", <br>=C2=A0 paper =3D "Crou19a.pdf"<br>}</div><div><br><= /div><div>@misc{Gaut19,<br>=C2=A0 author =3D "Gauthier, Thibault"= ,<br>=C2=A0 title =3D {{Deep Reinforcement Learning in HOL4}},<br>=C2=A0 ye= ar =3D "2019",<br>=C2=A0 link =3D "\url{<a href=3D"https://a= rxiv.org/pdf/1910.11797.pdf" target=3D"_blank">https://arxiv.org/pdf/1910.1= 1797.pdf</a>}",<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 "The pape= r describes an implementation of deep reinforcement<br>=C2=A0 =C2=A0 learni= ng through self-supervised learning within the proof<br>=C2=A0 =C2=A0 assis= tant HOL4. A close interaction between the machine learning<br>=C2=A0 =C2= =A0 modules and the HOL4 library is achieved by the choice of tree<br>=C2= =A0 =C2=A0 neural networks (TNNs) as machine learning models and the intern= al<br>=C2=A0 =C2=A0 use of HOL4 terms to represent tree structures of TNNs.= Recursive<br>=C2=A0 =C2=A0 improvement is possible when a given task is ex= pressed as a search<br>=C2=A0 =C2=A0 problem. In this case, a Monte Carlo T= ree Search (MCTS) algorithm<br>=C2=A0 =C2=A0 guided by a TNN can be used to= explore the search space and<br>=C2=A0 =C2=A0 produce better examples for = training the next TNN. As an<br>=C2=A0 =C2=A0 illustration, tasks over prop= ositional and arithmetical terms,<br>=C2=A0 =C2=A0 representative of fundam= ental theorem proving techniques, are<br>=C2=A0 =C2=A0 specified and learne= d: truth estimation, end-to-end computation,<br>=C2=A0 =C2=A0 term rewritin= g and term synthesis.",<br>=C2=A0 paper =3D "Gaut19.pdf"<br>= }</div><div><br></div><div>@misc{Lamp19,<br>=C2=A0 author =3D "Lample,= Guillaume and Charton, Francois",<br>=C2=A0 title =3D {{Deep Learning= for Symbolic Mathematics}},<br>=C2=A0 year =3D "2019",<br>=C2=A0= link =3D "\url{<a href=3D"https://arxiv.org/pdf/1912.01412.pdf" targe= t=3D"_blank">https://arxiv.org/pdf/1912.01412.pdf</a>}",<br>=C2=A0 lin= k =3D "\url{<a href=3D"https://www.youtube.com/watch?v=3DO_sHHG5_lr8" = target=3D"_blank">https://www.youtube.com/watch?v=3DO_sHHG5_lr8</a>}",= <br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 "Neural networks have a reput= ation for being better at solving<br>=C2=A0 =C2=A0 statistical or approxima= te problems than at performing<br>=C2=A0 =C2=A0 calculations or working wit= h symbolic data. In this paper, we show<br>=C2=A0 =C2=A0 that they can be s= urprisingly good at more elaborated tasks in<br>=C2=A0 =C2=A0 mathematics, = such as symbolic integration and solving differential<br>=C2=A0 =C2=A0 equa= tions. We propose a syntax for representing mathematical<br>=C2=A0 =C2=A0 p= roblems, and methods for generating large datasets that can be<br>=C2=A0 = =C2=A0 used to train sequence-to-sequence models. We achieve results that<b= r>=C2=A0 =C2=A0 outperform commercial Computer Algebra Systems such as Matl= ab or<br>=C2=A0 =C2=A0 Mathematica.",<br>=C2=A0 paper =3D "Lamp19= .pdf",<br>=C2=A0 keywords =3D "printed, DONE"<br>}</div><div= ><br></div><div>@misc{Olsa19,<br>=C2=A0 author =3D "Olsak, Miroslav an= d Kaliszyk, Cezary and Urban, Josef",<br>=C2=A0 title =3D {{Property I= nvariant Embedding for Automated Reasoning}},<br>=C2=A0 year =3D "2019= ",<br>=C2=A0 link =3D "\url{<a href=3D"https://arxiv.org/pdf/1911= .12073.pdf" target=3D"_blank">https://arxiv.org/pdf/1911.12073.pdf</a>}&quo= t;,<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 "Automated reasoning and t= heorem proving have recently become<br>=C2=A0 =C2=A0 major challenges for m= achine learning. In other domains,<br>=C2=A0 =C2=A0 representations that ar= e able to abstract over unimportant<br>=C2=A0 =C2=A0 transformations, such = as abstraction over translations and<br>=C2=A0 =C2=A0 rotations in vision, = are becoming more common. Standard methods of<br>=C2=A0 =C2=A0 embedding ma= thematical formulas for learning theorem proving are<br>=C2=A0 =C2=A0 howev= er yet unable to handle many important transformations. In<br>=C2=A0 =C2=A0= particular, embedding previously unseen labels, that often arise<br>=C2=A0= =C2=A0 in definitional encodings and in Skolemizatin, has been very weak<b= r>=C2=A0 =C2=A0 so far. Similar problems appear when tranferring knowledge = between<br>=C2=A0 =C2=A0 known symbols.<br><br>=C2=A0 =C2=A0 We propose a n= ovel encoding of formulas that extends existing<br>=C2=A0 =C2=A0 graph neur= al network models. This encoding represents symbols only<br>=C2=A0 =C2=A0 b= y nodes in the graph, without giving the network any knowledge of<br>=C2=A0= =C2=A0 the original labels. We provide additional links between such<br>= =C2=A0 =C2=A0 nodes that allow the network to recover the meaning and there= fore<br>=C2=A0 =C2=A0 correctly embed such nodes irrespective of the given = labels. We<br>=C2=A0 =C2=A0 test the proposed encoding in an automated theo= rem prover based on<br>=C2=A0 =C2=A0 the tableaux connection calculus, and = show that it improves on the<br>=C2=A0 =C2=A0 best characterizations used s= o far. The encoding is further<br>=C2=A0 =C2=A0 evaluated on the premise se= lection task and a newly introduced<br>=C2=A0 =C2=A0 symbol guessing task, = and shown to correctly predict 65\% of the<br>=C2=A0 =C2=A0 symbol names.&q= uot;,<br>=C2=A0 paper =3D "Olsa19.pdf"<br>}<br><br></div><div>@mi= sc{Piot19,<br>=C2=A0 author =3D "Piotrowski, Bartosz and Brown, Chad E= . and <br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Kaliszyk, Cezary",= <br>=C2=A0 title =3D {{Can Neural Networks Learn Symbolic Rewriting?}},<br>= =C2=A0 year =3D "2019",<br>=C2=A0 link =3D "\url{<a href=3D"= https://arxiv.org/pdf/1911.04783.pdf" target=3D"_blank">https://arxiv.org/p= df/1911.04783.pdf</a>}",<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 "= ;This work investigates if the current neural architectures are<br>=C2=A0 = =C2=A0 adequate for learning symbolic rewriting. Two kinds of data sets<br>= =C2=A0 =C2=A0 are proposed for this research -- one based on automated proo= fs<br>=C2=A0 =C2=A0 and the other being a synthetic set of polynomial terms= . The<br>=C2=A0 =C2=A0 experiments with use of the current neural machine t= ranslation<br>=C2=A0 =C2=A0 models are performed and its results are discus= sed. Ideas for<br>=C2=A0 =C2=A0 extending this line of research are propose= d and its relevance is<br>=C2=A0 =C2=A0 motivated.", <br>=C2=A0 paper = =3D "Piot19.pdf"<br>}<br><br>@misc{Sanc19,<br>=C2=A0 author =3D &= quot;Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence <br>=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and Lerner, Sorin",<br>=C2=A0 title= =3D {{Generating Correctness Proofs with Neural Networks}},<br>=C2=A0 year= =3D "2019",<br>=C2=A0 link =3D "\url{<a href=3D"https://arx= iv.org/pdf/1907.07794.pdf" target=3D"_blank">https://arxiv.org/pdf/1907.077= 94.pdf</a>}",<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 "Foundation= al verification allows programmers to build software<br>=C2=A0 =C2=A0 which= has been empirically shown to have high levels of assurance<br>=C2=A0 =C2= =A0 in a variety of important domains. However, the cost of producing<br>= =C2=A0 =C2=A0 foundationally verified software remains prohibitively high f= or<br>=C2=A0 =C2=A0 most projects, as it requires significant manual effort= by highly<br>=C2=A0 =C2=A0 trained experts. In this paper we present Prove= rbot9001 a proof<br>=C2=A0 =C2=A0 search system using machine learning tech= niques to produce proofs<br>=C2=A0 =C2=A0 of software correctness in intera= ctive theorem provers. We<br>=C2=A0 =C2=A0 deomonstrate Proverbot9001 on th= e proof obligations from a large<br>=C2=A0 =C2=A0 practical proof project, = the CompCert verified C compiler, and<br>=C2=A0 =C2=A0 show that it can eff= ectively automate what was previously manual<br>=C2=A0 =C2=A0 proofs, autom= atically solving 15.77\% of proofs in our test<br>=C2=A0 =C2=A0 dataset. Th= is corresponds to an over 3X improvement over the prior<br>=C2=A0 =C2=A0 st= ate of the art machine learning technique for generating proofs<br>=C2=A0 = =C2=A0 in Coq.",<br>=C2=A0 paper =3D "Sanc19.pdf"<br>}<br><b= r>@misc{Wang19a,<br>=C2=A0 author =3D "Wang, Qingxiang and Brown, Chad= and Kaliszyk, Cezary and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urba= n, Josef", <br>=C2=A0 title =3D {{Exploration of Neural Machine Transl= ation in<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of = Mathematics in Mizar}},<br>=C2=A0 year =3D "2019",<br>=C2=A0 link= =3D "\url{<a href=3D"https://arxiv.org/pdf/1912.02636.pdf" target=3D"= _blank">https://arxiv.org/pdf/1912.02636.pdf</a>}",<br>=C2=A0 abstract= =3D<br>=C2=A0 =C2=A0 "In this paper we share several experiments tryi= ng to<br>=C2=A0 =C2=A0 automatically translate informal mathematics into fo= rmal<br>=C2=A0 =C2=A0 mathematics. In our context informal mathematics refe= rs to<br>=C2=A0 =C2=A0 human-written mathematical sentences in the LaTeX fo= rmat; and<br>=C2=A0 =C2=A0 formal mathematics refers to statements in the M= izar language. We<br>=C2=A0 =C2=A0 conducted our experiments against three = established neural<br>=C2=A0 =C2=A0 network-based machine translation model= s that are know to deliver<br>=C2=A0 =C2=A0 competitive results on translat= ing between natural languages. To<br>=C2=A0 =C2=A0 train these models we al= so prepared four informal-to-formal<br>=C2=A0 =C2=A0 datasets. We compare a= nd analyze our results according to whether<br>=C2=A0 =C2=A0 the model is s= upervised or unsupervised. In order to augment the<br>=C2=A0 =C2=A0 data av= ailable for auto-formalization and improve the results, we<br>=C2=A0 =C2=A0= develop a custom type-elaboration mechanism and integrate it into<br>=C2= =A0 =C2=A0 the supervised translation.",<br>=C2=A0 paper =3D "Wan= g19a.pdf"<br>}<br><br><br></div><div><br></div><div><br></div><div><br= ></div></div></div> </blockquote></div> </blockquote></div> </blockquote></div> --000000000000c3745f05d5397925--