5 ms·

What does AI for Math mean? People doing Math research that want to transition to AI research?

by upmind 2y ago

cvoss 2y ago
Broadly, as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process: 1) Identify a suitable language for use by both humans and computers for communication and manipulation of mathematical theorems and their proofs. 2) Employ both mathematicians and machine learning algorithms to generate interesting sentences in that language.
- upmind 2y ago
  That makes a lot more sense, thanks.
- riku_iki 2y ago
  > as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process I reviewed the doc, and it is just curated list of links on various projects (ML frameworks, proof assistant, some tutorials), and does not outline plan you described here. Or I missed something?..
  - cvoss 2y ago
    The first section, Textbooks and Survey Papers, begins with Formal Proof (this is where one identifies the suitable language for mathematics), followed by general Machine Learning references, and concluding with Machine Learning for Formal Proof. Other sections have similar divisions, though some go off into adjacent fields where one finds non-AI* algorithms for specific mathematical applications, such as automated symbolic calculus or SMT solving, to name just two. *Some people's terminology would classify such algorithms as "AI". I wouldn't, but they are nonetheless on-topic because you might invoke them to assist, focus, refine, or accelerate other techniques.
deleted 2y ago
[deleted]
benreesman 2y ago
I’m generally a bit of an LLM skeptic, at least as concerns extravagant claims around “AGI” or self-improvement of any of that nonsense. But there are activities where an inherently high-temperature assistant (e.g. some Instruct-inspired tune) are a great fit, and those are almost definitionally at the boundary of “objectively faithful” and “a bit stochastic”. I’ve never done any work in novel mathematics myself, but I’m a big fan of those who do, and any study of those who do paints a picture of roughly that boundary: those who are proficient can easily spot a falsehood but only with difficulty generate inspiration for a new idea. Of all the highly optimistic applications for 2024 LLMs, mathematics sounds pretty plausible?
- kevinventullo 2y ago
  FWIW as a former mathematician, I believe that if LLM’s can crack mathematics in the sense of say, solving the Riemann Hypothesis through chains of logical reasoning, then we’d be in the back half of reaching “AGI” in the sense of solving broad classes of general problems like drug discovery, or getting fusion to work, or even improving itself.
  - benreesman 2y ago
    Oh sure, I think that’s pretty uncontroversial. An LLM that can with any consistency start at “prove or disprove P = NP” and arrive at a proof is in some sense super-intelligence. Even the best funded boosters are making no such claims AFAIK, I think a much more reasonable and sober assertion might be like “they are useful to doing real mathematics”.
  - adroniser 2y ago
    The curious thing is if you can ever hit a snowball type point, because by proving theorems you are generating training data, and maybe you can get to a point where you effectively have limitless data.
  - quonn 2y ago
    Science needs experiments and those will not go faster because of AI. So why would fusion arrive any faster?
deleted 2y ago
[deleted]
fsmv 2y ago
Terry Tao has recently been exploring the computer proof writing language Lean and since you can mechanically check the validity of the proof it's perfectly valid to have an AI generate Lean code. If it's wrong Lean will give errors and if it's a valid proof it doesn't matter where it came from.

What does AI for Math mean? People doing Math research that want to transition to AI research?

by upmind 2y ago

What does AI for Math mean? People doing Math research that want to transition to AI research?

Broadly, as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process: 1) Identify a suitable language for use by both humans and computers for communication and manipulation of mathematical theorems and their proofs. 2) Employ both mathematicians and machine learning algorithms to generate interesting sentences in that language.

upmind 2y ago
That makes a lot more sense, thanks.
riku_iki 2y ago
> as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process I reviewed the doc, and it is just curated list of links on various projects (ML frameworks, proof assistant, some tutorials), and does not outline plan you described here. Or I missed something?..
- cvoss 2y ago
  The first section, Textbooks and Survey Papers, begins with Formal Proof (this is where one identifies the suitable language for mathematics), followed by general Machine Learning references, and concluding with Machine Learning for Formal Proof. Other sections have similar divisions, though some go off into adjacent fields where one finds non-AI* algorithms for specific mathematical applications, such as automated symbolic calculus or SMT solving, to name just two. *Some people's terminology would classify such algorithms as "AI". I wouldn't, but they are nonetheless on-topic because you might invoke them to assist, focus, refine, or accelerate other techniques.

deleted 2y ago

[deleted]

benreesman 2y ago

I’m generally a bit of an LLM skeptic, at least as concerns extravagant claims around “AGI” or self-improvement of any of that nonsense. But there are activities where an inherently high-temperature assistant (e.g. some Instruct-inspired tune) are a great fit, and those are almost definitionally at the boundary of “objectively faithful” and “a bit stochastic”. I’ve never done any work in novel mathematics myself, but I’m a big fan of those who do, and any study of those who do paints a picture of roughly that boundary: those who are proficient can easily spot a falsehood but only with difficulty generate inspiration for a new idea. Of all the highly optimistic applications for 2024 LLMs, mathematics sounds pretty plausible?

kevinventullo 2y ago
FWIW as a former mathematician, I believe that if LLM’s can crack mathematics in the sense of say, solving the Riemann Hypothesis through chains of logical reasoning, then we’d be in the back half of reaching “AGI” in the sense of solving broad classes of general problems like drug discovery, or getting fusion to work, or even improving itself.
- benreesman 2y ago
  Oh sure, I think that’s pretty uncontroversial. An LLM that can with any consistency start at “prove or disprove P = NP” and arrive at a proof is in some sense super-intelligence. Even the best funded boosters are making no such claims AFAIK, I think a much more reasonable and sober assertion might be like “they are useful to doing real mathematics”.
- adroniser 2y ago
  The curious thing is if you can ever hit a snowball type point, because by proving theorems you are generating training data, and maybe you can get to a point where you effectively have limitless data.
- quonn 2y ago
  Science needs experiments and those will not go faster because of AI. So why would fusion arrive any faster?

deleted 2y ago

[deleted]

fsmv 2y ago

Terry Tao has recently been exploring the computer proof writing language Lean and since you can mechanically check the validity of the proof it's perfectly valid to have an AI generate Lean code. If it's wrong Lean will give errors and if it's a valid proof it doesn't matter where it came from.