shagunsodhani

Deep Math: Deep Sequence Models for Premise Selection

Introduction

• 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

apaszke

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)
        jac.append(grad_x.reshape(x.shape))