Skip to content

Instantly share code, notes, and snippets.

import torch
def jacobian(y, x, create_graph=False):
jac = []
flat_y = y.reshape(-1)
grad_y = torch.zeros_like(flat_y)
for i in range(len(flat_y)):
grad_y[i] = 1.
grad_x, = torch.autograd.grad(flat_y, x, grad_y, retain_graph=True, create_graph=create_graph)
shagunsodhani / Deep
Created July 16, 2016 10:09
Notes for Deep Math paper
View Deep

Deep Math: Deep Sequence Models for Premise Selection


  • Automated Theorem Proving (ATP) - Attempting to prove mathematical theorems automatically.
  • Bottlenecks in ATP:
    • Autoformalization - Semantic or formal parsing of informal proofs.
    • Automated Reasoning - Reasoning about already formalised proofs.
  • Paper evaluates the effectiveness of neural sequence models for premise selection (related to automated reasoning) without using hand engineered features.
  • Link to the paper