Perspectives on neural proof nets

TL;DR

This paper introduces a novel neural network approach to proof net proof search that generates graph structures representing lambda-terms before detailed vertex labeling, contrasting with traditional methods that rely on supertagging and atomic formula matching.

Contribution

It proposes a new two-step neural method for proof search in type-logical grammars, combining graph generation with vertex labeling to improve proof structure prediction.

Findings

Graph generation guarantees lambda-term correspondence

Vertex labeling enhances detailed proof structure

Alternative approach outperforms standard supertagging methods

Abstract

In this paper I will present a novel way of combining proof net proof search with neural networks. It contrasts with the 'standard' approach which has been applied to proof search in type-logical grammars in various different forms. In the standard approach, we first transform words to formulas (supertagging) then match atomic formulas to obtain a proof. I will introduce an alternative way to split the task into two: first, we generate the graph structure in a way which guarantees it corresponds to a lambda-term, then we obtain the detailed structure using vertex labelling. Vertex labelling is a well-studied task in graph neural networks, and different ways of implementing graph generation using neural networks will be explored.