In general, I'm pretty skeptical of Neural Net generation of math, but I'm following the literature quite closely.
I recently spent time with an effort that tried to do integration. It was interesting because they could "round trip" the solution by differentiating the result. I worked with the authors, added some of their results to Axiom, and suggested possible further work. But the approach, while it looks impressive, has quite a few flaws. I have yet to "deep dive" into this paper. It is really interesting to me that it claims to generate code. I would like to see a "round trip" where some LEAN math was used to generate code and then the code was proven using LEAN. Especially interesting would be the question of how the definitions and axioms of the original LEAN proof were used, if at all, in the proof of the code. (Of course, LEAN doesn't seem to focus on proving code.) >From an Axiom point of view, "proven code generation" from a proven theorem is my holy grail. If there was a way to form a one-to-one, onto mapping between theorems and code I'd be rewriting all of Axiom using it. I doubt that a Neural Net can achieve such a mapping. Given that Axiom is using first-class dependent types I'm not at all clear how that could be possible using a Neural Net. Can a Neural Net even infer the correct Types? I suppose, for the simple case such as NAT, it could "learn" from the definitions but cubical types might be a tad bit harder. Nor is it clear to me how you would generate code that was sound but not complete. I just looked up Bartosz's body of work. It looks really interesting, giving me much more to read. Tim On Sun, Jan 9, 2022 at 1:22 PM Jeremy Avigad <avi...@cmu.edu> wrote: > 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" >> } >> >> >> >> >> >>
