Live data from Hacker News

Richard Sutton and Andrew Barto Win 2024 Turing Award

awards.acm.org

41–50 of 119 posts

Re: Richard Sutton and Andrew Barto Win 2024 Turing Award

#41
post #12

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.

What kind of company needs formal verification? Real time systems?

Re: Richard Sutton and Andrew Barto Win 2024 Turing Award

#42

Earlier 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?

Real time / embedded / etc for money handling, healthcare, aviation/transport... And 'needs' is a loaded term; the biggest $ contributors to formal verification progress are blockchain companies these days while a lot of critical systems are badly written, outsourced things that barely have tests.

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

#43

Good 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?

that was “bitter lesson” in action.

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

#44
post #13

Amazing 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.

https://nationalpost.com/news/canada/ai-guru-rich-sutton-dee...

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

#48
post #16
post #13

Amazing 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.

At his level it is much more than just being able to do what he wants, it’s about attracting resources and talent to accomplish his goals.

From that perspective location still matters if you want to maximise impact

Re: Richard Sutton and Andrew Barto Win 2024 Turing Award

#49
Huge congratulations to Andrew Barto and Richard Sutton on the well-deserved Turing Award! as a student, their textbook Reinforcement Learning: An Introduction was my gateway into the field. I still remembered that how Chapter 6 on ‘Temporal Difference Learning’ fundamentally reshaped the way I thought about sequential decision-making.

a timeless classic that I still highly recommend reading today!

Post reply on HN