5 ms·

The IDP Knowledge Base System

marginalia_nu 3y ago
I've read the entire landing page and I'm still not sure what IDP is or does. Which, to be fair, is a common failure pattern with many landing pages.
- anentropic 3y ago
  looks potentially interesting but a lot of it is kind of baffling, assumes a lot of familiarity with fairly esoteric topic, not clear where to start the tutorial page https://www.idp-z3.be/tutorial.html https://www.idp-z3.be/tutorial.html is a bit more enlightening as is https://interactive-idp.gitlab.io/ https://interactive-idp.gitlab.io/ learning material but I didn't find those first, I found the docs first (via the four "learn more" links on the landing page) and I don't think they are the best starting point https://docs.idp-z3.be/en/latest/introduction.html https://docs.idp-z3.be/en/latest/introduction.html > IDP-Z3 can be installed using the python package ecosystem. > install python 3, with pip3, making sure that python3 is in the PATH. > use git to clone https://gitlab.com/krr/IDP-Z3 https://gitlab.com/krr/IDP-Z3 to a directory on your machine > (For Linux and MacOS) open a terminal in that directory and run the following command First thought is... why isn't it published to PyPI? But then elsewhere https://docs.idp-z3.be/en/latest/IDP-Z3.html https://docs.idp-z3.be/en/latest/IDP-Z3.html > the idp_engine package available on Pypi. And looking in the git repo it seems like this is the same package published as https://pypi.org/project/idp-engine/ https://pypi.org/project/idp-engine/ Why not just say "pip install idp-engine"...?
  - pcarbonn 3y ago
    Thanks for the feedback. We'll see how we can improve the communication. Quick response: with pypi, you can only install the reasoning engine. By cloning the repository, you get the full suite of tools, including the "interactive consultant".
    - anentropic 3y ago
      I see... I think it could probably be evolved so that they can be pip installed too. e.g. instead of git clone and `poetry run python3 main.py` maybe your pip package could provide its own cli frontend for running the server.
  - crabbone 3y ago
    > Why not just say "pip install idp-engine"...? (I have nothing to do with IDP-Z3) This is the general pattern: * If you are a developer: get sources and work on sources, because, probably, you want to add to them or modify them etc. Part of this experience may be creating a package and installing it with pip or some other package installation program, but it's not usually what other developers (contributors) would be working on. * If you are a user: use the supported package manager to obtain the package and use it through documented interface. I'm honestly not sure if this is why or how these instructions came to be, but this is a fairly common thing to do, so, w/o looking, I'd guess this is what it is.
YoshiRulz 3y ago
I read through the syntax tutorial, and based on that alone I'm guessing this thing would be a huge pain to work with. The operators `=<`, `<=`, `>=`, and `=>` are easily confusable/typo-able, and I have to imagine the for-all operator is `!` only because someone had already decided to use `?` for there-exists, since who in their right mind would use a `!` prefix to mean anything other than boolean negation?
lucifer153 3y ago
It seems it has a lot in common with Lamport's TLA+, can someone compare?
- pcarbonn 3y ago
  Hi, I'm one of the main devs. TLA+ is useful to prove properties of programs. By contrast, IDP-Z3 is a reasoning engine that can be used as a module in a program. It is closer to a constraint solver, but offers more functionality than a traditional CSP solver. For example, it can compute what are relevant questions, given some inputs. This is useful to build "interactive consultants". For example, you give IDP-Z3 the formula that links a tax-free amount, a tax rate and a tax-included amount, and the values of any two of its parameters, and it will compute the missing parameter. You do not need to write 3 different formula, one for each case. If you give him only one parameter, it will say that the other two parameters are relevant.
  - anonzzzies 3y ago
    So it's layer on top of the z3-solver right? That's a way to see it?
    - pcarbonn 3y ago
      Yes. It uses a more convenient language than SMT-Lib to express "knowledge", and offers more functionality.
ansible 3y ago
I'm glad to see the design of the knowledge base language is aware of context (here called a domain). This is better than other systems, like what is used to parse / dump data from Wikipedia, where the context is basically "the real world right now". However, it doesn't seem like they wanted systems to be able to use and switch between domains easily, nor be able to backtrack (where you have inferred some knowledge, and you are trying to figure out what domain(s) you should be operating inside). Contextual reasoning is very important for many situations, because time is one of the most important contexts. You can have a fact like "the iPhone is the best selling phone". This fact is true or false based on the context. It is definitely false in the real world year 2006 and before, because the first iPhone was not released yet. While the fact may be true right now in a global context, if we are talking about a specific country or region, it may be false. For example, I would expect that satellite-capable phones may be more popular in a highly remote (non-urban) country or region.
- TrueDuality 3y ago
  I really want to see an open knowledge base project tackle exactly what you're describing. Cyc has a pretty solid foundation for accomplishing this using what they call microtheories (personally a weird term to me). It's a great step in the right direction but its a closed ecosystem with a huge amount of cognitive overhead to do anything against. A lot of other projects seem to do better with the ingestion and updating of information (albeit with less automated tooling). I've been refreshing myself on ontology design and knowledge representation lately. I'm kind of surprised that is hasn't moved very much in the last two decades. I'm guessing we're about to hit an inflection point there as it becomes a cool topic with the current AI trends.
  - ansible 3y ago
    Formal knowledge representation and any sort of formal reasoning is not the way the industry is going right now with LLMs though. It occurs to me that if we want LLMs to be able to reason better, we may need to write texts that explicitly embody the reasoning we desire, and not just use a bunch of books or whatever scraped from the Internet.
