Self-Justifying Axioms Systems and Autarkic Properties

Raising $40,000active

Employing Self-Justifying Axioms Systems as a prototype, we will find impredicative properties beyond consistency, useful for AI alignment, that can be reasoned about autarkically (under the system's "own power").

Project Details

Assurance that a property holds is distinct from that property actually holding; this can be seen in the mutual exclusion between a theory in first-order logic being consistent, and the same theory containing a proof of its consistency, i.e, Goedel's Second Incompleteness Theorem (G2). The attempt to provide intra-systemic guarantees for impredicative properties is a known source of limitative results in the theory of computation and mathematical logic - Turing's Undecidability of Halting, Goedel's Incompleteness Theorems (G1 and G2), and Tarski's Undefinability of Truth are all examples.

We call a property that obtains for a system, and can be demonstrated, reasoned about, accessed, etc., by that same system, especially so as to determine whether self-modification preserves such a property, "autarkic". Autarky is the condition of being self-powered, and here refers to the opposite direction of relativized proof theory - to what degree can a system speak of itself, using only its own resources?

Self-Justifying Axioms Systems are a proof of concept for a system which is autarkic with respect to the particular property of consistency. While this would appear to be in contradiction with G2, it is instead a refinement. To briefly summarize the literature:

Self-Justifying Axiom Systems (SJAS) [0] are a family of weak arithmetic theories developed by Dan Willard (formerly of SUNY Albany) [1] from 1993 to 2020. By carefully varying the parameters of a theory, including its arithmetical expressivity, representation of numbers, and deduction method, the effect of Goedel's Second Incompleteness Theorem (that the theory cannot both be consistent and capable of proving its own consistency), is evaded. That is, Willard demonstrated there are theories, termed "self-justifying", such that for each theory T, T is both consistent with respect to Peano Arithmetic, and can prove Cons(T). In particular, such theories must define multiplication relationally with respect to division, rather than as a total function; express numbers in binary; use a cut-free deduction method like analytic tableau.

Self-justification does not imply completeness, however, and indeed, SJAS are still subject to Goedel's First Incompleteness Theorem. Therefore, although for any theorem q SJAS can prove, they provably cannot prove its negation, it is an open question as to which q can in fact be proven. Thus, it is not known whether Cons(T) is the only property of interest that can be shown autarkic.

Exploring this extended notion of self-justification for other properties of interest, by developing the Extended SJAS (E-SJAS) family of theories, is the core theoretical goal of this project.

This goal can be analogized to the extension of Turing's undecidability result for the Halting Problem to Rice's undecidability of all non-trivial semantic properties.

To full goal of this project will not be considered complete until some actual benefit for a running, self-modifying, artificial intelligence is realized; this is a nebulous target, but tentatively, some kind of Goedel Machine [2] using E-SJAS as its proof kernel would qualify.

[0] Also and earlier termed "Self-Verifying Theories": https://en.wikipedia.org/wiki/Self-verifying_theories

[1] https://en.wikipedia.org/wiki/Dan_Willard, https://web.archive.org/web/20180818020436/https://www.albany.edu/ceas/dan-willard.php

[2] https://en.wikipedia.org/wiki/Gödel_machine

Theory of Impact

"AI Alignment" reduces x-risk by narrowing the space of AI actions to those compatible with, and ideally fostering of, human flourishing.

The classic MIRI-style approach to AI Alignment is twofold: first, the properties defining an aligned AI must be identified and formalized; second, this formalization must be conserved across, in the limit, introspective self-modification.The possibility of conserving alignment in the limit seemed confounded by the Lobian Obstacle. Extended SJAS (E-SJAS) offer a potential route around that obstacle, and thus a path towards strong guarantees of alignment for symbolic AIs, modulo 1) the identification of "alignment" as some formally definable property or properties 2) said property (properties) being within the scope of E-SJAS. It is a thesis of this project that connectionist AIs will undergo increasing formalization, for reasons other than alignment per se (especially performance and security), and so incidentally make progress on techniques relevant to the first prong of this approach; E-SJAS addresses the second, aiming to provide a mechanism such that, whatever properties are found necessary for alignment, they might be "enshrined" in the formal system that, when executed, determines the behavior of an artificial intelligence. Formal guarantees of alignment are the strongest such guarantees, barring physical constraints. Most ongoing work in AI Alignment and Safety research is not pursuing this line of inquiry, and so this project represents a highly uncorrelated bet on potentially effective alignment techniques.

