Scott Garrabrant, Tsvi Benson-Tilsen, Andrew Critch, Nate Soares, Jessica Taylor
2016 · arXiv
We present a computable algorithm that assigns probabilities to every logical statement in a given formal language, and refines those probabilities over time. For instance, if the language is Peano arithmetic, it assigns probabilities to all arithmetical statements, including claims about the twin prime conjecture, the outputs of long-running computations, and its own probabilities. We show that our algorithm, an instance of what we call a logical inductor, satisfies a number of intuitive desiderata, including: (1) it learns to predict patterns of truth and falsehood in logical statements, often long before having the resources to evaluate the statements, so long as the patterns can be written down in polynomial time; (2) it learns to use appropriate statistical summaries to predict sequences of statements whose truth values appear pseudorandom; and (3) it learns to have accurate beliefs about its own current beliefs, in a manner that avoids the standard paradoxes of self-reference. For example, if a given computer program only ever produces outputs in a certain range, a logical inductor learns this fact in a timely manner; and if late digits in the decimal expansion of $π$ are difficult to predict, then a logical inductor learns to assign $\approx 10\%$ probability to "the $n$th digit of $π$ is a 7" for large $n$. Logical inductors also learn to trust their future beliefs more than their current beliefs, and their beliefs are coherent in the limit (whenever $φ\implies ψ$, $\mathbb{P}_\infty(φ) \le \mathbb{P}_\infty(ψ)$, and so on); and logical inductors strictly dominate the universal semimeasure in the limit. These properties and many others all follow from a single logical induction criterion, which is motivated by a series of stock trading analogies. Roughly speaking, each logical sentence $φ$ is associated with a stock that is worth \$1 per share if [...]
Metadata: arXiv. Abstracts retain their original authors’ rights.
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
4 selected excerpts · 4 total mentions
For context: Logical Induction https://arxiv.org/abs/1609.03543 Sadly the line of research seems to have been abandoned. Kind of understandable with the ascent of LLMs: there is no time left for a multi-decade research program.
Probabilistic reasoning is possible in a formal setting; It produces a probability distribution over answers. To ground probabilistic logic itself I'm not aware of much progress beyond the initial idea of logical induction[0]. [0] https://arxiv.org/abs/1609.03543
That statement is too strong. The practical effect is that you should not try to build an algorithm to detect infinite loops in general (though you wouldn't need undecidability for this, per se. E.g., NP-completeness of the halting problem would probably have been sufficient to kill attempts at a general algorithm dead in the water). Of course, it is true in specific cases that you can decide whether a given program halts, and, indeed in almost all practical instances if you know how to solve a given problem then you should be able to construct an algorithm to solve it which provably halts. (Not including, of course, things that depend on environmental inputs, something…
that computes whether a given number satisfies Goldbach's conjecture, etc.) There is, of course, enormous theoretical value in the undecidability of the halting problem, and in Kurt Gödel's undecidability of a general axiomatic system. And this theoretical value guides future theoretical research which is likely to lead to further practical value in future - which indicates a practical effect in the long-term. Also, of course, it indicates that an attempt to build a general theorem-prover is a useless endeavor (though approximate / specialized theorem provers are, of course, possible and indeed exist). In particular, Gödel's undecidability has quite real implications for an Artificial General Intelligence which would have to reason about mathematics in general, and about its own thought processes in particular. Under classical mathematical reasoning, such an AI would be unable to "have confidence" in its own reasoning process. However, if the assumptions are relaxed from statements with 0/1 truth values to statements with probabilities, and time-independence of truth is relaxed, it is possible to define an agent which is able to assign (almost) consistent (actually "coherent") probabilities to what its own beliefs w̶i̶l̶l̶ ̶b̶e̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶m̶i̶t̶ ̶(̶a̶s̶ ̶t̶ ̶g̶o̶e̶s̶ ̶t̶o̶ ̶i̶n̶f̶i̶n̶i̶t̶y̶)̶) are at time t. See https://arxiv.org/abs/1609.03543 for more details. This is probably the strongest such statement that can be made in this class of arguments.
I think that Penrose basically thinks it's useful that humans can heuristically step up from a logic system S to S+"statement X is true" in an almost-grounded way, but in reality we are all actually constrained by Godel, Tarski, etc. We just trick ourselves into assuming we can inductively keep stepping up from S+"X is true" indefinitely for any practical problem we encounter, but that is actually an ungrounded assumption. What seems like an even better formal solution is something like logical induction[0] that works over something like probabilities instead of truth/falsehood. It has an existence proof but not a constructive formalization, afaik, but maybe some recent progress has been made. 0: https://arxiv.org/abs/1609.03543
More from the same topics.
Anders Sandberg, Eric Drexler, Toby Ord
The Fermi paradox is the conflict between an expectation of a high {\em ex ante} probability of intelligent life elsewhere in the universe and the apparently lifeless universe we in fact observe.
Chiyuan Zhang, Samy Bengio, Moritz Hardt +2
Despite their massive size, successful deep artificial neural networks can exhibit a remarkably small difference between training and test performance.
Haoran Xu, Fredrik Kjolstad
Fast compilation is important when compilation occurs at runtime, such as query compilers in modern database systems and WebAssembly virtual machines in modern browsers.
Scott Aaronson
In honor of Alan Turing's hundredth birthday, I unwisely set out some thoughts about one of Turing's obsessions throughout his life, the question of physics and free will.