- The paper presents Deep Convolutional Generative Adversarial Nets (DCGAN) - a topologically constrained variant of conditional GAN.
- Link to the paper
- Stable to train
{-# LANGUAGE GADTs #-} | |
{- | |
The following code is based on experimental code by Aslan Askerov | |
based on Ramsey and Pfeffers "Stochastic Lambda Calculus and Monads of | |
Probability Distributions". Implementation of random n is from | |
Audebaud and Paulin-Mohring paper, so is the random walk example. | |
This gist is used here http://madsbuch.com/the-probability-monad/ | |
The class hierarchy is as follows: |
import keras | |
import numpy as np | |
timesteps = 60 | |
input_dim = 64 | |
samples = 10000 | |
batch_size = 128 | |
output_dim = 64 | |
# Test data. |
from selenium import webdriver | |
from selenium.webdriver.support.ui import WebDriverWait | |
from selenium.webdriver.common.by import By | |
from selenium.webdriver.support import expected_conditions as EC | |
import requests | |
import os | |
def download_all_papers(base_url, save_dir, driver_path): | |
driver = webdriver.Chrome(driver_path) |
// An example of using the PyTorch C++ API to implement a custom forward and backward function | |
#include <iostream> | |
#include <vector> | |
#include <torch/torch.h> | |
#include <torch/csrc/autograd/variable.h> | |
#include <torch/csrc/autograd/function.h> | |
#include <torch/csrc/autograd/VariableTypeUtils.h> | |
#include <torch/csrc/autograd/functions/utils.h> |
Lean extends the Calculus of Inductive Constructions with quotient types, as discussed by Carneiro (2019, Sec 2.7.1). However, that and other choices break some metatheoretic properties of CIC (Carneiro, 2019, Sec. 3.1), properties that Coq developers care about; consistency is nevertheless preserved.
Coq does not add support for quotients; one must instead use setoids explicitly. By looking at Carneiro (2019), we can see the difference: unlike quotient A/R, a setoid (A, R) is not a standard type, and we must explicitly remember to use R instead of standard equality wherever needed. Both with setoids and quotients, we must ensure that functions respect the equivalence on their domain. However, when using quotients A/R, that must only be checked for functions that use A/R's eliminator, while with setoids we need more work. For example, take a function f : A/R -> B, and g : B -> C: we can