A NN Solves and Generates Math Problems

--000000000000f134e205d4eb8a72
Content-Type: text/plain; charset="UTF-8"

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

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

<div dir=3D"ltr"><div>This is an interesting paper (especially given that i=
t</div><div>is work under Gilbert Strang):</div><div><br></div><div><div>A =
Neural Network Solves and Generates Mathematics</div><div>Problems by Proga=
m Synthesis: Calculus, Differential</div><div>Equations, Linear Algebra, an=
d More.</div><div><a href=3D"https://arxiv.org/pdf/2112.15594.pdf">https://=
arxiv.org/pdf/2112.15594.pdf</a></div><div><br></div><div>&quot;This work s=
hows that a neural network that generates</div><div>programs (i.e. program =
synthesis) is the key to solving</div><div>math and STEM courses at scale, =
as it turns question</div><div>answering into a programming task.&quot;</di=
v><div><br></div><div>This seems interesting from several aspects:</div><di=
v><br></div><div>1) Can this be applied to logic systems? Can it help <br><=
/div><div>generate &quot;proven 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 Computational Type Theory using Nuprl</div><div>J=
ournal of Applied Logic 4 (2006) pp 428--469<br></div><div><a href=3D"https=
://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=3DC11F82ADA943=
90097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955=
D0AC6724F&amp;originRegion=3Dus-east-1&amp;originCreation=3D20220106150458"=
>https://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=3DC11F82=
ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77F=
FC4955D0AC6724F&amp;originRegion=3Dus-east-1&amp;originCreation=3D202201061=
50458</a></div><div><br></div><div>3) Can the type of an object be inferred=
 by casting it as a</div><div>question in mathematics? Is the generated pro=
