41–50 of 66 posts
So does this mean that the era of automated theorem proving and AI-driven mathematics is finally upon us? I'm no expert, but this seems pretty groundbreaking.
This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.
Earlier quoted context omitted.
How do you manage to claim that your computable logical inductor dominates the incomputable universal semimeasure?
I'm not an author but this property with respect to a universal 'semimeasure' holds in the limit as time goes to infinity, as do most stated properties of logical inductors. The fact that they're computable is academic.
Earlier quoted context omitted.
This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.
What is your definition of practical?
Theoretical stuff is like: proving theorems, conceptualizing the task at hand, philosophical inquiry into the nature of agents/intelligence/reasoning/goals/human values
I'm not trying to argue which is more important, but surely MIRI focuses more on the theoretical.
The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified. A formal system can…
The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified. A formal system can…
> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true. I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with Loeb's theorem). It's true that you cannot show that, say, second order arithmetic is consistent in the same system. In fact, every soundness proof (for a sufficiently strong logic) will have to be c…
On a separate matter, are there any principled meta-universal rules for incrementing the universe index? That is, if one suspects that one's current universe lacks proving power, is it possible to generate the axioms for a more powerful universe?
Earlier quoted context omitted.
This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.
At least public practical research. But I've long wondered what their bank account would look like if they had a side venture into exploiting narrow AI for commercial use rather than rely on donations.
Slightly OT but it's well worth watching the recent film about Ramanujan, "The Man Who Knew Infinity". It has kept me thinking what "intuition" really is, how it develops and happens in the brain, and what would be needed to build AI that has intuition.
It is enjoyable reading and very thorough. Pending revolutionary new insights I might even regard it as conclusive.
Earlier quoted context omitted.
This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.
What is your definition of practical?
[0] In the sense of "valid under these known precepts", not "speculative".
[1] Non "Friendly AI", not "non-Friendly" AI.
The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified. A formal system can…
But can it show that it's actually running this correct algorithm to determine whether the statement about itself is probably true? There is always an external context that runs the computation. A computation never exists in "abstract space", it always happens on a physical level. Any computation is only good if it runs in the context that it was designed for. What I mean is that the AI can never "know" if it's still…
The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified. A formal system can…
> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true. I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with Loeb's theorem). It's true that you cannot show that, say, second order arithmetic is consistent in the same system. In fact, every soundness proof (for a sufficiently strong logic) will have to be c…
As you say, this isn't quite self-trust. Another natural move is to relax the criterion of self-trust away from "it proves itself consistent" (impossible by incompleteness) towards "it assigns high probability that it has good beliefs". (Formalizations of this are in the paper.)
> At the moment I'm just confused what the problem is
In short, it would be nice to have a model of "good reasoning under deductive limitation", where "good reasoning" means something like "has accurate beliefs about all questions of interest" (for example, facts about the outputs of long-running computations), and where "deductive limitation" rules out the reasoning process "just wait for your theorem prover to decide the question".
Examples of long-running computations that are hard to compute exactly, but that we can sometimes still have reasonable beliefs about: optimal moves in chess, go, etc.; the accuracy of some ML system after a given training regimen; a weather-forecasting program that runs a gigantic series of simulations; and so on.