larsr

VAE Derivation: From KL Divergence to ELBO

Showing that minimizing KL divergence is equivalent to maximizing ELBO

$$\text{(1)} \quad \text{KL}(q_\phi(z|x) | p(z|x)) = \mathbb{E}_{q_\phi(z|x)}\left[\log \frac{q_\phi(z|x)}{p(z|x)}\right] \quad \text{[definition of KL]}$$

$$\text{(2)} \quad = \mathbb{E}_{q_\phi(z|x)}[\log q_\phi(z|x)] - \mathbb{E}_{q_\phi(z|x)}[\log p(z|x)] \quad \text{[split logarithm]}$$

$$\text{(3)} \quad = \mathbb{E}_{q_\phi(z|x)}[\log q_\phi(z|x)] - \mathbb{E}_{q_\phi(z|x)}\left[\log \frac{p(x,z)}{p(x)}\right] \quad \text{[Bayes rule]}$$

Disable Device Enrollment Program (DEP) notification on macOS Catalina.md

With full reinstall (recommended)

a. Boot into recovery using command-R during reboot, wipe the harddrive using Disk Utility, and select reinstall macOS

b. Initial installation will run for approximately 1 hour, and reboot once

c. It will then show a remaining time of about 10-15 minutes

Creating a `.so` dynamic library of a haskell program and calling it from C

TLDR:

Export a haskell function with foreign export.
Create a C wrapper that calls hs_init when the library is loaded.
Compile the .hs and .c wrapper with ghc, linking with lHSrts-ghc8.6.5
Use it from C by linking as usual.

(For more details, see here.)

Haskell

import Crypto.Cipher.AES
import Data.ByteString.UTF8 (fromString, toString)
import Data.ByteString.Base16 (encode)


main = do

	#!/usr/bin/env bash

	#
	# This command runs python modules with uvx.
	# Rename or make a link to this script to decide what module to run.
	# Example:
	# ln -s quick-command.sh ipython; ./ipython
	# If you set DOCKER=1 it will run them inside an alpine linux instance.
	# ln -s quick-command.sh ipython; DOCKER=1 ./ipython
	# Don't be shy to modify the uvx command at the bottom if you need i.e. some more libraries!

	Definition plus_assoc : forall a b, a + b = b + a :=
	nat_ind (fun n => forall b, n + b = b + n)
	(nat_ind (fun n => n = n + 0) eq_refl (fun n => eq_S _ _))
	(fun n H b => eq_trans (eq_S _ _ (H b))
	(nat_ind (fun b => S (b + n) = b + S n)
	eq_refl
	(fun _ => eq_S _ _) b) : S (n + b) = b + S n).

	(* Proof that you can build foldR out of foldL *)


	Require Import Arith List. Import ListNotations.


	Fixpoint foldR {A : Type} {B : Type} (f : A -> B -> B) (v : B) (l : list A) : B :=
	match l with
	\| nil => v
	\| x :: xs => f x (foldR f v xs)

	#include <stdio.h>
	#include <stdlib.h>
	#include <stdint.h>
	#ifdef _MSC_VER
	#include <intrin.h> /* for rdtscp and clflush */
	#pragma optimize("gt",on)
	#else
	#include <x86intrin.h> /* for rdtscp and clflush */
	#endif

	# docker build -t coq .
	# coqtop() (docker run --rm -v "$HOME:$HOME" -ti coq sh -c "cd $HOME ; "'coqtop $(cat ~/src/VST/_CoqProject-export)'" $@")

	#FROM coqorg/coq:dev
	FROM coqorg/coq:8.11.0

	RUN opam init -y; \
	opam repo --set-default add coq-released https://coq.inria.fr/opam/released; \
	opam install -y -b coq-mathcomp-algebra coq-mathcomp-analysis coq-coquelicot coq-compcert

	cat >demo.hs <<EOF
	quicksort [] = []
	quicksort (p:xs) = (quicksort lesser) ++ [p] ++ (quicksort greater)
	where
	lesser = filter (< p) xs
	greater = filter (>= p) xs

	main = print(quicksort([5,2,1,0,8,3]))
	EOF