Applications of logical uncertainty

post by alex_zag_al · 2014-10-18T19:26:30.516Z · LW · GW · Legacy · 19 comments

Contents

  Combining information from simulation and experiment
  Automated theorem proving
  Friendly AI
  Philosophy
  Learning about probabilistic logical uncertainty
None
19 comments

Lately I've been reading a lot about the problem of logical uncertainty. The problem is that there are logical consequences of your beliefs that you're uncertain about.

So, for statements like "the billionth digit of pi is even", it's provable from your beliefs. But you're still uncertain of it. So, the problem is, what's its probability? Well, 1/2, probably, but from what principled theory can you derive that?

That's the question. What probabilities we should assign to logical statements, and what laws of probability apply to them.

With all the time I've been spending on it, I've been wondering, will I ever have the opportunity to use it? My conclusion is, probably not me, personally. But I have come up with a decent list of ways other people might use it.

Combining information from simulation and experiment

This is why I first became interested in the problem--I was working in protein structure prediction.

The problem in protein structure prediction is figuring out how the protein folds. A protein is a big molecule. They're always these long, linear chains of atoms with relatively short side-branches. Interestingly, there are easy experiments to learn what they'd look like all stretched out in a line like this. But in reality, this long chain is folded up in a complex way. So, the problem is: given the linear, stretched out structure, what's the folded structure?

We have two general approaches to solve this problem.

One is a physics calculation. A protein folds because of electromagnetic forces, and we know how those work. So, you can set up a quantum physics simulation and end up with the correct fold. But you won't really end up with anything because your simulation will never finish if you do it precisely. So a lot of work goes into coming up with realistic approximate calculations, and using bigger computers. (Or distributed computing - Rosetta@Home distributes the calculations over the idle time of people's home computers, and you can download it now if you want your computer to help solve protein structures.)

Another is by experiment. We get some kind of reading from the protein structure--X-rays or radio waves, usually--and use that to solve the structure. This can be thought of as Bayesian inference, and, in fact, that's how some people do it--see a book dear to my heart, Bayesian Methods in Structural Bioinformatics. Some of the chapters are about P(observations|structure), and some are about the prior distribution, P(structure). This prior usually comes from experience with previous protein structures.

(A third approach that doesn't really fit into this picture is the videogame FoldIt.)

But, it occurred to me, doesn't the simulation provide a prior?

This is actually a classic case of logical uncertainty. Our beliefs actually imply a fold--we know the linear chain, we know the laws of physics, from that you can theoretically calculate the folded structure. But we can't actually do it, which is why we need experiments, the experiments are actually resolving logical uncertainty.

My dream is for us to be able to do that explicitly, in the math. To calculate a prior using the laws of physics plus logical uncertainty, and then condition on experimental evidence to resolve that uncertainty.

There are two people that I know of, doing research that resembles this. One is Francesco Stingo. He published a method for detecting binding between two different kinds of molecules--miRNA and mRNA. His method has a prior that is based in part on chemistry-based predictions of binding, and updated on the results of microarray experiments. The other is Cari Kaufman, who builds probability distributions over the results of a climate simulation. (the idea seems to be to extrapolate from simulations actually run with similar but not identical parameters)

What I have in mind would accomplish the same kind of thing in a different way--the prior would come from a general theory for assigning probabilities to statements of mathematics, and "the laws of physics predict these two molecules bind" would be one such statement.

Automated theorem proving

I don't know anything about this field, but this kind of makes sense--what if you could decide which lemmas to try and prove based on their probability? That'd be cool.

Or, decide which lemmas are important with value of information calculations.

(AlanCrowe talked about something like this in a comment)

Friendly AI

I don't really understand this, something about a "Löbian obstacle." But Squark has a bit of an overview at "Overcoming the Loebian obstacle using evidence logic". And qmaurmann wrote something on a similar topic, "Meditations on Löb’s theorem and probabilistic logic." eli_sennesh also recently wrote a related post.

There's an interesting result, in this line of research. It says that, although it's well known that a formal system cannot contain a predicate representing truth in that system, this is actually just because formal proof systems only assign certainties of 0 and 1. If they instead gave false statements probability infinitesimally close to 0, and true statements infinitesimally close to 1, they could define truth. (Disclaimer: I can't follow all the math and the result has not yet been published in a peer reviewed journal). This is such an odd use of probabilistic logical uncertainty, nothing like the applications I've been imagining, but there it is.

(walkthrough of the paper here)

Philosophy

Philosophically, I want to know how you calculate the rational degree of belief in every proposition. Good philosophical theories don't necessarily need to be practical to use. Even if it's impossible to compute, it's got to give the right answer in simple thought experiments, so I feel like I can reason without paradox. But even getting all these simple thought experiments right is hard. Good philosophical theories are hard to come by.

Bayesian confirmation theory has been a successful philosophical theory for thought experiments involving the confirmation of theories by evidence. It tells you how belief in a hypothesis should go up or down after seeing observational evidence.

But what about mathematical evidence, what about derivations? Wasn't Einstein's derivation that general relativity predicts the orbit of Mercury evidence in favor of the theory? I want a philosophical theory, I want basic principles, that will tell me "yes." That will tell me the rational degree of belief is higher if I know the derivation.

Philosophers frame this as the "problem of old evidence." They think of it like: you come up with a new theory like GR, consider old evidence like Mercury, and somehow increase your confidence in the new theory. The "paradox" is that you didn't learn of any new evidence, but your confidence in the theory still changed. Philosopher Daniel Garber argues that the new evidence is a mathematical derivation, and the problem would be solved by extending Bayesian probability theory to logical uncertainty. (The paper is called "Old Evidence and Logical Omniscience in Bayesian Confirmation Theory," and can be found here)

A more general philosophical theory than Bayesian confirmation theory is Solomonoff induction, which provides a way to assign probabilities to any observation given any past observations. It requires infinite computing power. However, there still is a rational degree of belief for an agent with finite computing power to have, given the computations that they've done. I want the complete philosophical theory that tells me that.

Learning about probabilistic logical uncertainty

I made a list of references here, if you'd like to learn more about the subject.

19 comments

Comments sorted by top scores.