Earlier quoted context omitted.
AI assisted theorem provers will go a bit in that direction. You may not know exactly how they managed to construct a proof, but you can examine that proof in detail and verify its correctness.
Yes, I have a small team of (me being 1/3) doing formal verification in my company and we do this and it doesn't actually matter if how the AI got there; we can mathematically say it's correct which is what matters. We do (and did) program synthesis and proofs but this is all very far from doing anything serious at scale.
Richard Sutton and Andrew Barto Win 2024 Turing Award
41–50 of 119 posts
Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#42Earlier quoted context omitted.
Yes, I have a small team of (me being 1/3) doing formal verification in my company and we do this and it doesn't actually matter if how the AI got there; we can mathematically say it's correct which is what matters. We do (and did) program synthesis and proofs but this is all very far from doing anything serious at scale.
What kind of company needs formal verification? Real time systems?
My worst fear, which is happening because it works-ish, is vague/fuzzy systems being the software because it's so like humans and we don't have anything else. It's a terrible idea, but of course we are in a hurry.
Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#43Good time to re-read The Bitter Lesson: https://www.cs.utexas.edu/~eunsol/courses/data/bitter_lesson...
The Bitter Lesson seems to be generally accepted knowledge in the field. Wouldn't that make DeepSeek R1 even more of a breakthrough?
for example there are clever ways of rewarding all the steps of a reasoning process to train a network to “think”. but deepseek found these don’t work as well as much simpler yes/no feedback on examples of reasoning.
Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#44Amazing that Sutton (American) chooses to live in Edmonton, AB rather than USA. Shows he has integrity and is not a careerist focused on prestige and money above all else.
He gave up his US citizenship years ago but he explains some of the reasons why he left. I'll also say that the AI research coming out of Canada is pretty great as well so I think it makes sense to do research there.
Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#45Their book "Introduction to Reinforcement Learning" is one of the most accessible texts in the AI/ML field, highly recommend reading it.
Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#46Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#47Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#48Amazing that Sutton (American) chooses to live in Edmonton, AB rather than USA. Shows he has integrity and is not a careerist focused on prestige and money above all else.
Keen is a fully remote outfit, so he can work wherever. It's pretty likely that his reputation would open that door for him no matter where he goes.
From that perspective location still matters if you want to maximise impact
Re: Richard Sutton and Andrew Barto Win 2024 Turing Award
#49a timeless classic that I still highly recommend reading today!