gram correctly</div><div>typed?</div><div><br></div><div>4) Can this be lay=
ered on MetaMath (LEAN) or FDL (Nuprl)</div><div>to generate logically equi=
valent code?</div><div><br></div><div>5) Can this be applied to gradual typ=
ing?<br></div><div><br></div><div>In any case, this represents an interesti=
ng &quot;interdisciplinary&quot;</div><div>effort connecting the math depar=
tment and CS.</div><div><br></div><div>Tim</div><div><br></div><div><br></d=
iv><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;Cr=
ouse, 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 Kapanipathi, Pavan and<b=
r>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pell, Edwin and Srinivas, Kavit=
ha and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Veronika and Wit=
brock, Michael and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fokoue, Ach=
ille&quot;,<br>=C2=A0 title =3D {{A Deep Reinforcement Learning Base Approa=
ch to Learning<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Transferable Pro=
of Guidance Strategies}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 li=
nke =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1911.02065.pdf">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 systems 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 guidance usin=
g reinforcement<br>=C2=A0 =C2=A0 learning. A key design principle of our sy=
stem is that it is<br>=C2=A0 =C2=A0 general enough to allow transfer to pro=
blems in different domains<br>=C2=A0 =C2=A0 that do not share the same voca=
bulary 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-base=
d attention mechanism to learn interactions between<br>=C2=A0 =C2=A0 clause=
s. 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;Crou19.pdf&qu=
ot;<br></div><div>}</div><div><br></div><div>@misc{Crou19a,<br>=C2=A0 autho=
r =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 and<br>=C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Wu, Lingfei and Forbus, Kenneth and =
Fokoue, Achille&quot;,<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 Fo=
rmulae 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.06904.pdf">h=
ttps://arxiv.org/pdf/1911.06904.pdf</a>}&quot;,<br>=C2=A0 abstract =3D <br>=
=C2=A0 =C2=A0 &quot;Recent advances in the integration of deep learning wit=
h<br>=C2=A0 =C2=A0 automated theorem proving have centered around the repre=
sentation<br>=C2=A0 =C2=A0 of graph-structured representations, in large pa=
rt driven by the<br>=C2=A0 =C2=A0 rapidly emerging body of research in geom=
etric deep<br>=C2=A0 =C2=A0 learning. Typically, structure-aware neural met=
hods for embedding<br>=C2=A0 =C2=A0 logical formulae have been variants of =
either Tree LSTMs or<br>=C2=A0 =C2=A0 GNNs. While more effective than chara=
cter and token-level<br>=C2=A0 =C2=A0 approaches, such methods have often m=
ade representational<br>=C2=A0 =C2=A0 trade-offs that limited their ability=
 to effectively represent the<br>=C2=A0 =C2=A0 global structure of their in=
puts. In this work, we introduce a<br>=C2=A0 =C2=A0 novel approach for embe=
dding 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 demonstrated<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 performance 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;Gau=
thier, Thibault&quot;,<br>=C2=A0 title =3D {{Deep 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">https://arxiv.org/pdf/191=
0.11797.pdf</a>}&quot;,<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 &quot;The p=
aper describes an implementation of deep reinforcement<br>=C2=A0 =C2=A0 lea=
rning through self-supervised learning within the proof<br>=C2=A0 =C2=A0 as=
sistant 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 int=
ernal<br>=C2=A0 =C2=A0 use of HOL4 terms to represent tree structures of TN=
Ns. Recursive<br>=C2=A0 =C2=A0 improvement is possible when a given task is=
 expressed as a search<br>=C2=A0 =C2=A0 problem. In this case, a Monte Carl=
o 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 f=
or training the next TNN. As an<br>=C2=A0 =C2=A0 illustration, tasks over p=
ropositional and arithmetical terms,<br>=C2=A0 =C2=A0 representative of fun=
damental theorem proving techniques, are<br>=C2=A0 =C2=A0 specified and lea=
rned: truth estimation, end-to-end computation,<br>=C2=A0 =C2=A0 term rewri=
ting and term synthesis.&quot;,<br>=C2=A0 paper =3D &quot;Gaut19.pdf&quot;<=
br>}</div><div><br></div><div>@misc{Lamp19,<br>=C2=A0 author =3D &quot;Lamp=
le, Guillaume and Charton, Francois&quot;,<br>=C2=A0 title =3D {{Deep Learn=
ing for Symbolic Mathematics}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=
=A0 link =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1912.01412.pdf">ht=
tps://arxiv.org/pdf/1912.01412.pdf</a>}&quot;,<br>=C2=A0 link =3D &quot;\ur=
l{<a href=3D"https://www.youtube.com/watch?v=3DO_sHHG5_lr8">https://www.you=
tube.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 solving=
<br>=C2=A0 =C2=A0 statistical or approximate problems than at performing<br=
>=C2=A0 =C2=A0 calculations or working with symbolic data. In this paper, w=
e show<br>=C2=A0 =C2=A0 that they can be surprisingly good at more elaborat=
ed tasks in<br>=C2=A0 =C2=A0 mathematics, such as symbolic integration and =
solving differential<br>=C2=A0 =C2=A0 equations. We propose a syntax for re=
presenting mathematical<br>=C2=A0 =C2=A0 problems, and methods for generati=
ng large datasets that can be<br>=C2=A0 =C2=A0 used to train sequence-to-se=
quence models. We achieve results that<br>=C2=A0 =C2=A0 outperform commerci=
al Computer Algebra Systems such as Matlab or<br>=C2=A0 =C2=A0 Mathematica.=
&quot;,<br>=C2=A0 paper =3D &quot;Lamp19.pdf&quot;,<br>=C2=A0 keywords =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, Jos=
ef&quot;,<br>=C2=A0 title =3D {{Property Invariant Embedding for Automated =
Reasoning}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 link =3D &quot;=
\url{<a href=3D"https://arxiv.org/pdf/1911.12073.pdf">https://arxiv.org/pdf=
/1911.12073.pdf</a>}&quot;,<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 &quot;A=
utomated reasoning and theorem proving have recently become<br>=C2=A0 =C2=
=A0 major challenges for machine learning. In other domains,<br>=C2=A0 =C2=
=A0 representations that are 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 mathematical formulas for learning theorem provi=
ng are<br>=C2=A0 =C2=A0 however yet unable to handle many important transfo=
rmations. In<br>=C2=A0 =C2=A0 particular, embedding previously unseen label=
s, that often arise<br>=C2=A0 =C2=A0 in definitional encodings and in Skole=
mizatin, has been very weak<br>=C2=A0 =C2=A0 so far. Similar problems appea=
r when tranferring knowledge between<br>=C2=A0 =C2=A0 known symbols.<br><br=
>=C2=A0 =C2=A0 We propose a novel encoding of formulas that extends existin=
g<br>=C2=A0 =C2=A0 graph neural network models. This encoding represents sy=
mbols only<br>=C2=A0 =C2=A0 by nodes in the graph, without giving the netwo=
rk any knowledge of<br>=C2=A0 =C2=A0 the original labels. We provide additi=
onal links between such<br>=C2=A0 =C2=A0 nodes that allow the network to re=
cover the meaning and therefore<br>=C2=A0 =C2=A0 correctly embed such nodes=
 irrespective of the given labels. We<br>=C2=A0 =C2=A0 test the proposed en=
coding in an automated theorem prover based on<br>=C2=A0 =C2=A0 the tableau=
x connection calculus, and show that it improves on the<br>=C2=A0 =C2=A0 be=
st characterizations used so far. The encoding is further<br>=C2=A0 =C2=A0 =
evaluated on the premise selection 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.&quot;,<br>=C2=A0 paper =3D &quot;Olsa19.pdf&quo=
t;<br>}<br><br></div><div>@misc{Piot19,<br>=C2=A0 author =3D &quot;Piotrows=
ki, 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 Le=
arn Symbolic Rewriting?}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 l=
ink =3D &quot;\url{<a href=3D"https://arxiv.org/pdf/1911.04783.pdf">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 da=
ta sets<br>=C2=A0 =C2=A0 are proposed for this research -- one based on aut=
omated proofs<br>=C2=A0 =C2=A0 and the other being a synthetic set of polyn=
omial terms. The<br>=C2=A0 =C2=A0 experiments with use of the current neura=
l 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 and Alhessi, Yousef and Saul, Lawrenc=
e <br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and Lerner, Sorin&quot;,<br=
>=C2=A0 title =3D {{Generating Correctness Proofs with Neural Networks}},<b=
r>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 link =3D &quot;\url{<a href=
=3D"https://arxiv.org/pdf/1907.07794.pdf">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 ha=
s 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 for<br>=
=C2=A0 =C2=A0 most projects, as it requires significant manual effort by hi=
ghly<br>=C2=A0 =C2=A0 trained experts. In this paper we present Proverbot90=
01 a proof<br>=C2=A0 =C2=A0 search system using machine learning techniques=
 to produce proofs<br>=C2=A0 =C2=A0 of software correctness in interactive =
theorem provers. We<br>=C2=A0 =C2=A0 deomonstrate Proverbot9001 on the proo=
f obligations from a large<br>=C2=A0 =C2=A0 practical proof project, the Co=
mpCert verified C compiler, and<br>=C2=A0 =C2=A0 show that it can effective=
ly automate what was previously manual<br>=C2=A0 =C2=A0 proofs, automatical=
ly solving 15.77\% of proofs in our test<br>=C2=A0 =C2=A0 dataset. This cor=
responds to an over 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 Ka=
liszyk, Cezary and<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urban, Jose=
f&quot;, <br>=C2=A0 title =3D {{Exploration of Neural Machine Translation i=
n<br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of Mathema=
tics in Mizar}},<br>=C2=A0 year =3D &quot;2019&quot;,<br>=C2=A0 link =3D &q=
uot;\url{<a href=3D"https://arxiv.org/pdf/1912.02636.pdf">https://arxiv.org=
/pdf/1912.02636.pdf</a>}&quot;,<br>=C2=A0 abstract =3D<br>=C2=A0 =C2=A0 &qu=
ot;In this paper we share several experiments trying to<br>=C2=A0 =C2=A0 au=
tomatically translate informal mathematics into formal<br>=C2=A0 =C2=A0 mat=
hematics. In our context informal mathematics refers to<br>=C2=A0 =C2=A0 hu=
man-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<br=
>=C2=A0 =C2=A0 network-based machine translation models that are know to de=
liver<br>=C2=A0 =C2=A0 competitive results on translating between natural l=
anguages. To<br>=C2=A0 =C2=A0 train these models we also prepared four info=
rmal-to-formal<br>=C2=A0 =C2=A0 datasets. We compare and analyze our result=
s according to whether<br>=C2=A0 =C2=A0 the model is supervised or unsuperv=
ised. In order to augment the<br>=C2=A0 =C2=A0 data available for auto-form=
alization and improve the results, we<br>=C2=A0 =C2=A0 develop a custom typ=
e-elaboration mechanism and integrate it into<br>=C2=A0 =C2=A0 the supervis=
ed 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>

--000000000000f134e205d4eb8a72--