Lessons from expert systems and CYC?

Stream: general

[Jaba Adams]

Hi folks, I'm new here. Found out about this by reading Quanta Magazine's "Building the Mathematical Library of the Future". I'm excited about this effort and that there's a whole community around it!

I was wondering -- have you taken any lessons from Doug Lenat's CYC project, and more generally the problems that we've run into building human-curated expert systems or ontologies?

There seems to be a kind of progression to these projects:
1) initial excitement / joy / productivity at green-field rapid progress
2) Becoming increasingly hemmed-in by existing definitions
3) ...
4) maintenance cost crosses over with new progress -- legacy system hell phase
4) It's 30 years later and the project is on life support

Is the fact that we now have machine learning and could use hybrid symbolic / connectionist techniques a remedy?

• Jaba

[Bryan Gin-ge Chen]

Welcome Jaba! I don't think there's been much discussion here of expert systems in relation to mathlib (I've personally never heard of the CYC project before now). As for whether machine learning can help with maintenance, I think it's too early to say. There are some people interested in applying machine learning to Lean and other theorem provers (see the Machine Learning for Theorem Proving stream), but it seems to me (as a somewhat-interested outsider) that most of the current focus is on using ML techniques to prove theorems rather than on e.g. improving the organization of libraries.

[Kevin Lacker]

CYC is a great thing to take lessons from, but I think I analyze it differently than you do

[Kevin Lacker]

I mean, to me the main thing about cyc is that Cycorp is a happily functioning company working on AI products, 36 years after cyc was initially created! that's quite a success, really. they didn't achieve human-level AI, but when people are talking about projects with those expectations, you're sort of doomed to failure

[Kevin Lacker]

I think cyc is kind of the unusual success case, when many of the projects in the early 80's, using similar styles of AI, did not work

[Kevin Lacker]

but still, I would estimate that more human effort goes into cyc today than is going into all formalizing-mathematics projects

[Kevin Lacker]

the second thing about cyc is that they reasonably quickly moved from being an academic project to having government customers for various knowledge-base-related things. kind of like a palantir of the 80's. that's an interesting evolution, but right now it has no real analogy to the lean world

[Kevin Lacker]

I think you are getting at a good point, though, which is that the 80's style expert systems didn't work, they didn't scale up enough. there I think the core problem was that they were encoding "fuzzy knowledge" in a rigorous, logical style of encoding. you would have a piece of knowledge like "pittsburgh is a midwestern city" and try to combine it with statements like "pennsylvania is on the east coast" and "the midwest is a different region than the east coast" and as the knowledge base grew and grew, these weird contradictions expanded, and that's how it didn't scale

[Kevin Lacker]

for mathematics it's different, because if you found 10 statements of accepted mathematics, but actually they had a contradiction when you combined them all together, well that would be a huge deal for mathematics and probably the mathematicians would have to get together and throw out one of the 10 and everyone would angst about it and create some new theories, like when they discovered the "set of all sets that dont contain themselves" paradoxes

[Kevin Lacker]

in pittsburgh-order-logic a la original cyc, that sort of contradiction happens all the time

[Kevin Lacker]

so i think that is the fundamental difference between math formalizations and 80's-style expert systems

[Jaba Adams]

@Kevin Lacker Thanks for these useful insights. It will be interesting to see how encoding a formal system will differ from encoding fuzzy "common sense" knowledge.