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