Gödel machine

Variables of interest

There are three variables that are particularly useful in the run time of the Gödel machine.

• At some time ${\displaystyle t}$, the variable ${\displaystyle \text{time}}$ will have the binary equivalent of ${\displaystyle t}$. This is incremented steadily throughout the run time of the machine.

• Any input meant for the Gödel machine from the natural environment is stored in variable ${\displaystyle x}$. It is likely the case that ${\displaystyle x}$ will hold different values for different values of variable ${\displaystyle \text{time}}$.

• The outputs of the Gödel machine are stored in variable ${\displaystyle y}$, where ${\displaystyle y(t)}$ would be the output bit-string at some time ${\displaystyle t}$.

At any given time ${\displaystyle t}$, where ${\displaystyle (1\le t\le T)}$, the goal is to maximize future success or utility. A typical utility function follows the pattern ${\displaystyle u(s,\mathrm{E}\mathrm{n}\mathrm{v}):S\times E\to \mathbb{R}}$:

${\displaystyle u(s,\mathrm{E}\mathrm{n}\mathrm{v})=E_{\mu }[\sum _{\tau =\text{time}}^{T}r(\tau )\mid s,\mathrm{E}\mathrm{n}\mathrm{v}]}$

where ${\displaystyle r(t)}$ is a real-valued reward input (encoded within ${\displaystyle s(t)}$) at time ${\displaystyle t}$, ${\displaystyle E_{\mu }[\cdot \mid \cdot ]}$ denotes the conditional expectation operator with respect to some possibly unknown distribution ${\displaystyle \mu }$ from a set ${\displaystyle M}$ of possible distributions (${\displaystyle M}$ reflects whatever is known about the possibly probabilistic reactions of the environment), and the above-mentioned ${\displaystyle \text{time}=\mathrm{time}(s)}$ is a function of state ${\displaystyle s}$ which uniquely identifies the current cycle. Note that we take into account the possibility of extending the expected lifespan through appropriate actions.

Instructions used by proof techniques

The nature of the six proof-modifying instructions below makes it impossible to insert an incorrect theorem into proof, thus trivializing proof verification.

get-axiom(n)

Appends the n-th axiom as a theorem to the current theorem sequence. Below is the initial axiom scheme:

• Hardware Axioms formally specify how components of the machine could change from one cycle to the next.
• Reward Axioms define the computational cost of hardware instruction and the physical cost of output actions. Related Axioms also define the lifetime of the Gödel machine as scalar quantities representing all rewards/costs.
• Environment Axioms restrict the way new inputs x are produced from the environment, based on previous sequences of inputs y.
• Uncertainty Axioms/String Manipulation Axioms are standard axioms for arithmetic, calculus, probability theory, and string manipulation that allow for the construction of proofs related to future variable values within the Gödel machine.
• Initial State Axioms contain information about how to reconstruct parts or all of the initial state.
• Utility Axioms describe the overall goal in the form of utility function u.

apply-rule(k, m, n)

Takes in the index k of an inference rule (such as Modus tollens, Modus ponens), and attempts to apply it to the two previously proved theorems m and n. The resulting theorem is then added to the proof.

delete-theorem(m)

Deletes the theorem stored at index m in the current proof. This helps to mitigate storage constraints caused by redundant and unnecessary theorems. Deleted theorems can no longer be referenced by the above apply-rule function.

set-switchprog(m, n)

Replaces switchprog S ^p_m:n, provided it is a non-empty substring of S ^p.

check()

Verifies whether the goal of the proof search has been reached. A target theorem states that given the current axiomatized utility function u (Item 1f), the utility of a switch from p to the current switchprog would be higher than the utility of continuing the execution of p (which would keep searching for alternative switchprogs).

state2theorem(m, n)

Takes in two arguments, m and n, and attempts to convert the contents of S_m:n into a theorem.

Example applications

Time-limited NP-hard optimization

The initial input to the Gödel machine is the representation of a connected graph with a large number of nodes linked by edges of various lengths. Within given time T it should find a cyclic path connecting all nodes. The only real-valued reward will occur at time T. It equals 1 divided by the length of the best path found so far (0 if none was found). There are no other inputs. The by-product of maximizing expected reward is to find the shortest path findable within the limited time, given the initial bias.

Fast theorem proving

Prove or disprove as quickly as possible that all even integers > 2 are the sum of two primes (Goldbach’s conjecture). The reward is 1/t, where t is the time required to produce and verify the first such proof.

Maximizing expected reward with bounded resources

A cognitive robot that needs at least 1 liter of gasoline per hour interacts with a partially unknown environment, trying to find hidden, limited gasoline depots to occasionally refuel its tank. It is rewarded in proportion to its lifetime, and dies after at most 100 years or as soon as its tank is empty or it falls off a cliff, and so on. The probabilistic environmental reactions are initially unknown but assumed to be sampled from the axiomatized Speed Prior, according to which hard-to-compute environmental reactions are unlikely. This permits a computable strategy for making near-optimal predictions. One by-product of maximizing expected reward is to maximize expected lifetime.