 |
Slide in Lev Reyzin's JMM talk "Problems in AI and ML for Mathematicians" Reyzin is paraphrasing Telgarsky. Posted with permission. |
We Decide Our Future: Mathematics in the Age of AI
With little computational complexity in the conference, I attended many of the AI talks. You could divide them into Math for AI and AI for Math. Mathematics of course plays critical roles in machine learning optimization, and several talks focused on provably good learning algorithms, though they overemphasized the importance of such. Do you get on a plane because you understand the physics or because air travel has a strong safety record?
But let's focus on AI for Math which generated the most discussion and angst.
I started the conference sitting on a panel on the challenges of peer review in mathematics. Math doesn't have the replication crisis that dogs other scientific communities. But math does have papers with very specialized, long, detailed proofs and few qualified referees willing to check them over with care.
We're not there yet, but in the "near future" we ought to have AI systems that can verify well-written proofs by compiling them using proof assistants like Lean. Referees could spend less time on checking proofs and more on deciding whether the model, theorem and/or techniques merit publication. We might get to the point that you couldn't even submit a paper to a journal until the proofs have been verified.
It's what comes next that really spooks mathematicians. While AI has made significant progress in solving competition problems with DeepMind's AlphaProof and Open AI's O3, it has only played minor roles in developing new ideas for theorems. Eventually AI systems will find critical steps for publishable theorems. Who do we give the credit to? When AI systems become stronger that typical PhD students, what kinds of problems to we give the students?
We'll get plenty of AI slop, flooding journals with mathematical papers that technically prove new theorems but don't offer any particularly interesting or illuminating insights. But we'll also get mathematicians who can unleash an army of virtual grad students to find new connections between different subfields, or make significant progress on major open problems in the field.
Some mathematicians don't want AI trained on their papers and using their techniques and theorems, even though they wouldn't have problems with other mathematicians doing so. In any case, they might not have much choice as many publishers are making deals with AI companies.
The future of mathematicians might follow that of artists and programmers. The best will do fine since they can find proofs beyond what an AI can do. Mathematicians who know how to ask the right questions can harness AI to make themselves far more productive. All mathematicians will have to navigate this brave new world.
"At least they'll still need us to teach the courses," one mathematician told me. Don't be so sure.
Attending a lecture is like going to a drama theater, watching a recorded lecture from home is like watching a movie, and of course you can also read a (text)book. As long as people go to theaters, there will be lecturers. But I agree that a large part of education could go to the AI - hopefully grading homework assignments will be among them...
ReplyDeleteIt's a strange experience to constantly hear how AI will take over all intellectual work, while all my experiences of actually using shows it can't be used for anything beyond bad art and platitudes.
ReplyDeleteWatching AI mania and their champions is as sad as watching LA wildfires eviscerating vast stretches of land where people populated known wildfire prone regions; both will only end when they have fully exhausted their resources one fuel, other capital.
Delete"Referees could spend less time on checking proofs". I always thought it wasn't the referee's job to check the proof, except in special circumstances like solving a major problem.
ReplyDeleteThat's true is CS theory conferences but math journals still want their proofs checked. Some journals will start with a quick review process where an expert will check that a result is interesting before sending it out for a proof check.
Deletehttps://www.ams.org/journals/notices/202409/rnoti-p1183.pdf
Delete"They don't need me to carefully check their proofs"
"Given that you're already reviewing a paper, why not also check the details of the proofs? If you have the time and inclination for this, by all means. But as your career progresses and your responsibilities accumulate, you will have less time while simultaneously finding yourself qualified to review more papers. At some point, certifying correctness will become infeasible. Sure, authors will be grateful if you notice a mistake in a proof, just like they will be grateful if you point out a typo, but this isn't your job."
That's one person's take. No one in the room during my peer review panel suggested not checking the proofs.
DeleteYou should suggest it.
DeleteWhen one formalises a proof in a proof assistant, it is still important to check that the definitions and theorem statements match what is intended or written down in pen and paper. At scale this is a social activity of maintaining good libraries if mathematics and TCS. I have been working towards this, but have a hard time convincing my fellow TCS folks that they actually need to care about the rigour of their proofs. Thus has to be a community effort, similar to mathlib.
ReplyDeleteI know a case where someone solved a conjecture AS STATED but it was nothing like what was INTENDED. The paper should have advertised itself as showing a flaw in the conjecture, not as solving the conjecture. AI may have this problem- solving conjectures as stated, not as intended.
ReplyDelete