Artificial Intelligence to Assist Mathematical Reasoning Proceedings of a Workshop (2023) / Chapter Skim
Currently Skimming:
2 Overview and Grand Vision
2 Overview and Grand Vision
Pages 5-10
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 5... ...
THE QUEST FOR AUTOMATED REASONING Vardi provided a brief history of mathematical proof and reasoning, beginning in ancient Greece and leading up to automated reasoning in the present day. He described the ancient Greek concept of the deductive proof as an airtight argument whose concept marked the beginning of mathematical reasoning.
|
From page 6... ...
In closing, Vardi remarked that the quest for automated reasoning is at the heart of mathematics and computer science. Huge progress has been made in Boolean reasoning, automated deduction, and proof assistants, as well as in the formal verification of programs and in formalized mathematics.
|
From page 7... ...
ha ( is os ra ff in tE is l se se in Si tE zC ec ha G in kM Sa om Sa co co Pr M zC er t+ lu lu pt + B G G ry at sa C is R in M S
|
From page 8... ...
Williamson presented an example using TensorFlow Playground2 that trained a function to classify orange versus blue nodes on a spiral. He emphasized that the process is stochastic, as well as not necessarily monotonically improving.
|
From page 9... ...
Williamson noted that researchers generally have held the position that NNs will remain black boxes, but recent work has pointed toward the future possibility of distilling human comprehension from them. Hassett inquired about the kinds of mathematical problems that will be susceptible to NN techniques.
|
From page 10... ...
Finally, Hassett asked Williamson and Vardi for their advice for a young person looking to enter this area of research. Vardi expressed that the PhD path is best for a person who finds it intellectually thrilling to be at the interface between the known and unknown.
|
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.