Lemminary@lemmy.world
on 16 May 2024 06:41
collapse
Ok
windie@lemmy.world
on 16 May 2024 06:13
nextcollapse
This might be a worthy application.
amzd@kbin.social
on 16 May 2024 07:48
nextcollapse
AI is insanely bad at distinguishing fact from hallucination, which seems like a terrible match for math
blargerer@kbin.social
on 16 May 2024 08:38
nextcollapse
I haven't read this article, but the one place machine learning is really really good, is narrowing down a really big solution space where false negatives and false positives are cheap. Frankly, I'm not sure how you'd go about training an AI to solve math problems, but if you could figure that out, it sounds roughly like it would fit the bill. You just need human verification as the final step, with the understanding that humans will rule out like 90% of the tries, but if you only need one success that's fine. As a real world example machine learning is routinely used in astronomy to narrow down candidate stars or galaxies from potentially millions of options to like 200 that can then undergo human review.
magic_lobster_party@kbin.run
on 16 May 2024 11:04
nextcollapse
The article is about using computers to discover new conjectures (mathematical statements that are not yet known to be true or false). The conjecture can be then later be formally proven (or disproven) by humans.
Sounds like a good match for me. Formulating conjectures is about finding an interesting pattern and argue that this pattern holds true. Computers are getting increasingly better at pattern matching, so why not use them?
Title is a bit clickbaity by calling it AI.
technocrit@lemmy.dbzer0.com
on 16 May 2024 15:16
collapse
Title is a bit clickbaity by calling it AI.
That’s literally every article about “AI”.
… the London Institute for Mathematical Sciences, of which I am director
There’s the reason. Self-promotion.
Even_Adder@lemmy.dbzer0.com
on 16 May 2024 15:10
collapse
AI isn’t just LLMs.
dragontamer@lemmy.world
on 16 May 2024 15:24
collapse
No one is talking about automated theorem provers (see 4 coloring theorem) or symbolic solvers (see Mathematica). These tools already revolutionized math decades ago.
The only thing that came out in the past year or two are LLMs. Which is clearly overhyped bullshit.
Even_Adder@lemmy.dbzer0.com
on 16 May 2024 15:29
collapse
The article doesn’t mention LLMs, and many ML related things came out in the last year or two that aren’t LLMs.
anton@lemmy.blahaj.zone
on 16 May 2024 08:21
nextcollapse
The absence of coincidence
Look up the strong law of small numbers.
Also, one of their examples of AI was an exhaustive search.
EarthShipTechIntern@lemm.ee
on 16 May 2024 08:38
nextcollapse
Set to be revolutionized by AI because AI can’t do math.
Says my brother, a Math Professor that works with people trying to develop AI
That’s because ChatGPT and the likes use machine learning to calculate odds of word combinations that make up a plausible sentence in a given context. There are scientific studies that postulate we’ll never have enough data to train those models properly, not to mention exponential energy consumption required. But this is not the only application of this technology.
The article isn’t about automatic proofs, but it’d be interesting to see a LLM that can write formal proofs in Coq/Lean/whatever and call external computer algebra systems like SageMath or Mathematica.
CapeWearingAeroplane@sopuli.xyz
on 16 May 2024 21:06
collapse
I was thinking something similar: If you have the computer write in a formal language, designed in such a way that it is impossible to make an incorrect statement, I guess it could be possible to get somewhere with this
threaded - newest
No
Are you saying “No… let’s not advance mathematics”? Or… “No, let’s not advance mathematics using AI”?
Yes
I was saying boourns
No
Ok
This might be a worthy application.
AI is insanely bad at distinguishing fact from hallucination, which seems like a terrible match for math
I haven't read this article, but the one place machine learning is really really good, is narrowing down a really big solution space where false negatives and false positives are cheap. Frankly, I'm not sure how you'd go about training an AI to solve math problems, but if you could figure that out, it sounds roughly like it would fit the bill. You just need human verification as the final step, with the understanding that humans will rule out like 90% of the tries, but if you only need one success that's fine. As a real world example machine learning is routinely used in astronomy to narrow down candidate stars or galaxies from potentially millions of options to like 200 that can then undergo human review.
The article is about using computers to discover new conjectures (mathematical statements that are not yet known to be true or false). The conjecture can be then later be formally proven (or disproven) by humans.
Sounds like a good match for me. Formulating conjectures is about finding an interesting pattern and argue that this pattern holds true. Computers are getting increasingly better at pattern matching, so why not use them?
Title is a bit clickbaity by calling it AI.
That’s literally every article about “AI”.
There’s the reason. Self-promotion.
AI isn’t just LLMs.
No one is talking about automated theorem provers (see 4 coloring theorem) or symbolic solvers (see Mathematica). These tools already revolutionized math decades ago.
The only thing that came out in the past year or two are LLMs. Which is clearly overhyped bullshit.
The article doesn’t mention LLMs, and many ML related things came out in the last year or two that aren’t LLMs.
Look up the strong law of small numbers.
Also, one of their examples of AI was an exhaustive search.
Set to be revolutionized by AI because AI can’t do math.
Says my brother, a Math Professor that works with people trying to develop AI
AI is math, statistics specifically.
.
AI can’t count the number of letters in a word
That’s because ChatGPT and the likes use machine learning to calculate odds of word combinations that make up a plausible sentence in a given context. There are scientific studies that postulate we’ll never have enough data to train those models properly, not to mention exponential energy consumption required. But this is not the only application of this technology.
The article isn’t about automatic proofs, but it’d be interesting to see a LLM that can write formal proofs in Coq/Lean/whatever and call external computer algebra systems like SageMath or Mathematica.
I was thinking something similar: If you have the computer write in a formal language, designed in such a way that it is impossible to make an incorrect statement, I guess it could be possible to get somewhere with this