You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Ben Sprott (Jun 21 2021 at 21:11):Can we start a list of companies which are doing AI and using Category Theory?
Spencer Breiner (Jun 21 2021 at 22:14):Probably depends on your definition of AI, but...
Spencer Breiner (Jun 21 2021 at 22:15):Conexus.ai (formerly Categorical Informatics)
Spencer Breiner (Jun 21 2021 at 22:15): Spencer Breiner (Jun 21 2021 at 22:16): Spencer Breiner (Jun 21 2021 at 22:18):Siemens (arXiv paper)
Spencer Breiner (Jun 21 2021 at 22:19): John Baez (Jun 21 2021 at 22:22):Does Statebox claim to do AI using category theory? I thought they just used Petri nets to design industrial processes.
Does Rchain claim to do AI using category theory?
Spencer Breiner (Jun 21 2021 at 22:23):Metron, Inc (arXiv, note: self-promotion)
John Baez (Jun 21 2021 at 22:23):Wow, now everyone is doing AI using category theory. :upside_down:
Fabrizio Genovese (Jun 21 2021 at 22:24):John Baez said:
Does Statebox claim to do AI? I thought they just used Petri nets to design industrial processes.
We don't do AI directly as of now, but we plan to do some for process mining
Fabrizio Genovese (Jun 21 2021 at 22:24):Also, RChain is a dead company unfortunately.
Spencer Breiner (Jun 21 2021 at 22:24):What counts? I've heard Fabrizio describe their work as "formally verified orchestration" (I think). I'd consider formal verification to be AI (which I take to be broader than ML)
Fabrizio Genovese (Jun 21 2021 at 22:25):Oh
Fabrizio Genovese (Jun 21 2021 at 22:25):then yes, we do lol
John Baez (Jun 21 2021 at 22:27):I think one could create a fairly short list of companies doing anything with category theory.
John Baez (Jun 21 2021 at 22:27):(If I'm wrong I'd be delighted.)
Spencer Breiner (Jun 21 2021 at 22:32):Fabrizio Genovese said:
Also, RChain is a dead company unfortunately.
I thought I had the wrong name, but rholang rang the right bell in my head. I guess this is what I was looking for:
Pyrofex
Georgios Bakirtzis (Jun 21 2021 at 22:32):Spencer Breiner said:
What counts? I've heard Fabrizio describe their work as "formally verified orchestration" (I think). I'd consider formal verification to be AI (which I take to be broader than ML)
I think we can have a discussion on this and agree on this us two but that is not how most people do AI. I would claim none of these companies do any "learning" in the modern sense.
Spencer Breiner (Jun 21 2021 at 22:36):I'd agree that "machine learning" is more of a stretch than "artificial intelligence". The latter has expert systems/formal verification baked in from earlier usage.
John Baez (Jun 21 2021 at 22:36):Spencer Breiner said:
Fabrizio Genovese said:
Also, RChain is a dead company unfortunately.
I thought I had the wrong name, but rholang rang the right bell in my head. I guess this is what I was looking for:
Pyrofex
I'm not quite sure of the situation, but I think "dead" is an exaggeration.
My former student @Mike Stay was running Pyrofex and working with Greg Meredith who runs RChain. Roughly a year or two ago, RChain lost a lot of money and trimmed back its operations. Pyrofex ran into trouble because a company they were working with failed to deliver their product on time.
John Baez (Jun 21 2021 at 22:42):However, Mike Stay is still working with Greg Meredith and my student @Christian Williams on ideas connected to category theory and computer science.
John Baez (Jun 21 2021 at 22:44):For example Mike and Christian came out with a paper on native type theory, which we've been discussing here... and it uses the -calculus, which is one of Greg Meredith's things.
Mike Stay (Jun 21 2021 at 22:54):I had thought about leaving, but we got a big contract and then some investment funding, so I'm still at Pyrofex. And RChain is still quite active. They launched main net last year. If you live outside the US, you can buy Rev on a couple of exchanges. But neither company is doing AI stuff.
Ben Sprott (Jun 22 2021 at 15:22):Thanks everyone for this. Does anyone have information about what they are doing at OiCOS expecially in terms of their use of CT?
Jules Hedges (Jun 22 2021 at 15:49):Ben Sprott said:
Thanks everyone for this. Does anyone have information about what they are doing at OiCOS expecially in terms of their use of CT?
It's quite a while since I talked with Viktor, but as far as I know he's not using any explicit category theory
Jules Hedges (Jun 22 2021 at 15:52):Spencer Breiner said:
What counts? I've heard Fabrizio describe their work as "formally verified orchestration" (I think). I'd consider formal verification to be AI (which I take to be broader than ML)
Going to definitely disagree with this. AI is a massive and broad subject - probably the single biggest subfield of computer science - but formal verification is not AI, nor is probably anything that any of these companies are doing
Jules Hedges (Jun 22 2021 at 15:54):Obviously the boundaries are blurry. All kinds of automated logical inference was once considered AI, so in that sense for example SAT and SMT solving would be AI, but as far as I know they're no longer used for anything that's recognisably AI
John Baez (Jun 22 2021 at 19:26):Okay, here's a question: are there any companies using category theory to do AI - in some sense that most of us would agree is really AI?
The name "conexus.ai" suggests AI, but if you go the webpage Spencer linked to, they don't seem to be doing AI and they're not calling themselves "conexus.ai". They seem to be doing databases, despite a line about "complex reasoning" (which may just mean that you can do sophisticated queries).
Spencer Breiner (Jun 22 2021 at 20:28):Jules Hedges said:
Going to definitely disagree with this. AI is a massive and broad subject - probably the single biggest subfield of computer science - but formal verification is not AI, nor is probably anything that any of these companies are doing
From wikipedia:
The traditional problems (or goals) of AI research include reasoning, knowledge representation, planning, learning, natural language processing, perception and the ability to move and manipulate objects
Formal verification hits reasoning and knowledge rep. If there is any automatic proving, that hits planning, too.
Mike Shulman (Jun 22 2021 at 20:36):In formal verification, as I understand it, it isn't the computer doing the "reasoning" or "knowledge representation". You wouldn't say that XML is AI because it's "knowledge representation", or that a go-cart is AI because it has "the ability to move".
Spencer Breiner (Jun 22 2021 at 20:44):You all seem very sure that AI is a narrowly defined field, but my understanding is otherwise. I'll let it go after this post.
Again from wikipedia:
In artificial intelligence, an expert system is a computer system emulating the decision-making ability of a human expert.[1] Expert systems are designed to solve complex problems by reasoning through bodies of knowledge, represented mainly as if–then rules rather than through conventional procedural code
Note that expert systems are not expected to produce the knowledge representations, but rather to use them to answer questions.
Similarly, I would argue that verification is reasoning; even if the verification system isn't producing the proof, it is checking it. Plus, any useful verification system also has some automated reasoning or tactics.
Jules Hedges (Jun 22 2021 at 21:04):John Baez said:
Okay, here's a question: are there any companies using category theory to do AI - in some sense that most of us would agree is really AI?
Anyone know about Uber? There was a rumour that they were doing something involving category theory, and they for sure (used to) do some very serious machine learning
John Baez (Jun 22 2021 at 21:16):Uber is one of the clients of Conexus, and Uber may use machine learning, and Conexus uses category theory...
Fabrizio Genovese (Jun 22 2021 at 23:13):Spencer Breiner said:
You all seem very sure that AI is a narrowly defined field, but my understanding is otherwise. I'll let it go after this post.
Again from wikipedia:
In artificial intelligence, an expert system is a computer system emulating the decision-making ability of a human expert.[1] Expert systems are designed to solve complex problems by reasoning through bodies of knowledge, represented mainly as if–then rules rather than through conventional procedural code
Note that expert systems are not expected to produce the knowledge representations, but rather to use them to answer questions.
Similarly, I would argue that verification is reasoning; even if the verification system isn't producing the proof, it is checking it. Plus, any useful verification system also has some automated reasoning or tactics.
I hate discussing about definitions, it's one of the ways to losing time people seem most affectionate to, but in my (limited, and for sure not indicative experience) you are the only person I know so far that considers formal verification part of AI.
Fabrizio Genovese (Jun 22 2021 at 23:14):...Which doesn't mean your opinion is wrong. But maybe it is unpopular. :stuck_out_tongue:
David Michael Roberts (Jun 23 2021 at 01:48):Jules Hedges said:
Obviously the boundaries are blurry. All kinds of automated logical inference was once considered AI, so in that sense for example SAT and SMT solving would be AI, but as far as I know they're no longer used for anything that's recognisably AI
A bit like running a logistic regression model and calling it machine learning :upside_down:
John Baez (Jun 28 2021 at 15:51):It's possible that people/companies interested in AI and category theory will attend this workshop on machine learning and type theory... and if you're interested, you should fill out this form:
https://twitter.com/TaliaRinger/status/1409302822940598272
Interested in a machine learning and type theory workshop? Please fill this form out so that I can gauge interest and collect ideas! https://forms.gle/oWUgW67CCChZfs6j8
- Talia Ringer (@TaliaRinger) Notification Bot (Jul 01 2021 at 13:15):This topic was moved by Morgan Rogers (he/him) to #general: off-topic > AI isn't just ML
Avi Craimer (Oct 01 2021 at 17:58):PlantingSpace is the company I'm working out, which is using category theory for a Bayesian learning system.
Fabrizio Genovese (Oct 01 2021 at 19:55):Oh cool, so you also work with Alessandro?
Fabrizio Genovese (Oct 01 2021 at 19:55):The redhead guy that does egraphs in Julia, I don't remember his surname unfortunately
Daniele Palombi (Oct 02 2021 at 11:20):Fabrizio Genovese said:
The redhead guy that does egraphs in Julia, I don't remember his surname unfortunately
Cheli