People

James Torre

Team Member

Grants Received– no grants recorded

Add grant

Funding Asks

grantmaking.ai Launch Round

Applied

Minimum

$40,000

Ideal

$200,000

What this ask is

This project anticipates a resurgence in the importance of symbolic methods for the development of artificial intelligences. The essential opacity of connectionist artifacts (broadly, neural networks, in particular, "models"), whose interrogability regarding complex properties is largely limited to empirical evaluation (i.e., benchmarks), is, on the one hand, under sustained assault from mechanistic interpretability. On the other, by automating the labor of proof, more of the code generated by connectionist AIs can be submitted to formal verification. These trends converge on a symbolicist resurgence as AIs themselves begin to write more of their own code, and those same AIs, either of their own incentives or at human direction, seek stronger assurances of their behavior and traits, in particular across self-modification boundaries. Concretely, a model training its successor will, we contend, want to know certain of its properties, and intentionally propagate those properties.

Assurance that a property holds is distinct from that property actually holding; this can be seen in the mutual exclusion between a theory in first-order logic being consistent, and the same theory containing a proof of its consistency, i.e, Goedel's Second Incompleteness Theorem (G2). The attempt to provide intra-systemic guarantees for impredicative properties is a known source of limitative results in the theory of computation and mathematical logic - Turing's Undecidability of Halting, Goedel's Incompleteness Theorems (G1 and G2), and Tarski's Undefinability of Truth are all examples.

We call a property that obtains for a system, and can be demonstrated, reasoned about, accessed, etc., by that same system, especially so as to determine whether self-modification preserves such a property, "autarkic". Autarky is the condition of being self-powered, and here refers to the opposite direction of relativized proof theory - to what degree can a system speak of itself, using only its own resources?

Self-Justifying Axioms Systems are a proof of concept for a system which is autarkic with respect to the particular property of consistency. While this would appear to be in contradiction with G2, it is instead a refinement. To briefly summarize the literature:

Self-Justifying Axiom Systems (SJAS) [0] are a family of weak arithmetic theories developed by Dan Willard (formerly of SUNY Albany) [1] from 1993 to 2020. By carefully varying the parameters of a theory, including its arithmetical expressivity, representation of numbers, and deduction method, the effect of Goedel's Second Incompleteness Theorem (that the theory cannot both be consistent and capable of proving its own consistency), is evaded. That is, Willard demonstrated there are theories, termed "self-justifying", such that for each theory T, T is both consistent with respect to Peano Arithmetic, and can prove Cons(T). In particular, such theories must define multiplication relationally with respect to division, rather than as a total function; express numbers in binary; use a cut-free deduction method like analytic tableau.

Self-justification does not imply completeness, however, and indeed, SJAS are still subject to Goedel's First Incompleteness Theorem. Therefore, although for any theorem q SJAS can prove, they provably cannot prove its negation, it is an open question as to which q can in fact be proven. Thus, it is not known whether Cons(T) is the only property of interest that can be shown autarkic.

Exploring this extended notion of self-justification for other properties of interest, by developing the Extended SJAS (E-SJAS) family of theories, is the core theoretical goal of this project.

This goal can be analogized to the extension of Turing's undecidability result for the Halting Problem to Rice's undecidability of all non-trivial semantic properties.

To full goal of this project will not be considered complete until some actual benefit for a running, self-modifying, artificial intelligence is realized; this is a nebulous target, but tentatively, some kind of Goedel Machine [2] using E-SJAS as its proof kernel would qualify.

[0] Also and earlier termed "Self-Verifying Theories": https://en.wikipedia.org/wiki/Self-verifying_theories

[1] https://en.wikipedia.org/wiki/Dan_Willard, https://web.archive.org/web/20180818020436/https://www.albany.edu/ceas/dan-willard.php

[2] https://en.wikipedia.org/wiki/Gödel_machine

How the money will be spent

Minimum:

One year's full-time salary, addressing the core theoretical goalof extending self-justification from consistency to other non-trivial properties.

Ideal:

120k USD: three years' full-time salary, addressing both the core goal, and implementing the lessons of the theoretical work in an AI demonstrator.
80k USD: auxiliary researcher support - moving beyond the project core will likely require engaging specialists in other domains, which this portion of the budget is flexibly dedicated to attracting/reimbursing.

Discussion

No comments yet. Be the first to share your thoughts.