Re: A NN Solves and Generates Math Problems

--000000000000456b4a05d52a4e53
Content-Type: text/plain; charset="UTF-8"

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"
> }
>
>
>
>
>
>

--000000000000456b4a05d52a4e53
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Thanks for this! It seems to speak to the success of the O=
penAI Codex more than anything else, but the results are impressive.<div><b=
r></div><div>Bartosz Piotrowski, a PhD student and author of one of the pap=
ers you cited, will be visiting Carnegie Mellon for a few months this sprin=
g.</div><div><br></div><div>Best wishes,</div><div><br></div><div>Jeremy</d=
iv></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_att=
r">On Thu, Jan 6, 2022 at 10:30 AM Tim Daly &lt;<a href=3D"mailto:axiomcas@=
gmail.com">[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"=
gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(20=
4,204,204);padding-left:1ex"><div dir=3D"ltr"><div>This is an interesting p=
aper (especially given that it</div><div>is work under Gilbert Strang):</di=
v><div><br></div><div><div>A Neural Network Solves and Generates Mathematic=
s</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://arxiv.org/pdf/2112.15594.pdf=
</a></div><div><br></div><div>&quot;This work shows that a neural network t=
hat generates</div><div>programs (i.e. program synthesis) is the key to sol=
ving</div><div>math and STEM courses at scale, as it turns question</div><d=
iv>answering into a programming task.&quot;</div><div><br></div><div>This s=
eems interesting from several aspects:</div><div><br></div><div>1) Can this=
 be applied to logic systems? Can it help <br></div><div>generate &quot;pro=
