Re: A NN Solves and Generates Math Problems
Suppose the goal was to generate code from proofs.
Suppose that certain tactics have "code-like" equivalents.
Can we define such a restricted set of tactics?
This would eliminate Coq's hammer tactic, for example.
The definition of an axiom could include the text for the
equivalent program, making them "effective theorems",
or "fully constructive theorems".
Given a proof of a theorem from this restricted set
it should be (somewhat) easier to create equivalent programs.
This amounts to "proving the theorem" by "writing the program",
albeit in a tactic language.
For example, a "reduce" tactic would apply a function to a
set of numbers (symbolically), with the proof condition that
the set is finite and the generated index decreases so we
can know that "reduce" terminates. That would then be
equivalent to the Lisp map operation.
Tim
On Sun, Jan 9, 2022 at 4:56 PM Tim Daly wrote:
> 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 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 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 Reinf
Re: A NN Solves and Generates Math Problems
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 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 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 neru
Re: A NN Solves and Generates Math Problems
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 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
