+- Ludii Forum (https://ludii.games/forums)
+-- Forum: Suggestions (https://ludii.games/forums/forumdisplay.php?fid=10)
+--- Forum: Ludii Features / Services (https://ludii.games/forums/forumdisplay.php?fid=11)
+--- Thread: An AI based on Positional Theorem Proving (/showthread.php?tid=401)
An AI based on Positional Theorem Proving - aindilis - 01-29-2021
Hi,
I am very exited to discover this project!
I haven't yet read much of the documentation, so please only if possible answer my most salient questions which haven't been already documented unless the answers are obscure.
The Ludii language looks to be extremely expressive/complex! It should therefore be possible to more elegantly state properties of games, which should speed up theorem proving, which I believe can be shown to dominate mere search in some contexts. A quick search of this thread for "theorem" had no results. Are there efforts to prove positional properties / trajectory invariants? (e.g. for instance with chess - opposite colored bishops can not capture, this pawn is overprotected, etc). I am working on a project to translate textbooks on Chess and Go into Prolog predicates ( https://github.com/aindilis/chap2/blob/master/analysis.pl ) ( https://github.com/aindilis/nlu-mf ) for use in positional theorem proving. My goal there is to 1) extract libraries of strategies, 2) ground Natural Language Understanding in a concrete domain for use in speeding up Rapid Knowledge Formation (RKF), 3) extract strategies that can be transferred for use with my Free Life Planner project ( https://github.com/aindilis/free-life-planner ).
I haven't read the grammar definition document yet, but it looks to be based on s-expressions. Is it Knowledge Interchange Format, First Order Logic, or something similar? Are the Ludii language constants defined in terms of a smaller set of primitives somewhere, preferably in a logic? Or is it defined programmatically in Java? Are there translations to or from Game Description Language? How does it compare to leading General Game Playing solvers? How does it compare as a framework to other GGP systems like Zillions of Games? Are there efforts to solve games, such as with Gamer: https://core.ac.uk/download/pdf/297278922.pdf
I have a stub project called Ender (named after the character from the novel Ender's Game who supposedly "wins all the games."). I intend to now let Ludii/Polygames do most of the heavy lifting. Would theorems (of positional properties) make useful features for Polygames?
I lost my first draft of the post, so I'm just going to post this now before I lose it again. More later.
Thank you,
Andrew
RE: An AI based on Positional Theorem Proving - cambolbro - 01-30-2021
Hi Andrew,
Thanks for your interest in the project! I'll try to answer as many of your questions as I can.
Quote:Are there efforts to prove positional properties / trajectory invariants?
(e.g. for instance with chess - opposite colored bishops can not capture, this pawn is overprotected, etc).
Not as such, though Ludii would provide a framework for performing such analyses. The focus of our research is more on identifying "good" rule sets in the general case.
Quote:My goal there is to 1) extract libraries of strategies, 2) ground Natural Language Understanding in a concrete domain for use in speeding up Rapid Knowledge Formation (RKF), 3) extract strategies that can be transferred for use with my Free Life Planner project ( https://github.com/aindilis/free-life-planner ).
Having said that, one aspect of the Digital Ludeme Project (that Ludii is being developed for) is to detect simple strategies in games by identifying features in the form of geometric piece patterns that our MCTS agents can use to improve playing strength. The idea is detect such useful features, transfer them between games to accelerate learning, then explain them to users in plain English. I'm also hoping that such analysis could be give a simple indicator of strategic depth in a rule set as another indicator of game quality.
Quote:I haven't read the grammar definition document yet, but it looks to be based on s-expressions.
Is it Knowledge Interchange Format, First Order Logic, or something similar?
Simple LISP-like s-expression in plain text.
Quote:Are the Ludii language constants defined in terms of a smaller set of primitives somewhere, preferably in a logic?
Or is it defined programmatically in Java?
The latter. Each token in the grammar corresponds to a Java class in our code base that implements a Ludeme interface. The structure of the grammar exactly matches the folder structure in our Core/src/game area.
Quote:Are there translations to or from Game Description Language?
Not yet. We have discussed translating both ways and there are complications with each. But it's something we'd like to get to towards the end of the project.
Quote:How does it compare to leading General Game Playing solvers?
Ludii doesn't solve games as such (except simple games whose trees are solved in the course of move planning). The research emphasis in the project is not solve games or derive optimal agents or strategies so much as to gain insight into what humans find interesting in games and identifying rule sets that exhibit those properties.
Quote:How does it compare as a framework to other GGP systems like Zillions of Games?
Ludii plays a similar role to Zillions as a tool for game designers to explore rule sets and evaluate them. Zillions is focussed more in Chess-like games; they are easy to implement in ZRF format and the in-built AI agents are highly optimised for them and very good at them. But once you deviate away from that style of game things are different; implementing my 3D marble-stacking connection game Akron in ZRF took many months and required writing a game-specific DLL for even the simplest AI support.
Zillions also focusses on the graphics, audio, etc. (they are defined among the game logic) and is aimed at providing an enjoyable playing experience more than Ludii is. Ludii strips the UI down to the bare basics, deliberately keeping things clean, to focus on the underlying gameplay. We deliberately separate the game logic (in the "game/match" section of each .lud) from the UI (in the "metadata" section of each .lud).
Ludii is more general, supports a wider range of games and game types, and the grammar is aimed at capturing important game concepts more clearly. The Zillions Language provides around 130 keywords while the Ludii grammar provides more that 10 times that many: 600+ ludeme classes, 600+ constant attributes used as arguments to them, and hundreds of "subludeme" classes that implement specific applications of "super ludemes", e.g. (count Sites ...), (count Pieces ...), etc. have corresponding CountPieces(), CountPieces(), etc. classes that are not seen in the grammar -- the super ludeme notation simplifies the grammar to hide them -- but are implicitly invoked when the super ludeme with the appropriate parameter is called.
The Ludii AIs aim at playing a wider range of games sensibly, rather than specialising in any particular type of game.
Encapsulating important game concepts into single keywords is a significant benefit over GDL when it comes to evolving rule sets.
Quote:Are there efforts to solve games, such as with Gamer: https://core.ac.uk/download/pdf/297278922.pdf
No, though I did run a student project last year that looked at properties of small (i.e. fully solvable) games as a first step to seeing how full game tree analysis might help identify flaws/strengths in small games.
Quote:Would theorems (of positional properties) make useful features for Polygames?
I'm not sure. My PhD student Dennis Soemers has done some work with Polygames so could perhaps answer that.
If you're interested in using Ludii to explore these questions we'd be more than happy to help!
Regards,
Cameron
RE: An AI based on Positional Theorem Proving - DennisSoemers - 01-31-2021
Quote:Would theorems (of positional properties) make useful features for Polygames?
In principle, I'd be inclined to say yes. If you can obtain reliable, accurate additional information about a game state, which can be relevant for the decision-making process of a game-playing agent, then providing that information as additional inputs to a neural network would likely allow it to learn more rapidly than if it had to automatically discover that knowledge through training with more raw inputs.
The main issue I see is that I would expect automated theorem proving based on Ludii's game descriptions to be rather difficult, much more so than with a game description language that is already logic-based like GDL. As Cameron already mentioned in the post above, the semantics of every single token that can be used in a game description file for Ludii are defined just by the corresponding Java code; the semantics are not defined in terms of logic-based propositions. I suppose that somewhere deep down every piece of Java could would have clear, strict semantics... but this is not readily and explicitly available in a logic-based format, and I imagine it would be extremely complicated to get it into such a form. Maybe I'm missing something though, this is not my area of expertise.