melagonster 3y ago
This looks beautiful. hope I have chances to try it.

I've read the entire landing page and I'm still not sure what IDP is or does. Which, to be fair, is a common failure pattern with many landing pages.

anentropic 3y ago
looks potentially interesting but a lot of it is kind of baffling, assumes a lot of familiarity with fairly esoteric topic, not clear where to start the tutorial page https://www.idp-z3.be/tutorial.html https://www.idp-z3.be/tutorial.html is a bit more enlightening as is https://interactive-idp.gitlab.io/ https://interactive-idp.gitlab.io/ learning material but I didn't find those first, I found the docs first (via the four "learn more" links on the landing page) and I don't think they are the best starting point https://docs.idp-z3.be/en/latest/introduction.html https://docs.idp-z3.be/en/latest/introduction.html > IDP-Z3 can be installed using the python package ecosystem. > install python 3, with pip3, making sure that python3 is in the PATH. > use git to clone https://gitlab.com/krr/IDP-Z3 https://gitlab.com/krr/IDP-Z3 to a directory on your machine > (For Linux and MacOS) open a terminal in that directory and run the following command First thought is... why isn't it published to PyPI? But then elsewhere https://docs.idp-z3.be/en/latest/IDP-Z3.html https://docs.idp-z3.be/en/latest/IDP-Z3.html > the idp_engine package available on Pypi. And looking in the git repo it seems like this is the same package published as https://pypi.org/project/idp-engine/ https://pypi.org/project/idp-engine/ Why not just say "pip install idp-engine"...?
- pcarbonn 3y ago
  Thanks for the feedback. We'll see how we can improve the communication. Quick response: with pypi, you can only install the reasoning engine. By cloning the repository, you get the full suite of tools, including the "interactive consultant".
  - anentropic 3y ago
    I see... I think it could probably be evolved so that they can be pip installed too. e.g. instead of git clone and `poetry run python3 main.py` maybe your pip package could provide its own cli frontend for running the server.
- crabbone 3y ago
  > Why not just say "pip install idp-engine"...? (I have nothing to do with IDP-Z3) This is the general pattern: * If you are a developer: get sources and work on sources, because, probably, you want to add to them or modify them etc. Part of this experience may be creating a package and installing it with pip or some other package installation program, but it's not usually what other developers (contributors) would be working on. * If you are a user: use the supported package manager to obtain the package and use it through documented interface. I'm honestly not sure if this is why or how these instructions came to be, but this is a fairly common thing to do, so, w/o looking, I'd guess this is what it is.

YoshiRulz 3y ago

I read through the syntax tutorial, and based on that alone I'm guessing this thing would be a huge pain to work with. The operators `=<`, `<=`, `>=`, and `=>` are easily confusable/typo-able, and I have to imagine the for-all operator is `!` only because someone had already decided to use `?` for there-exists, since who in their right mind would use a `!` prefix to mean anything other than boolean negation?

lucifer153 3y ago

It seems it has a lot in common with Lamport's TLA+, can someone compare?

pcarbonn 3y ago
Hi, I'm one of the main devs. TLA+ is useful to prove properties of programs. By contrast, IDP-Z3 is a reasoning engine that can be used as a module in a program. It is closer to a constraint solver, but offers more functionality than a traditional CSP solver. For example, it can compute what are relevant questions, given some inputs. This is useful to build "interactive consultants". For example, you give IDP-Z3 the formula that links a tax-free amount, a tax rate and a tax-included amount, and the values of any two of its parameters, and it will compute the missing parameter. You do not need to write 3 different formula, one for each case. If you give him only one parameter, it will say that the other two parameters are relevant.
- anonzzzies 3y ago
  So it's layer on top of the z3-solver right? That's a way to see it?
  - pcarbonn 3y ago
    Yes. It uses a more convenient language than SMT-Lib to express "knowledge", and offers more functionality.

ansible 3y ago

I'm glad to see the design of the knowledge base language is aware of context (here called a domain). This is better than other systems, like what is used to parse / dump data from Wikipedia, where the context is basically "the real world right now". However, it doesn't seem like they wanted systems to be able to use and switch between domains easily, nor be able to backtrack (where you have inferred some knowledge, and you are trying to figure out what domain(s) you should be operating inside). Contextual reasoning is very important for many situations, because time is one of the most important contexts. You can have a fact like "the iPhone is the best selling phone". This fact is true or false based on the context. It is definitely false in the real world year 2006 and before, because the first iPhone was not released yet. While the fact may be true right now in a global context, if we are talking about a specific country or region, it may be false. For example, I would expect that satellite-capable phones may be more popular in a highly remote (non-urban) country or region.

TrueDuality 3y ago
I really want to see an open knowledge base project tackle exactly what you're describing. Cyc has a pretty solid foundation for accomplishing this using what they call microtheories (personally a weird term to me). It's a great step in the right direction but its a closed ecosystem with a huge amount of cognitive overhead to do anything against. A lot of other projects seem to do better with the ingestion and updating of information (albeit with less automated tooling). I've been refreshing myself on ontology design and knowledge representation lately. I'm kind of surprised that is hasn't moved very much in the last two decades. I'm guessing we're about to hit an inflection point there as it becomes a cool topic with the current AI trends.
- ansible 3y ago
  Formal knowledge representation and any sort of formal reasoning is not the way the industry is going right now with LLMs though. It occurs to me that if we want LLMs to be able to reason better, we may need to write texts that explicitly embody the reasoning we desire, and not just use a bunch of books or whatever scraped from the Internet.

melagonster 3y ago

This looks beautiful. hope I have chances to try it.