A Neural Network Solves and Generates Mathematics
Problems by Progam Synthesis: Calculus, Differential
Equations, Linear Algebra, and More.
"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
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"
}