ven code&quot; from a proof system? (LEAN)</div><div><br></div><div>2) Can =
it be applied in programs like NuPRL / RedPRL?</div><div>(Innovations in Co=
mputational Type Theory using Nuprl</div><div>Journal of Applied Logic 4 (2=
006) pp 428--469<br></div><div><a href=3D"https://reader.elsevier.com/reade=
r/sd/pii/S1570868305000704?token=3DC11F82ADA94390097338EF7E421A4D9DFEF90933=
6A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0AC6724F&amp;originRegion=
=3Dus-east-1&amp;originCreation=3D20220106150458" target=3D"_blank">https:/=
/reader.elsevier.com/reader/sd/pii/S1570868305000704?token=3DC11F82ADA94390=
097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0=
AC6724F&amp;originRegion=3Dus-east-1&amp;originCreation=3D20220106150458</a=
></div><div><br></div><div>3) Can the type of an object be inferred by cast=
ing it as a</div><div>question in mathematics? Is the generated program cor=
rectly</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 c=
ode?</div><div><br></div><div>5) Can this be applied to gradual typing?<br>=
</div><div><br></div><div>In any case, this represents an interesting &quot=
;interdisciplinary&quot;</div><div>effort connecting the math department an=
d CS.</div><div><br></div><div>Tim</div><div><br></div><div><br></div><div>=
<br></div><div>There are various connections to Neural Networks and Math:</=
div><div><br></div><div>@misc{Crou19,<br>=C2=A0 author =3D &quot;Crouse, Ma=
xwell 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 Kapanipathi, Pavan and<br>=C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pell, Edwin and Srinivas, Kavitha and<br=
>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Veronika and Witbrock, Mi=
chael and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fokoue, Achille&quot=
;,<br>=C2=A0 title =3D {{A Deep Reinforcement Learning Base Approach to Lea=
rning<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Transferable Proof Guidan=
ce Strategies}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 linke =3D &=
quot;\url{<a href=3D"https://arxiv.org/pdf/1911.02065.pdf" target=3D"_blank=
">https://arxiv.org/pdf/1911.02065.pdf</a>}&quot;,<br>=C2=A0 abstract =3D <=
br>=C2=A0 =C2=A0 &quot;Traditional first-order logic (FOL) reasoning system=
s usually<br>=C2=A0 =C2=A0 rely on manual heuristics for proof guidance. We=
 propose TRAIL: a<br>=C2=A0 =C2=A0 system that learns to perform proof guid=
ance using reinforcement<br>=C2=A0 =C2=A0 learning. A key design principle =
of our system is that it is<br>=C2=A0 =C2=A0 general enough to allow transf=
er 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 develope=
d 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 ne=
ural-based attention mechanism to learn interactions between<br>=C2=A0 =C2=
=A0 clauses. We demonstrate that this approach enables the system to<br>=C2=
=A0 =C2=A0 generalize from training to test data across 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 representing and processing of=
 logical<br>=C2=A0 =C2=A0 formalisms.&quot;,<br>=C2=A0 paper =3D &quot;Crou=
19.pdf&quot;<br></div><div>}</div><div><br></div><div>@misc{Crou19a,<br>=C2=
=A0 author =3D &quot;Crouse, Maxwell and Abdelaziz, Ibrahim and<br>=C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Thost, Veronika a=
nd<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Wu, Lingfei and Forbus, Ken=
neth and Fokoue, Achille&quot;,<br>=C2=A0 title =3D {{Improving Graph Neura=
l 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 &quot;2019&quot=
;,<br>=C2=A0 linke =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1911.069=
04.pdf" target=3D"_blank">https://arxiv.org/pdf/1911.06904.pdf</a>}&quot;,<=
br>=C2=A0 abstract =3D <br>=C2=A0 =C2=A0 &quot;Recent advances in the integ=
ration of deep learning with<br>=C2=A0 =C2=A0 automated theorem proving hav=
e centered around the representation<br>=C2=A0 =C2=A0 of graph-structured r=
epresentations, in large part driven by the<br>=C2=A0 =C2=A0 rapidly emergi=
ng body of research in geometric deep<br>=C2=A0 =C2=A0 learning. Typically,=
 structure-aware neural methods for embedding<br>=C2=A0 =C2=A0 logical form=
ulae have been variants of either Tree LSTMs or<br>=C2=A0 =C2=A0 GNNs. Whil=
e 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 represent the<br>=C2=A0 =C2=A0 g=
lobal structure of their inputs. In this work, we introduce a<br>=C2=A0 =C2=
=A0 novel approach for embedding logical formulae using DAG LSTMs that<br>=
=C2=A0 =C2=A0 is designed to overome the limitations of both Tree LSTMs and=
<br>=C2=A0 =C2=A0 GNNs. The effectiveness of the proposed framework is demo=
nstrated<br>=C2=A0 =C2=A0 on the tasks of premise selection and proof step =
classification<br>=C2=A0 =C2=A0 where it achieves the state-of-the-art perf=
ormance on two standard<br>=C2=A0 =C2=A0 datasets.&quot;, <br>=C2=A0 paper =
=3D &quot;Crou19a.pdf&quot;<br>}</div><div><br></div><div>@misc{Gaut19,<br>=
=C2=A0 author =3D &quot;Gauthier, Thibault&quot;,<br>=C2=A0 title =3D {{Dee=
p Reinforcement Learning in HOL4}},<br>=C2=A0 year =3D &quot;2019&quot;,<br=
>=C2=A0 link =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1910.11797.pdf=
" target=3D"_blank">https://arxiv.org/pdf/1910.11797.pdf</a>}&quot;,<br>=C2=
=A0 abstract =3D<br>=C2=A0 =C2=A0 &quot;The paper describes an implementati=
on of deep reinforcement<br>=C2=A0 =C2=A0 learning through self-supervised =
learning within the proof<br>=C2=A0 =C2=A0 assistant HOL4. A close interact=
ion between the machine learning<br>=C2=A0 =C2=A0 modules and the HOL4 libr=
ary is achieved by the choice of tree<br>=C2=A0 =C2=A0 neural networks (TNN=
s) as machine learning models and the internal<br>=C2=A0 =C2=A0 use of HOL4=
 terms to represent tree structures of TNNs. Recursive<br>=C2=A0 =C2=A0 imp=
rovement is possible when a given task is expressed as a search<br>=C2=A0 =
=C2=A0 problem. In this case, a Monte Carlo Tree 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<b=
r>=C2=A0 =C2=A0 illustration, tasks over propositional and arithmetical ter=
ms,<br>=C2=A0 =C2=A0 representative of fundamental theorem proving techniqu=
es, are<br>=C2=A0 =C2=A0 specified and learned: truth estimation, end-to-en=
d computation,<br>=C2=A0 =C2=A0 term rewriting and term synthesis.&quot;,<b=
r>=C2=A0 paper =3D &quot;Gaut19.pdf&quot;<br>}</div><div><br></div><div>@mi=
sc{Lamp19,<br>=C2=A0 author =3D &quot;Lample, Guillaume and Charton, Franco=
is&quot;,<br>=C2=A0 title =3D {{Deep Learning for Symbolic Mathematics}},<b=
r>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 link =3D &quot;\url{<a href=
=3D"https://arxiv.org/pdf/1912.01412.pdf" target=3D"_blank">https://arxiv.o=
rg/pdf/1912.01412.pdf</a>}&quot;,<br>=C2=A0 link =3D &quot;\url{<a href=3D"=
https://www.youtube.com/watch?v=3DO_sHHG5_lr8" target=3D"_blank">https://ww=
w.youtube.com/watch?v=3DO_sHHG5_lr8</a>}&quot;,<br>=C2=A0 abstract =3D<br>=
=C2=A0 =C2=A0 &quot;Neural networks have a reputation for being better at s=
olving<br>=C2=A0 =C2=A0 statistical or approximate problems than at perform=
ing<br>=C2=A0 =C2=A0 calculations or working with symbolic data. In this pa=
per, we show<br>=C2=A0 =C2=A0 that they can be surprisingly good at more el=
aborated tasks in<br>=C2=A0 =C2=A0 mathematics, such as symbolic integratio=
n and solving differential<br>=C2=A0 =C2=A0 equations. We propose a syntax =
for representing mathematical<br>=C2=A0 =C2=A0 problems, and methods for ge=
nerating large datasets that can be<br>=C2=A0 =C2=A0 used to train sequence=
-to-sequence models. We achieve results that<br>=C2=A0 =C2=A0 outperform co=
mmercial Computer Algebra Systems such as Matlab or<br>=C2=A0 =C2=A0 Mathem=
atica.&quot;,<br>=C2=A0 paper =3D &quot;Lamp19.pdf&quot;,<br>=C2=A0 keyword=
s =3D &quot;printed, DONE&quot;<br>}</div><div><br></div><div>@misc{Olsa19,=
<br>=C2=A0 author =3D &quot;Olsak, Miroslav and Kaliszyk, Cezary and Urban,=
 Josef&quot;,<br>=C2=A0 title =3D {{Property Invariant Embedding for Automa=
ted Reasoning}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 link =3D &q=
uot;\url{<a href=3D"https://arxiv.org/pdf/1911.12073.pdf" target=3D"_blank"=
>https://arxiv.org/pdf/1911.12073.pdf</a>}&quot;,<br>=C2=A0 abstract =3D<br=
>=C2=A0 =C2=A0 &quot;Automated reasoning and theorem proving have recently =
become<br>=C2=A0 =C2=A0 major challenges for machine learning. In other dom=
ains,<br>=C2=A0 =C2=A0 representations that are able to abstract over unimp=
ortant<br>=C2=A0 =C2=A0 transformations, such as abstraction over translati=
ons and<br>=C2=A0 =C2=A0 rotations in vision, are becoming more common. Sta=
ndard methods of<br>=C2=A0 =C2=A0 embedding mathematical formulas for learn=
ing theorem proving are<br>=C2=A0 =C2=A0 however yet unable to handle many =
important transformations. In<br>=C2=A0 =C2=A0 particular, embedding previo=
usly unseen labels, that often arise<br>=C2=A0 =C2=A0 in definitional encod=
ings and in Skolemizatin, has been very weak<br>=C2=A0 =C2=A0 so far. Simil=
ar problems appear when tranferring knowledge between<br>=C2=A0 =C2=A0 know=
n symbols.<br><br>=C2=A0 =C2=A0 We propose a novel encoding of formulas tha=
t extends existing<br>=C2=A0 =C2=A0 graph neural network models. This encod=
ing represents symbols only<br>=C2=A0 =C2=A0 by 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 therefore<br>=C2=A0 =C2=A0 correctly=
 embed such nodes irrespective of the given labels. We<br>=C2=A0 =C2=A0 tes=
t the proposed encoding in an automated theorem prover based on<br>=C2=A0 =
=C2=A0 the tableaux connection calculus, and show that it improves on the<b=
r>=C2=A0 =C2=A0 best characterizations used so far. The encoding is further=
<br>=C2=A0 =C2=A0 evaluated on the premise selection task and a newly intro=
duced<br>=C2=A0 =C2=A0 symbol guessing task, and shown to correctly predict=
 65\% of the<br>=C2=A0 =C2=A0 symbol names.&quot;,<br>=C2=A0 paper =3D &quo=
t;Olsa19.pdf&quot;<br>}<br><br></div><div>@misc{Piot19,<br>=C2=A0 author =
=3D &quot;Piotrowski, Bartosz and Brown, Chad E. and <br>=C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 Kaliszyk, Cezary&quot;,<br>=C2=A0 title =3D {{Can =
Neural Networks Learn Symbolic Rewriting?}},<br>=C2=A0 year =3D &quot;2019&=
quot;,<br>=C2=A0 link =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1911.=
04783.pdf" target=3D"_blank">https://arxiv.org/pdf/1911.04783.pdf</a>}&quot=
;,<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 &quot;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 f=
or this research -- one based on automated proofs<br>=C2=A0 =C2=A0 and the =
other being a synthetic set of polynomial terms. The<br>=C2=A0 =C2=A0 exper=
iments with use of the current neural machine translation<br>=C2=A0 =C2=A0 =
models are performed and its results are discussed. Ideas for<br>=C2=A0 =C2=
=A0 extending this line of research are proposed and its relevance is<br>=
=C2=A0 =C2=A0 motivated.&quot;, <br>=C2=A0 paper =3D &quot;Piot19.pdf&quot;=
<br>}<br><br>@misc{Sanc19,<br>=C2=A0 author =3D &quot;Sanchez-Stern, Alex a=
nd Alhessi, Yousef and Saul, Lawrence <br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 and Lerner, Sorin&quot;,<br>=C2=A0 title =3D {{Generating Correc=
tness Proofs with Neural Networks}},<br>=C2=A0 year =3D &quot;2019&quot;,<b=
r>=C2=A0 link =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1907.07794.pd=
f" target=3D"_blank">https://arxiv.org/pdf/1907.07794.pdf</a>}&quot;,<br>=
=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 &quot;Foundational 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 imp=
ortant domains. However, the cost of producing<br>=C2=A0 =C2=A0 foundationa=
lly verified software remains prohibitively high for<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 Proverbot9001 a proof<br>=C2=
=A0 =C2=A0 search system using machine learning techniques to produce proof=
s<br>=C2=A0 =C2=A0 of software correctness in interactive theorem provers. =
We<br>=C2=A0 =C2=A0 deomonstrate Proverbot9001 on the proof obligations fro=
m 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 effectively automate what =
was previously manual<br>=C2=A0 =C2=A0 proofs, automatically solving 15.77\=
% of proofs in our test<br>=C2=A0 =C2=A0 dataset. This corresponds to an ov=
er 3X improvement over the prior<br>=C2=A0 =C2=A0 state of the art machine =
learning technique for generating proofs<br>=C2=A0 =C2=A0 in Coq.&quot;,<br=
>=C2=A0 paper =3D &quot;Sanc19.pdf&quot;<br>}<br><br>@misc{Wang19a,<br>=C2=
=A0 author =3D &quot;Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary a=
nd<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urban, Josef&quot;, <br>=C2=
=A0 title =3D {{Exploration of Neural Machine Translation in<br>=C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of Mathematics in Mizar}}=
,<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 link =3D &quot;\url{<a hre=
f=3D"https://arxiv.org/pdf/1912.02636.pdf" target=3D"_blank">https://arxiv.=
org/pdf/1912.02636.pdf</a>}&quot;,<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 =
&quot;In this paper we share several experiments trying to<br>=C2=A0 =C2=A0=
 automatically translate informal mathematics into formal<br>=C2=A0 =C2=A0 =
mathematics. In our context informal mathematics refers to<br>=C2=A0 =C2=A0=
 human-written mathematical sentences in the LaTeX format; and<br>=C2=A0 =
=C2=A0 formal mathematics refers to statements in the Mizar language. We<br=
>=C2=A0 =C2=A0 conducted our experiments against three established neural<b=
r>=C2=A0 =C2=A0 network-based machine translation models that are know to d=
eliver<br>=C2=A0 =C2=A0 competitive results on translating between natural =
languages. To<br>=C2=A0 =C2=A0 train these models we also prepared four inf=
ormal-to-formal<br>=C2=A0 =C2=A0 datasets. We compare and analyze our resul=
ts according to whether<br>=C2=A0 =C2=A0 the model is supervised or unsuper=
vised. In order to augment the<br>=C2=A0 =C2=A0 data available for auto-for=
malization and improve the results, we<br>=C2=A0 =C2=A0 develop a custom ty=
pe-elaboration mechanism and integrate it into<br>=C2=A0 =C2=A0 the supervi=
sed translation.&quot;,<br>=C2=A0 paper =3D &quot;Wang19a.pdf&quot;<br>}<br=
><br><br></div><div><br></div><div><br></div><div><br></div></div></div>
</blockquote></div>

--000000000000456b4a05d52a4e53--