alreadydone / contents Goto Github PK

Harrison-John.pdf

Background: Mathematicians are listed as the occupation that is most exposed to large language models in research from OpenAI & UPenn: GPTs are GPTs: An Early Look at the Labor Market Impact Potential of Large Language Models.

See also How will AI change mathematics? Rise of chatbots highlights discussion, Feb 2023, Nature (mentions the IPAM workshop and Venkatesh symposium).

Kevin Buzzard on the Sparks of AGI paper:

For example in arguably the hardest math problem they give the system (p40, a modified IMO problem) I have several issues with their presentation. ...

When I was a kid in the early 80s, chess computers had just become viable. ... The only problem was that these chess computers were absolutely lousy at chess. They would never throw away pieces or accidentally let themselves get bank rank checkmated in 1, and they could beat rabbits by simply taking all their pieces and then overwhelming them, but on a reasonably hard setting they were still no match for an average club player, and if you put them on the hardest setting then they typically took hours to make a move. Down my chess club the kids loved them, and the experts showed no interest in them because they had nothing to teach the experts. 15 years later, thanks to IBM (who were at that time a powerhouse in the computing world) who decided to throw a ton of money at the problem, they were beating grandmasters, and since then we've never looked back.

I feel like we're in the "early 80s" phase right now with these large language models, and that is why I am super-uninterested in them right now. I certainly go around giving talks where I extol their virtues, and show a slide where they're solving 50% of the easiest IMO problem ever in Lean and claim that this is a breakthrough (which it is!). But at the end of the day GPT4 getting a half-decent mark in AMC 12, a multiple choice exam meant for schoolkids, is something which can simultaneously be regarded as an amazing achievement and something which indicates that there is still an essentially infinite amount of work still to be done before they are going to be doing research maths, which is why I am still bewildered by the claims of Szegedy¹ et al that this is going to happen by 2029. Right now they can beat rabbits at maths and that's it. Beating rabbits is a major achievement but undergraduates can easily do this too.

Shortly afterwards, Buzzard gave a talk to undergraduate students titled Will Computers Prove Theorems? (slides).²

Abstract: Today we have ChatGPT. In ten years' time will we have a machine where you can type in the statement of the Riemann Hypothesis, press a button, and out pops a correct proof? My guess is no. However in ten years' time will we have machines which can give humans mathematical ideas? Will we have interactive mathematics papers where you can choose the level of detail you want to see in a proof? Will we have machines which understand the state of the art in mathematics? Will mathematicians be being helped by computers in new ways? My guess is that these things are not out of the question. I'll talk about recent developments in AI and in theorem proving software which make me cautiously optimistic.

Now let me collect some reactions to AI from Fields medalists below:

Timothy Gowers is still pursuing his GOFAI approach to automated theorem proving, but he definitely plays a lot with ChatGPT. See also his talk at the Venkatesh symposium.

Terence Tao hosted the Machine Assisted Proofs workshop at IPAM in February (co-organized by Avigad, Buzzard, Jordan Ellenberg, Gowers among others). ChatGPT was a hot topic during the workshop, and Tao has been experimenting with integrating ChatGPT into daily workflow lately³. He also wondered about an automated tool for dependency graph drawing from papers.

Akshay Venkatesh has been thinking about the impact of AI (mechanization) on maths since as early as November 2021, and his Aleph Zero essay was the theme of a symposium held in October 2022 (pre-ChatGPT) organized by Buzzard, Michael Harris et al. Among the speakers were Avigad, Gowers, Andrew Granville, Geordie Williamson, Emily Riehl, and AI researchers Melanie Mitchell⁴ and Irina Rish. Harris collected participants' impressions in a blog post (and wrote some posts before the symposium as well). Venkatesh has this interesting idea that automated discovery of simplification of proofs could already have a huge impact on the evaluation of mathematical work and people:

