YouTuber: you can't say that AI isn't smart when it solved a math problem
-
YouTuber: you can't say that AI isn't smart when it solved a math problem
holy shit it guessed it's way through with a proof checker (LEAN) telling it "no, try again" an unlimited number of times
(this is known as directed search in The Literature and it's decades old)
Imagine if you got that treatment. Imagine taking an math exam you get infinite tries at. Would the fact that you eventually got one of questions right mean you're good at math? I want to actually claw my eyes out
-
YouTuber: you can't say that AI isn't smart when it solved a math problem
holy shit it guessed it's way through with a proof checker (LEAN) telling it "no, try again" an unlimited number of times
(this is known as directed search in The Literature and it's decades old)
Imagine if you got that treatment. Imagine taking an math exam you get infinite tries at. Would the fact that you eventually got one of questions right mean you're good at math? I want to actually claw my eyes out
@gildilinie reminds me of that scene in UHF where a blind guy makes a few moves on a Rubik's Cube, holds it up, and asks his companion "Is this it?" and the companion says "No", and repeats, ad infinitum
-
YouTuber: you can't say that AI isn't smart when it solved a math problem
holy shit it guessed it's way through with a proof checker (LEAN) telling it "no, try again" an unlimited number of times
(this is known as directed search in The Literature and it's decades old)
Imagine if you got that treatment. Imagine taking an math exam you get infinite tries at. Would the fact that you eventually got one of questions right mean you're good at math? I want to actually claw my eyes out
you can apply directed search to any problem with an unknown answer but where a guess is easy to check + a guesser that sometimes moves in the right direction. It's literally one step above brute force search in terms of sophistication
-
@gildilinie reminds me of that scene in UHF where a blind guy makes a few moves on a Rubik's Cube, holds it up, and asks his companion "Is this it?" and the companion says "No", and repeats, ad infinitum
@Mycroft yes that's how we got "AI solved 100 year old math problem" headlines
-
you can apply directed search to any problem with an unknown answer but where a guess is easy to check + a guesser that sometimes moves in the right direction. It's literally one step above brute force search in terms of sophistication
usually directed search isn't chosen unless nothing else is available because it takes a metric ass ton of compute. but that's what they have
-
@Mycroft yes that's how we got "AI solved 100 year old math problem" headlines
@gildilinie infinite monkeys on infinite typewriters producing so many scripts for Harniet by burning down finite rainforests
-
usually directed search isn't chosen unless nothing else is available because it takes a metric ass ton of compute. but that's what they have
People who go on YouTube to say "well it solved a math problem it's thinking" should all be forced to get a scarlet letter face tattoo that says "huckster"
like yes the technique works. Worked before chatbots too. the cost of using some trillion parameter model to do it would feed a small city forever
-
@gildilinie infinite monkeys on infinite typewriters producing so many scripts for Harniet by burning down finite rainforests
@Mycroft and fortinbras, knee deep in Danes, lived happily ever after
-
People who go on YouTube to say "well it solved a math problem it's thinking" should all be forced to get a scarlet letter face tattoo that says "huckster"
like yes the technique works. Worked before chatbots too. the cost of using some trillion parameter model to do it would feed a small city forever
the "smart" is the people who made LEAN and Rocq etc and programmed it to check if some random symbols sequence was a valid proof for whatever
-
the "smart" is the people who made LEAN and Rocq etc and programmed it to check if some random symbols sequence was a valid proof for whatever
anyway if you have an infinite supply of money time and compute, no morals, and you learn how to set up LEAN as a part of this loop... you could do it too. Might be cheaper to not do it with a trillion parameter neural network but... I guess misery and cost is no object
-
YouTuber: you can't say that AI isn't smart when it solved a math problem
holy shit it guessed it's way through with a proof checker (LEAN) telling it "no, try again" an unlimited number of times
(this is known as directed search in The Literature and it's decades old)
Imagine if you got that treatment. Imagine taking an math exam you get infinite tries at. Would the fact that you eventually got one of questions right mean you're good at math? I want to actually claw my eyes out
@gildilinie@beige.party Someone at work was talking about a vibe-coded library in a specialist discipline that a decade ago would have been most of a PhD dissertation. And he was right, those deliverables qualify.
But while he took that as a sign the AI tools were getting good, I interpreted it as meaning the PhD programs never had been good in the first place.
-
you can apply directed search to any problem with an unknown answer but where a guess is easy to check + a guesser that sometimes moves in the right direction. It's literally one step above brute force search in terms of sophistication
@gildilinie this also happens to be true of security issues. anyway, AFL++ is a real woman and we're getting married soon
-
YouTuber: you can't say that AI isn't smart when it solved a math problem
holy shit it guessed it's way through with a proof checker (LEAN) telling it "no, try again" an unlimited number of times
(this is known as directed search in The Literature and it's decades old)
Imagine if you got that treatment. Imagine taking an math exam you get infinite tries at. Would the fact that you eventually got one of questions right mean you're good at math? I want to actually claw my eyes out
@gildilinie Yeah, unfortunately "AI" is so ingrained into people's minds. LLMs are autocompletion on speed and can be very useful with the right settings.
But they aren't and never will be "intelligent".
-
J jwcph@helvede.net shared this topic
