aweinstock — LessWrong

LESSWRONG
LW

Another thing that you can do when folding associative operations over a sequence is re-parenthesize them in a way that makes them more efficient to compute.

For example, if A is a 1x1000 vector, B is a 1000x1000 square matrix, and C is a 1000x1 vector, (AB)(BC) takes less time and space to compute than A(BB)C since the intermediate 1000x1000 BB needs to be stored explicitly in the latter.

In the following python snippet, the computation of A(BB)C takes around 3/4ths of a second, while (AB)(BC) takes a handful of milliseconds.

from time import time
from numpy.random import random
A = random((1, 1000))
B = random((1000, 1000))
C = random((1000, 1))
a0 = time(); print(A.dot(B.dot(B)).dot(C)); a1 = time(); print(a1 -

aweinstockJun 23, 2020

Requesting feedback/advice: what Type Theory to study for AI safety?

"Types and Programming Languages" by Benjamin Pierce is a good textbook for learning about typesystems in general (both theory and implementation). While it doesn't cover dependent types in detail (it only goes as far as F_Omega in that direction), it provides a solid background for further reading.

"Software Foundations" (available at https://softwarefoundations.cis.upenn.edu/) is about proving programs correct in Coq (with embeddings of various Hoare logics). VST (https://vst.cs.princeton.edu/) shows that the methodology in Software Foundation extends to proving properties about actual C programs.

MIRI's papers "Proof-Producing Reflection for HOL" (https://intelligence.org/files/ProofProducingReflection.pdf) and "Definability of Truth in Probabilistic Logic" (https://intelligence.org/files/DefinabilityTruthDraft.pdf) are partial positive results on side-stepping some problems of self-reference in formal logic (the former via stratification of the logic, the latter via generalizing truth values to probabilities).