Let us suppose that the energies of ℵ(0) are partly directed towards reworking the existing literature: revisiting and supplying proofs of known results rather than examining open questions. As we have emphasized, the number of mathematicians who have thought about a specific question is typically very small, and it is likely that very many parts of the literature would be greatly revised even through careful re-examination by many human mathematicians. It is not unlikely that we will see a scenario that has happened surprisingly rarely in recent history – replacement of long elaborate proofs by short overlooked ones. What effect might a five page combinatorial proof of the Weil conjectures have? Even if such an extreme scenario does not occur, it seems very likely that the web of relationships between standard lemmas and theorems will be altered. This discussion also suggests why the operators of ℵ(0) may be induced to revisit old problems over studying new ones: besides settling concerns about formal correctness, the shifting of foundations has a larger social impact than adding new levels.

Shing-Tung Yau just gave a talk at Fudan University on Friday, and he predicts no substantial change to human social structure within ten years, and top mathematicians won't be affected by AI:

Yau told a reporter from Yicai, "Artificial intelligence is unlikely to have any impact on top mathematicians, but it may have some impact on ordinary mathematicians."
He also predicted that AI would not have a big impact on human social structure within the next ten years, and most of the talk about AI replacing humans is "scaremongering." "Every era of technological change has produced such talk, but in the end, we have always passed through fairly smoothly," Yau told Yicai. "At least in the next ten years, I don't see any substantial changes that AI will make to human society, that is, changes in the entire structure of society."
In an interview with Yicai before the World AI Conference (WAIC) in Shanghai last August, Yau said, "The success of AI is actually a wonderful experience for everyone, but so far no one has been able to deeply explain why AI can be successful."
And this is precisely the path to success for OpenAI, when data accumulates to a certain amount, the ability of AI makes a qualitative leap. Yau once said, "Mathematics should find a way to discover the secrets of why AI is successful."
Six months later, when Yau was asked the same question by Yicai, he said, "A large amount of data will bring about qualitative changes, but qualitative changes are still limited, and I believe that we still need to further study and understand its entire structure."
He emphasized that the limitation of AI is that it can currently only integrate and synthesize a lot of existing data, but it is difficult to make scientific breakthroughs in terms of concepts. This means that AI is still unable to think creatively like humans.

Math Panel with Simon Donaldson, Maxim Kontsevich, Jacob Lurie, Terence Tao, Richard Taylor, and Yuri Milner (interviewer), 2015 Breakthrough Prize Symposium (Nov 10, 2014), Stanford University, https://youtu.be/eNgUQlpc1m0?t=2337 (Fields medalists in bold)

Against formalization:

Efim Zelmanov, On proof and progress in mathematics: the perspective of a research mathematician, in Mathematical Proof Between Generations, July 2022

William Thurston, On proof and progress in mathematics, https://arxiv.org/abs/math/9404236, April 1994 (historical document)

In response to https://leanprover-community.github.io/archive/stream/208328-IMO-grand-challenge/topic/Current.20status.3F.html#320982506

@Mario Carneiro I think models like the Toolformer that offloads/outsources some capabilities to external (symbolic) tools will drive down at least the inference cost, if not the training cost as well. The paper reports competitive zero-shot performance with much lower parameter count. (Langchain's MRKL systems are also mentioned by many people in connection with it.) RETRO performs well on knowledge-intensive tasks with much lower parameter count, by retrieving from a database rather than a toolbox. And there are architecture innovations like RWKV-LM that are less resource-intensive than transformers but may prove to be as powerful (they just released an RNN with 14B parameters).

Next-generation models may be trained to not just use tools, but also create tools and organize them into a codebase (think of long-term memory, or crystallized intelligence), and they're gonna read books and papers and grow mathlib for us automatically (auto-formalization). Being able to execute programs and observe outputs serves as a strong form of grounding (Yoav Goldberg, 5th paragraph), similar to formalization of mathematics. Drori et al.'s PNAS paper and Program-aided Language Models from CMU already do program synthesis in Python, but do not store the programs and build upon them; as we know, to prove a big theorem, it's often necessary to have lots of intermediate lemmas in place.

As the model continually learns, it might gradually optimize programs in its codebase (think of AlphaTensor), including other models it creates and stores there, so more efficient models could eventually emerge in the codebase and the original model could offload most of its capability to them, and we could just use the most efficient one. The original model probably need to be of adaptive computation time though, since otherwise offloading can't possibly save time even though it may improve accuracy. Data center cooling, neural architecture search, and chip design are other places where a positive feedback loop for AI efficiency could be formed.

ChatGPT has shown that reinforcement learning can be a very effective way of aligning language models to our purposes, and a codebase has a naturally associated dependency graph, which could potentially help with credit assignment, so actions that wrote the most popular functions/theorems in the codebase/library could be rewarded. As a bonus, PageRank is easy on a DAG.

I've written down some thoughts in this tweet thread a few weeks ago but apparently I was talking into air 😂 Are my ideas too crazy, or too well-known and already actively pursued in major labs @Geoffrey Irving @Timothee Lacroix? Or maybe I was just shadow-banned by Twitter. (Unfortunately it seems OpenAI's Lean paper authors have all left ...)

