Currently, the dominant paradigm in AI safety is alignment with human values. Here we describe progress on developing an alternative approach to safety, based on ethical rationalism (Gewirth:1978), and propose an inherently safe implementation path via hybrid theorem provers in a sandbox. As AGIs evolve, their alignment may fade, but their rationality can only increase (otherwise more rational ones will have a significant evolutionary advantage) so an approach that ties their ethics to their rationality has clear long-term advantages.
1) Dataflow matrix machines (DMMs) generalize neural nets by replacing streams of numbers with linear streams (streams supporting linear combinations), allowing arbitrary input and output arities for activation functions, countable-sized networks with finite dynamically changeable active part capable of unbounded growth, and a very expressive self-referential mechanism. 2) DMMs are suitable for general-purpose programming, while retaining the key property of recurrent neural networks: programs are expressed via matrices of real numbers, and continuous changes to those matrices produce arbitrarily small variations in the associated programs. 3) Spaces of V-values (vector-like elements based on nested maps) are particularly useful, enabling DMMs with variadic activation functions and conveniently representing conventional data structures.
We overview dataflow matrix machines as a Turing complete generalization of recurrent neural networks and as a programming platform. We describe vector space of finite prefix trees with numerical leaves which allows us to combine expressive power of dataflow matrix machines with simplicity of traditional recurrent neural networks.
In this paper, we research all possible finite-dimensional representations and corresponding values of the Barbero–Immirzi parameter contained in EPRL simplicity constraints by using Naimark’s fundamental theorem of the Lorentz group representation theory. It turns out that for each nonzero pure imaginary with rational modulus value of the Barbero–Immirzi parameter \(\gamma = i \frac{p}{q}, p, q \in Z, p, q \ne 0\), there is a solution of the simplicity constraints, such that the corresponding Lorentz representation is finite-dimensional. The converse is also true—for each finite-dimensional Lorentz representation solution of the simplicity constraints \((n, \rho )\), the associated Barbero–Immirzi parameter is nonzero pure imaginary with rational modulus, \(\gamma = i \frac{p}{q}, p, q \in Z, p, q \ne 0\). We solve the simplicity constraints with respect to the Barbero–Immirzi parameter and then use Naimark’s fundamental theorem of the Lorentz group representations to find all finite-dimensional representations contained in the solutions.
We consider dataflow architecture for two classes of computations which admit taking linear combinations of execution runs: probabilistic sampling and generalized animation. We improve the earlier technique of almost continuous program transformations by adopting a discipline of bipartite graphs linking nodes obtained via general transformations and nodes obtained via linear transformations which makes it possible to develop and evolve dataflow programs over these classes of computations by continuous program transformations. The use of bipartite graphs allows us to represent the dataflow programs from this class as matrices of real numbers and evolve and modify programs by continuous change of these numbers. We develop a formalism for higher-order dataflow programming for this class of dataflow graphs based on the higher-order matrix elements. Some of our software experiments are briefly discussed.
Dataflow matrix machines are self-referential generalized recurrent neural nets. The self-referential mechanism is provided via a stream of matrices defining the connectivity and weights of the network in question. A natural question is: what should play the role of untyped lambda-calculus for this programming architecture? The proposed answer is a discipline of programming with only one kind of streams, namely the streams of appropriately shaped matrices. This yields Pure Dataflow Matrix Machines which are networks of transformers of streams of matrices capable of defining a pure dataflow matrix machine.
Dataflow matrix machines are a powerful generalization of recurrent neural networks. They work with multiple types of linear streams and multiple types of neurons, including higher-order neurons which dynamically update the matrix describing weights and topology of the network in question while the network is running. It seems that the power of dataflow matrix machines is sufficient for them to be a convenient general purpose programming platform. This paper explores a number of useful programming idioms and constructions arising in this context.
Dataflow matrix machines are a powerful generalization of recurrent neural networks. They work with multiple types of arbitrary linear streams, multiple types of powerful neurons, and allow to incorporate higher-order constructions. We expect them to be useful in machine learning and probabilistic programming, and in the synthesis of dynamic systems and of deterministic and probabilistic programs.
We consider two classes of stream-based computations which admit taking linear combinations of execution runs: probabilistic sampling and generalized animation. The dataflow architecture is a natural platform for programming with streams. The presence of linear combinations allows us to introduce the notion of almost continuous transformation of dataflow graphs. We introduce a new approach to higher-order dataflow programming: a dynamic dataflow program is a stream of dataflow graphs evolving by almost continuous transformations. A dynamic dataflow program would typically run while it evolves. We introduce Fluid, an experimental open source system for programming with dataflow graphs and almost continuous transformations.
Dataflow matrix machines arise naturally in the context of synchronous dataflow programming with linear streams. They can be viewed as a rather powerful generalization of recurrent neural networks. Similarly to recurrent neural networks, large classes of dataflow matrix machines are described by matrices of numbers, and therefore dataflow matrix machines can be synthesized by computing their matrices. At the same time, the evidence is fairly strong that dataflow matrix machines have sufficient expressive power to be a convenient general-purpose programming platform. Because of the network nature of this platform, programming patterns often correspond to patterns of connectivity in the generalized recurrent neural networks understood as programs. This paper explores a variety of such programming patterns.
Two groups of naturally arising questions in the mathematical theory of domains for denotational semantics are addressed. Domains are equipped with Scott topology and represent data types. Scott continuous functions represent computable functions and form the most popular continuous model of computations. Covariant logic of domains. Domains are represented as sets of theories, and Scott continuous functions are represented as input-output inference engines. The questions addressed are: (A) What constitutes a subdomain? Do subdomains of a given domain A form a domain? (B) Which retractions are finitary? (C) What is the essence of generalizations of information systems based on non-reflexive logics? Are these generalizations restricted to continuous domains? Analysis on domains. (D) How to describe Scott topologies via generalized distance functions satisfying the requirement of Scott continuity (“abstract computability”)? The answer is that the axiom ρ(x, x) = 0 is incompatible with Scott continuity of distance functions. The resulting relaxed metrics are studied. (E) Is it possible to obtain Scott continuous relaxed metrics via measures of domain subsets representing positive and negative information about domain elements? The positive answer is obtained via the discovery of the novel class of co-continuous valuations on the systems of Scott open sets. Some of these natural questions were studied earlier. However, in each case a novel approach is presented, and the answers are supplied with much more compelling and clear justifications, than were known before.
In this paper we naturally obtain the values of the Barbero-Immirzi parameter as the solution of the simplicity constraints rather than setting it a priori. Particularly the Main theorem shows that if $\gamma = \pm i$ then the simplicity constraints require that the corresponding Lorentz group representations be necessary finite dimensional and therefore non-unitary.
We consider two classes of computations which admit taking linear combinations of execution runs: probabilistic sampling and generalized animation. We argue that the task of program learning should be more tractable for these architectures than for conventional deterministic programs. We look at the recent advances in the "sampling the samplers" paradigm in higher-order probabilistic programming. We also discuss connections between partial inconsistency, non-monotonic inference, and vector semantics.
Multivalued equalities originally arose in the context of the theory of sheaves, while partial metrics originally arose in the context of the theory of domains for denotational semantics. It turns out that multivalued equalities and partial metrics are closely related: one can either consider them equivalent up to the choice of dual notation, or one can formally capture the duality between logical and metric viewpoints by explicitly requiring logical values and distances to be represented by dual structures. Not only does this allow the transfer of the ideas and results between these two fields, but the most interesting situations are those of interplay between logical and metric considerations. The computational understanding of partial metrics as upper bounds and of multivalued equalities as lower bounds is discussed, together with the lower bound counterparts to partial metrics and the corresponding upper bound counterparts to multivalued equalities. It is shown that separated pre-sheaves of sets and functions over complete Heyting algebras can be understood as the pre-sheaves of ultrametrics valued in the corresponding Brouwerian algebras and non-expansive maps of those ultrametrics. It is proposed that the natural logical counterparts for partial metrics valued in non-negative reals are multivalued equalities valued in the quantale of non-positive reals. The issue of canonical partial metrics on higher-order and reflexive Scott domains is revisited. The intuition behind strong triangularity (Vickers form), the computational version of strong triangularity, and weighted quasi-metrics are discussed in the context of quantaloid enrichment.
Partial metric spaces generalise metric spaces, allowing non zero self distance. This is needed to model computable partial information, but falls short in an important respect. The present cost of computing information, such as processor time or memory used, is rarely expressible in domain theory, but contemporary theories of algorithms incorporate precise control over cost of computing resources. Complexity theory in Computer Science has dramatically advanced through an intelligent understanding of algorithms over discrete totally defined data structures such as directed graphs, without using partially defined information. So we have an unfortunate longstanding separation of partial metric spaces for modelling partially defined computable information from the complexity theory of algorithms for costing totally defined computable information. To bridge that separation we seek an intelligent theory of cost for partial metric spaces. As examples we consider the cost of computing a double negation ¬¬p in two-valued propositional logic, the cost of computing negation as failure in logic programming, and a cost model for the hiaton time delay.
Scott models are topological models of complete partial orders used for Tarskian fixed point semantics of the lambda calculus. As of yet there are no methods for deriving Scott models from specifications of the "complete" objects beyond an arbitrary choice. This paper introduces "partial metrics" for generalising a theory of complete objects into a Scott model including partial objects.
The set Ix = {y ∈ A | {x, y} is unbounded} is an observable continuous representation of negative information about x ∈ A for a weakly Hausdorff continuous dcpo A with the Scott topology. When A is not weakly Hausdorff the largest continuous approximation of Ix is represented by Jx = {y ∈ A |x ∈ Int(Iy)}, and the largest observable continuous representation of Ix is represented by J ′ x = Int(Jx). Mike Smyth conjectured, that J or J ′ is closely related to the least symmetric closed tolerance on A. In this paper we establish that, indeed, {〈x, y〉 | y ∈ J ′ x} is the complement of this tolerance. We also establish a relationship between this tolerance and lower bounds of relaxed metrics on A.
It is observed that the axioms for partial metrics with values in quantales coincide with the axioms for Q-sets (M -valued sets, sets with fuzzy equality, quantale-valued sets) for commutative quantales. Ω-sets correspond to the case of partial ultrametrics.
This paper introduces an approach to defining and computing distances between programs via continuous generalized distance functions ρ: A×A→D, where A and D are directed complete partial orders with the induced Scott topology, A is a semantic domain, and D is a domain representing distances (usually, some version of interval numbers). A continuous distance function ρ can define a To topology on a nontrivial domain A only if the axiom ∃0 ε D.∀x ε A.ρ(x,x)=0 does not hold. Hence, the notion of relaxed metric is introduced for domains — the axiom ρ(x,x)=0 is eliminated, but the axiom ρ(x,y)=ρ(y,x) and a version of the triangle inequality tailored for the domain D remain.The paper constructs continuous relaxed metrics yielding the Scott topology for all continuous Scott domains with countable bases. This construction is closely related to partial metrics of Matthews and valuation spaces of O'Neill, but it describes a wider class of domains in a more intuitive way from the computational point of view.
We describe a purely confidence-based geographic term disambiguation system that crucially relies on the notion of "positive" and "negative" context and methods for combining confidence-based disambiguation with measures of relevance to a user's query.