Artificial Intelligence to Assist Mathematical Reasoning Proceedings of a Workshop (2023) / Chapter Skim
Currently Skimming:
3 Case Studies
3 Case Studies
Pages 11-22
The Chapter Skim interface presents what we've algorithmically identified as the most significant single chunk of text within every page in the chapter.
Select key terms on the right to highlight them within pages of the chapter.
From page 11... ...
CASE STUDIES: ARTIFICIAL INTELLIGENCE TO ASSIST MATHEMATICAL REASONING Yann LeCun, Meta Platforms, Inc., moderated the session on case studies in AI to assist mathematical reasoning; he introduced speakers François Charton, Meta AI, and Adam Wagner, Worcester Polytechnic Institute. Reasoning with Transformers Charton presented the goal of solving mathematical problems with a transformer -- a type of neural network (NN)
|
From page 12... ...
Even when the model failed, it respected certain properties, which suggests that some of the underlying mathematics was learned. Furthermore, when he altered the experiment and stopped training the model after it reached 70 percent accuracy, it still predicted eigenvalues correctly in 99.6 percent of test cases.
|
From page 13... ...
He acknowledged that this was a "dream scenario," with both an obvious way to phrase the conjecture as a game and an obvious choice of reward function. Wagner shared five more complex examples with unique challenges in which the RL algorithm still successfully refuted an open conjecture.
|
From page 14... ...
Wagner's final example studied a conjecture posed by Paul Erdős in 1962, which differed from his earlier examples in that any counter example must be an infinite sequence of graphs. Wagner and his colleague Gwenaël Joret found a way to produce a counterexample with RL by using a standard "trick" in graph theory: constructing a finite graph and then taking a limit to infinity.
|
From page 15... ...
Charton described the motivation of curriculum learning; the logarithmic distribution ensures that the model trains on a greater number of simpler cases, imitating how humans first learn simple problems before learning more difficult ones. Delving into more general topics, LeCun posed a question about how combining generative methods like LLMs with computational and mathematical tools like WolframAlpha might be useful in the context of mathematical reasoning.
|
From page 16... ...
Before the advent of computers, absolute precision in mathematics was considered unfeasible. However, mathematicians can now write complex proofs precisely using interactive proof assistants, which he defined as "software that helps mathematicians [and]
|
From page 17... ...
Additional motivation for using proof assistants arises from the way these tools push researchers to consider how to express formal rules for mathematics, which can lead to new insights; for example, recent work revealed new logical insight about the notion of equality -- a very basic mathematical notion -- and unexpected connections between equality and the field of homotopy theory. Proof assistants can provide a new avenue for mathematicians to organize their ideas and to improve their understanding of complex proofs, which could ultimately lead to producing better proofs.
|
From page 18... ...
He pointed workshop participants toward a tool developed by Patrick Massot and Kyle Miller with interactive elements that allow users to hover over statements and see the current Lean proof state in ordinary language, among other functionalities.7 For authors, Commelin asserted that formal proofs should be flexible (in terms of foundations, input, and output) , powerful, and expressive.
|
From page 19... ...
Mathematics Versus Computer Science Proofs Offering a perspective from computer science, Morrisett expressed that one of the main challenges today in software security is ensuring that there are no bugs that can be exploited. The hope in software verification is that proof assistants can check correctness, safety, and security in the massive amounts of code that cannot be checked properly by humans.
|
From page 20... ...
At this point, Morrisett and some of his students decided to build a formally verified checker for the software fault isolation tool. Morrisett noted that constructing code and its proof of correctness together is often easier than verifying code after the fact.
|
From page 21... ...
Morrisett described writing definitions as very difficult, which Commelin and Coquand both seconded. Ringer followed up by inquiring about the most useful qualities for practical proof automation.
|
From page 22... ...
2012. "Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs." Pp.
|
Key Terms
This material may be derived from roughly machine-read images, and so is provided only to facilitate research.
More
information on Chapter Skim is available.