Re: https://lipn.info/@mevenlennonbertrand/116997917683191056
To riff on this a bit from a very different field at a very different scale, as a pretext to share an anecdote:
When I was a graduate student I spent a fair amount of time (an embarrassing amount of time) trying to get a computer to learn how to play Tic-Tac-Toe (naughts and crosses) by self play, given minimal help. Why? Because it turns out to be significantly harder than you might think based on the simplicity of the game, and I was curious why. It's not that hard in the grand scheme of things, but it's weirdly harder than you'd (well, I'd) expect (1). So, I went about coding up a Tic-Tac-Toe implementation that could play as quickly as possible, since gameplay would be the inner loop of a search algorithm, tested it some, and set a self-play-based search I was working on loose. Before too long my search was logging data that suggested it had found at least one optimal player. I was excited because I had opinions about how to use self-play to guide strategy search and it seemed like I might have some data supporting those opinions (calling them "hypotheses" would be giving my past self too much credit).
After quite a bit of testing, I discovered that my Tic-Tac-Toe implementation had a bug: in a small set of configurations of the board, my code would flag two in a row as a win instead of three in a row. My "optimal players" turned out to exploit this fact, choosing moves to drive the game into that set of configurations, then "winning" with two in a row. Oops. (2)
I noticed the problem because some of my discovered players were beating a minimax player during post hoc testing, which I knew to be impossible. I was able to sort out why because Tic-Tac-Toe is small enough to exhaustively test: you can enumerate the < 6,000 board configurations (3), run a function or strategy on all of them, and analyze the output in a reasonable amount of time and without too much trouble. I was able to spot by eye what was wrong.
One might ask: why didn't you have unit tests to do this sort of thing? Well, after that experience I did do more routine testing. However, speaking more generally now, there's an infinite regress when it comes to checking whether or not an implementation of a set of rules is faithful to the intention of that set of rules. Barring some kind of theoretical guarantee you'd need some other implementation of the rules to perform that sort of test. How can you be certain that implementation is comprehensive and also doesn't have a bug? You sometimes can't, practically speaking, and sometimes you can't theoretically speaking either. When the domain becomes large and complicated enough that both the above features about Tic-Tac-Toe I took advantage of---a sure indicator grounded in theory, and the ability to comprehensively and satisfactorily test---fail to hold, you're a bit adrift. (4)
I'm not very familiar with Lean, but I do know a bit about type theory, and modern type checkers tend to be Turing complete. Formal verification of a Turing complete programming language is not easy. I understand that practical type systems are designed to make type judgments of interest decidable, but that does not mean they're easy nor that the rules are easy to implement faithfully or test. It seems to me to be a tough problem, which is one of many reasons why I've taken the claims about LLMs doing this or that math thing with a big grain of salt. (5) I've expected to see the analog of my two-in-a-row "optimal" Tic-Tac-Toe players emerge to much fanfare for awhile now, and I expect to see many more.
#AI #LLM #FormalizedMath #math #Lean #ComputerScience #LearningBySelfPlay #SelfPlay #TicTacToe
(1) Donald Michie reported his MENACE system, which was a rudimentary form of reinforcement learning, could learn a decent game of Tic-Tac-Toe within a few hundred games. Christopher Rosin reported his coevolution-based Tic-Tac-Toe learner, a variant of learning by self play, required tens of billions of games to achieve less competence. Arthur Samuel's system learned master-level checkers by self play faster than this.
(2) Debugging a system by wrapping a search or optimization algorithm around it is an underappreciated technique I've used many times. It's a bit like fuzzing with an incentive to cause trouble.
(3) When I said "given minimal help", I meant it: I didn't give the players knowledge of the board symmetries.
(4) Personally I think it's incumbent on computer science professionals to flag when this is the case, since that's something we're educated to know (at least in principle).
(5) "Under the assumption that the implementation of system Y is correct, a human-written formalization of problem X in system Y produced output that a team of humans verified could be adapted into a proof of theorem Z" would grab fewer headlines than "AI proves Z", though.
To riff on this a bit from a very different field at a very different scale, as a pretext to share an anecdote:
When I was a graduate student I spent a fair amount of time (an embarrassing amount of time) trying to get a computer to learn how to play Tic-Tac-Toe (naughts and crosses) by self play, given minimal help. Why? Because it turns out to be significantly harder than you might think based on the simplicity of the game, and I was curious why. It's not that hard in the grand scheme of things, but it's weirdly harder than you'd (well, I'd) expect (1). So, I went about coding up a Tic-Tac-Toe implementation that could play as quickly as possible, since gameplay would be the inner loop of a search algorithm, tested it some, and set a self-play-based search I was working on loose. Before too long my search was logging data that suggested it had found at least one optimal player. I was excited because I had opinions about how to use self-play to guide strategy search and it seemed like I might have some data supporting those opinions (calling them "hypotheses" would be giving my past self too much credit).
After quite a bit of testing, I discovered that my Tic-Tac-Toe implementation had a bug: in a small set of configurations of the board, my code would flag two in a row as a win instead of three in a row. My "optimal players" turned out to exploit this fact, choosing moves to drive the game into that set of configurations, then "winning" with two in a row. Oops. (2)
I noticed the problem because some of my discovered players were beating a minimax player during post hoc testing, which I knew to be impossible. I was able to sort out why because Tic-Tac-Toe is small enough to exhaustively test: you can enumerate the < 6,000 board configurations (3), run a function or strategy on all of them, and analyze the output in a reasonable amount of time and without too much trouble. I was able to spot by eye what was wrong.
One might ask: why didn't you have unit tests to do this sort of thing? Well, after that experience I did do more routine testing. However, speaking more generally now, there's an infinite regress when it comes to checking whether or not an implementation of a set of rules is faithful to the intention of that set of rules. Barring some kind of theoretical guarantee you'd need some other implementation of the rules to perform that sort of test. How can you be certain that implementation is comprehensive and also doesn't have a bug? You sometimes can't, practically speaking, and sometimes you can't theoretically speaking either. When the domain becomes large and complicated enough that both the above features about Tic-Tac-Toe I took advantage of---a sure indicator grounded in theory, and the ability to comprehensively and satisfactorily test---fail to hold, you're a bit adrift. (4)
I'm not very familiar with Lean, but I do know a bit about type theory, and modern type checkers tend to be Turing complete. Formal verification of a Turing complete programming language is not easy. I understand that practical type systems are designed to make type judgments of interest decidable, but that does not mean they're easy nor that the rules are easy to implement faithfully or test. It seems to me to be a tough problem, which is one of many reasons why I've taken the claims about LLMs doing this or that math thing with a big grain of salt. (5) I've expected to see the analog of my two-in-a-row "optimal" Tic-Tac-Toe players emerge to much fanfare for awhile now, and I expect to see many more.
#AI #LLM #FormalizedMath #math #Lean #ComputerScience #LearningBySelfPlay #SelfPlay #TicTacToe
(1) Donald Michie reported his MENACE system, which was a rudimentary form of reinforcement learning, could learn a decent game of Tic-Tac-Toe within a few hundred games. Christopher Rosin reported his coevolution-based Tic-Tac-Toe learner, a variant of learning by self play, required tens of billions of games to achieve less competence. Arthur Samuel's system learned master-level checkers by self play faster than this.
(2) Debugging a system by wrapping a search or optimization algorithm around it is an underappreciated technique I've used many times. It's a bit like fuzzing with an incentive to cause trouble.
(3) When I said "given minimal help", I meant it: I didn't give the players knowledge of the board symmetries.
(4) Personally I think it's incumbent on computer science professionals to flag when this is the case, since that's something we're educated to know (at least in principle).
(5) "Under the assumption that the implementation of system Y is correct, a human-written formalization of problem X in system Y produced output that a team of humans verified could be adapted into a proof of theorem Z" would grab fewer headlines than "AI proves Z", though.
Edited 49d ago