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 <axiom...@gmail.com> 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" > } > > > > > >
