sometimes things are right under your nose

[gusl]

I've been meaning to email Raul Valdes-Perez, to ask if there's anyone at CMU still doing work on scientific discovery, mathematical discovery, algorithm discovery, etc.

His research goal is similar to mine:

My research goal is to improve on the current state of scientific, engineering, and other professional reasoning by developing characterizable methods and interactive software that partially automate high-end tasks of discovery. In short: Better discovery of new, interesting knowledge.

This explains my interests in:
* formalization
* machine learning / scientific methodology (i.e. same thing).

His publications are all over the place too.

Anyway, I was just biking back from the cluster, when I noticed a big Vivisimo sign next to the RiteAid on Murray (corner with Forbes). I probably noticed this sign a handful of times before, but I only made the connection now. Vivisimo is his start-up, which explains why he is an "adjunct" professor.

But what does "adjunct professor" mean?

Comments

[bhudson.livejournal.com]

"Adjunct" means "teaches a class, gets paid shit and a title for it." Like, $2500 or so. And the right to call him/herself an adjunct professor.

It's a temporary position, of course: when the class is over, the position ends (though adjuncts typically maintain long-term contact teaching a class or two every semester).

[bhudson.livejournal.com]

I'm not sure how the twelf and other theorem-proving stuff that goes on at CMU relates to this that you're interested in. There are theorem proving frameworks that do some discovery, but the names escape me. I'm betting jcreed would at least know who would know.

[gustavolacerda.livejournal.com]

I don't think Twelf is used for proof search... which is not to say it couldn't. I have asked Frank Pfenning about computational scientific discovery here, and his best guess was Raul Valdes-Perez.

The "this" that I am interested is the scientific process (and its automation), which includes:
* discovery: coming up with interesting hypotheses
* justification: "proving" the above, by finding explanatory links (deductive, inductive, abductive, etc.) between the hypothesis and the theory&data.

Justification can make use of proof search. This should be especially useful in deeply-deductive (math-heavy) domains. But most science is like reverse mathematics: you work from the consequences (observables) to the axioms (theoretical entities). So we need theorem-provers that do reverse-mathematics.

Machine learning, i.e. the automatic creation of statistical models, is about justification, I would say, although the "theory" is usually implicit: often, the output of learning is an "empirical model", with no (or weak) links to a theory. By looking at these graphs, you may eventually develop a bridge between empirical model and theory.
I suppose you could say that sometimes the theory comes first and models come from theories, but I can't imagine any examples of that.

"Data mining" usually means machine learning for the discovery of new patterns (The term "KDD" is more explicitly so, since it contains the word "discovery").

Oops, I guess I got carried away with my definitions!

[jcreed.livejournal.com]

Well, Twelf is used all the time for proof search in the logic programming sense, and infrequently (but sometimes) for proof search in the sense of automated theorem proving.

Basically I stick to my belief that automatically replicating the way human cognition is presently used in discovering interesting conjectures and proofs of them is tremendously hard, and certainly at least somewhat harder than was expected by early AI research. I've heard of essentially no research that demonstrated that "jumping in the deep end" (studying how humans deal with proofs at a high level, as opposed to incrementally studying logics and proof theories, and perhaps tactics for them) actually yields results that generalize well, although I would love to have my intuitions refuted by such results!

[neelk]

I agree with you that the problem is hard, but my sense of why is a little different. Basically, I think that we (proof theorists) can do a pretty good job with first-order logic, as long as it doesn't have induction. We know where the nondeterminism is, and how to keep it (somewhat) under control. Adding induction just runs us over with a steamroller, because now we need to generalize induction hypotheses, and that's an infinite search space. It has to be searched heuristically, and proof-theoretic methods aren't great at that. You need some kind of machine learning or AI there to get any traction, I bet. But blindly applying ML won't help, because naive approaches to logic are killed by nondeterminism.

So you need an machine learning expert who is also a structural proof theorist. That combination of skills may not actually exist....

[jcreed.livejournal.com]

I think I disagree: you probably need even more than that.

There is a big gap between machine learning algorithms that do admittedly incredibly useful things with text, and future algorithms that might actually do things with text that resembles cognition. I think if you found a way to do machine learning to search for generalizations of the induction hypothesis, it might buy you a little, but only that; really being smart is what's necessary in the long run, and that's hard.

[gustavolacerda.livejournal.com]

In my view, a large part of "being smart" (in the context of searching for proofs) is having multiple representations, and having them integrated enough that you can switch between them.

[neelk]

Maybe my sights might be lower than yours: I'd be overjoyed with a theorem prover that could do as well as a C- student in 212. At least I wouldn't have to freaking prove that addition is commutative ever again....

[gustavolacerda.livejournal.com]

But blindly applying ML won't help, because naive approaches to logic are killed by nondeterminism.

What does this mean?

[neelk]

Suppose you're doing formal proof. You have some set of assumptions, and you want to use them and the rules of inference to find out if a conclusion follows. Your prover can only do one thing at a time, and you have a set of assumptions to pick from, so you have to guess which one to look at. And since your guess might be wrong, you have to be able to backtrack. And since you have to make a new guess at each step, you end up with a LOT of nondeterminism, and that's without even starting to think about quantifiers.

Proof theory can help, because you can prove that a good deal of that nondetermism is inessential -- that is, it doesn't matter which choice you make, so you don't have to save those backtracking points. This shrinks the search space a lot, which means that algorithms for exploring it have a much easier time of it.

[kvschwartz.livejournal.com]

I have some philosophy-oid questions for you:

What are some of the big Open Questions in philosophy these days? I know there are a lot in philosophy of mind -- dualism vs. monism; strong A.I. vs weak A.I.; can consciousness be algorithmic?; does a computer "understand" what it does? -- "The Chinese Room" thought experiment -- is that by Searle? by whomever.

What are some more?

Also, in other fields of philosophy?

Also are there any Open Questions in logic today, as there were so famously, say, 100 years ago, before Goedel and Tarski shattered the dreams of the formalists?

Who would you say are the most important philosophers still active today? (Is Gilbert Harman one of them? I ask because I studed with him at Princeton oh sooo many years ago.


Many thanks!