4 ms·
> Are there any other interesting complete information games? How about axioms of logic as legal moves, and asking it to go from a set of axioms to open mathem
by 317070 9y ago
> Are there any other interesting complete information games?
How about axioms of logic as legal moves, and asking it to go from a set of axioms to open mathematical problems?
Or chemical procedures and components as moves, and asking it to tackle a disease with a known molecular structure?
It is not as straightforward as I make it sound, but these are complete information problems.
- seanwilson 9y ago> How about axioms of logic as legal moves, and asking it to go from a set of axioms to open mathematical problems? I'm not sure how you could train it against itself. The branching factor would be infinite as well so I don't know how you'd constrain the legal moves. For example, maybe rewriting (a * 2) to (a + a) or (a * 4 - a * 2) and so on for every theorem you know would be useful in a proof, plus you can invent your own theorems as intermediate steps.
- rhaps0dy 9y ago>How about axioms of logic as legal moves, and asking it to go from a set of axioms to open mathematical problems? >Or chemical procedures and components as moves, and asking it to tackle a disease with a known molecular structure? >It is not as straightforward as I make it sound, but these are complete information problems. However they are not adversarial games. Self-play only works for adversarial games. Also each mathematical problem is different and needs to be solved only once, and likewise for molecular structures. Additionally, they only need to be solved once, so there is no "gradient of skill" that we know to climb.
- fmap 9y agoTheorem proving in intuitionistic logic is a two-player game and maps perfectly to the kind of Monte-Carlo Tree Search that's employed here. Except that it is far more difficult than Chess/Go/etc., since the branching factor is essentially unbounded.
- seanwilson 9y agoCan you elaborate? How could you score how close you are to a solution and what would the second player be doing?
- fmap 9y agoConsider a formula made up of only conjunctions and disjunctions and true/false. The first player tries to prove the formula and gets to move at every disjunction and is allowed to select which side of the disjunction to prove. The second player tries to prevent the first player from finding a proof and gets to move at every conjunction, selecting a side of the conjunction to descend to. The final state here is an atomic proposition which is either true or false and determines which player won. You derive a value function from that in the same way as you do for Go or Chess. You can extend this idea to full first-order intuitionistic logic and probably also to higher-order logics, as well as many different modal logics. There are also formulations of classical logic as a single player game, but that doesn't seem to be very useful here.
- lukasLansky 9y agohttps://en.wikipedia.org/wiki/Game_semantics https://en.wikipedia.org/wiki/Game_semantics
- VikingCoder 9y agoI believe both of those have been done.
- CJefferson 9y agoUnfortunately the things AlphaZero can do is much more restrictive than that -- it needs a very small, fixed state of the world and set of possible moves. While chess if very complicated to play, the state can be represented by (at worst) an 8x8x6 boolean array (board, one of 6 possible pieces), for go a 17x17x2 boolean array. There is nothing similar for logic and and deep learning breaks down (in my experience) once you don't have that nice regular input space.