4 ms·

>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 mo

>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 ago
Theorem 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 ago
  Can you elaborate? How could you score how close you are to a solution and what would the second player be doing?
  - fmap 9y ago
    Consider 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 ago
https://en.wikipedia.org/wiki/Game_semantics https://en.wikipedia.org/wiki/Game_semantics

fmap 9y ago

Theorem 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 ago
Can you elaborate? How could you score how close you are to a solution and what would the second player be doing?
- fmap 9y ago
  Consider 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 ago

https://en.wikipedia.org/wiki/Game_semantics https://en.wikipedia.org/wiki/Game_semantics