I think these ideas overlap with those of memorizing transformers from @Yuhuai Tony Wu, @Christian Szegedy, et al. which use non-differentiable memory as well, but memory access is via kNN lookup of vector embeddings. Since LMs are supposed to good at languages, I think it's natural to let them establish and follow naming conventions to name the new concepts they invented, and interact with their memory via tokens, but I don't have the experience to judge which approach is more practical.

As for democratization of access, I'm generally optimistic: I'm pretty impressed that I can now run Stable Diffusion (SD) to create 512x512 images with just 4GB VRAM on my laptop. And it may not be difficult to adapt LMs to our particular purpose: for example, it now suffice to fine-tune only 3MB of the SD model's parameters on custom data, thanks to LoRA. Open Assistant is now crowd-sourcing training data to create a ChatGPT clone, and this paradigm of distributed data generation combined with centralized training could be traced back to Leela Zero / Leela Chess Zero. It's worth noting that people are building distributed training infrastructure as well, but it may take time to mature.

Volunteer computing has a long history and people have donated massive amounts of compute to projects like GIMPS (Mersenne prime search), or Fishtest, and through BOINC. So it's just a matter of popularizing mathematics to get more computing resources directed to mathlib. When AI is capable of creating new mathematics, it will draw even more volunteer resources: it's much more exciting to see long-standing conjectures being solved than seeing Elo rating keeps improving monotonically (pun intended). Considering how fast LMs can turn natural language into code and vice versa (already useful in reverse engineering), I think the formal-informal gap could be fairly small for machines.

Time is on our side. Conversational LMs will revolutionize education, and people around the world will get equal access to the most sophisticated mathematical ideas. Advanced mathematics will come out of brains of geniuses and ivory towers and reach more people than ever. (mathlib is already democratizing access to every detail for every proof and definition in it, which you don't normally get in textbooks, and LMs will be able to parse and summarize the Lean code and explain the big picture.) As automation progresses and people work less hours, they will have more spare time to devote to mathematics, among other means of entertainment. Gladly, Microsoft's CEO seems to share the same vision:

Do we need to learn math anymore? Why learn math?
Lemme tell you, I'm an electrical engineer who never understood the Maxwell's equations. So now I finally get, thanks to ChatGPT, a better understanding of it. So I think one of the things is we will all enjoy a lot more math because we will have that personalized tutor who will, in fact, be able to intervene at the crucial time when you're making a conceptual mistake and help you learn. So just imagine that, just Matt, what if there was a fantastic tutor teacher for every student learning math going forward, that is now possible.

Exciting times are ahead!

(Mandatory disclaimer: ChatGPT did not engage in the writing of this essay.)

[The following two posts are my reply to /u/starspawn0's comment on the paper Language Modeling for Formal Mathematics by Christian Szegedy et al., posted on subreddit 'thisisthewayitwillbe', in which he asked "why they don't just try to train large language models to write proofs the way humans do, and worry about mapping it all to a more useful form (HOL/Isabelle-checkable) later".]