Artificial Intelligence to Assist Mathematical Reasoning Proceedings of a Workshop (2023) / Chapter Skim
Currently Skimming:
5 Technical Advances Required to Expand Artificial Intelligence for Mathematical Reasoning
5 Technical Advances Required to Expand Artificial Intelligence for Mathematical Reasoning
Pages 49-62
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 49... ...
Principles of Programming and Proof Language Giving an overview of the field of principles of programming languages, Pientka discussed what AI can do for mathematical reasoning from the perspective of the field's community. She described the research landscape in this field as a combination of work in programming languages based on logical principles, proofs about programs and programming languages themselves -- traditionally done on paper but increasingly using proof assistants, and implementation and evaluation of programming and proof environments.
|
From page 50... ...
In programming languages, the ground is like an earthquake zone, and work goes into establishing the stability of smaller houses, ensuring they do not collapse. Pientka explained that programming language proofs are difficult to write on paper because of the level of detail one must consider.
|
From page 51... ...
Second, proof automation has high potential for programming language proofs. Because the goal of proofs is often clear and the language is a moving target, she underscored that one should, in principle, be able to port proof structures to new languages, making programming language theory a useful testbed for proof automation.
|
From page 52... ...
He noted that this pattern of abstraction is so pervasive that a new type theory emerged as a default for the Hoare triple type. He said that each thread and Hoare type should have two local variables.
|
From page 53... ...
, which is designed to help them do this work efficiently. For widely used programming languages such as Python, IDE tools offer a programmer ML support in a carefully designed way which does not interrupt workflow, including auto complete tools like GitHub Copilot that quickly recompute "foreground" suggestions with each keystroke, as well as slower tools for "background" tasks that store suggestions unobtrusively for the user to consult later.
|
From page 54... ...
Pientka added that it would be useful to have methods to abstract conceptual ideas beyond the level of tactics, such as what clauses and rules are used for certain kinds of proofs. Ringer asked whether mathematicians truly need these kinds of logics and type theories, and, if so, how the speakers would convince them to invest in these foundations.
|
From page 55... ...
In response to a workshop participant's question requesting recommendations for introductory books or papers for mathematicians to learn more about proof assistants, the speakers shared resources. Nanevski offered "Programs and Proofs," a collection of lecture notes from a summer school led by Ilya Sergey.2 Pientka stated that something like P OPLMark for mathematicians would be incredibly valuable, recalling her earlier remarks that it was a small enough challenge to provide an entry point 2 These notes can be found at https://ilyasergey.net/pnp, accessed July 2, 2023.
|
From page 56... ...
RESEARCH ADVANCES IN THE MATHEMATICAL SCIENCES Speakers Javier Gómez-Serrano, Brown University; Adam Topaz, University of Alberta; and Alex Kontorovich, Rutgers University, presented research advances in the mathematical sciences and participated in a discussion moderated by Brendan Hassett, Brown University. Artificial Intelligence, Computer-Assisted Proofs, and Mathematics Gómez-Serrano discussed recent advances in the interplay among AI, computer-assisted proofs, and mathematics.
|
From page 57... ...
Formal Mathematics and Artificial Intelligence Topaz presented his experiences formalizing research-level mathematics and the ability of formal methods to act as a bridge between AI and mathematics. He distinguished library building from research mathematics, asserting that formal libraries capture a segment of mathematical knowledge in a formal system and are meant to be used in other formalization endeavors.
|
From page 58... ...
He concluded that between mathematics formalization and AI research, advances in one area can support the other, and he advocated for increased collaboration between the two. Artificial Intelligence to Assist Mathematical Reasoning Kontorovich presented the path to developing AI to assist mathematical reasoning, offering several "conjectures" about the realities and future of the field.
|
From page 59... ...
This question led Kontorovich to his second conjecture, stating that the path to AI assisting mathematical reasoning will be through an adversarial process, likely involving interactive theorem provers. He imagined a process involving feedback between an LLM and a theorem prover, with the LLM suggesting possible directions and the theorem prover certifying mathematical correctness of steps.
|
From page 60... ...
Formal mathematics libraries such as Lean's mathlib, Coq's Mathematical Components, Isabelle's Archive of Formal Proofs and the Mizar Mathematical Library are each already a kind of journal, with maintainers who are effectively editors and a completely open, public trail. The theorem proving community could start a mathematics journal associated with formal mathematics library development, where significant contributions are associated with a paper that could, for example, include AI to Assist Mathematical Reasoning AI makes its own Human Definitions and formalization Conjectures AI Assists in Theorem Proving Autoformalization: AI solves the AI learns to prove Riemann things we already Hypothesis know, verifiably Lean FIGURE 5-1 Flowchart of a potential future of artificial intelligence (AI)
|
From page 61... ...
Topaz recalled the demonstration he gave with sorry statements and described how AI could be useful; he added that as AI becomes a useful assistant, mathematicians will learn to write proofs in a way that is more amenable to AI assistance. Gómez-Serrano noted that one of the most significant contributions of LLMs is awareness -- the attention on LLMs gives mathematicians an opportunity to educate the public.
|
From page 62... ...
2020. "A Promising Path Towards Autoformalization and General Artificial Intelligence." 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.