Neural Proof Nets

Abstract

Linear logic and the linear λ-calculus have a long standing tradition in the study of natural language form and meaning. Among the proof calculi of linear logic, proof nets are of particular interest, offering an attractive geometric representation of derivations that is unburdened by the bureaucratic complications of conventional prooftheoretic formats. Building on recent advances in set-theoretic learning, we propose a neural variant of proof nets based on Sinkhorn networks, which allows us to translate parsing as the problem of extracting syntactic primitives and permuting them into alignment. Our methodology induces a batch-efficient, end-to-end differentiable architecture that actualizes a formally grounded yet highly efficient neuro-symbolic parser. We test our approach on ÆThel, a dataset of type-logical derivations for written Dutch, where it manages to correctly transcribe raw text sentences into proofs and terms of the linear λ-calculus with an accuracy of as high as 70%.

arXiv comment14 pages, CoNLL2020

References in corpus (8)

• When Does Label Smoothing Help?
• Learning to Map Sentences to Logical Form: Structured Classification with Probabilistic Categorial Grammars
• BERTje: A Dutch BERT Model
• Learning Latent Permutations with Gumbel-Sinkhorn Networks
• Sparse Sinkhorn Attention
• Encoding word order in complex embeddings
• Stochastic Optimization of Sorting Networks via Continuous Relaxations
• Constructive Type-Logical Supertagging with Self-Attention Networks

Cited by in corpus (3)

• Is Neuro-Symbolic AI Meeting its Promise in Natural Language Processing? A Structured Review
• Improving BERT Pretraining with Syntactic Supervision
• A Logic-Based Framework for Natural Language Inference in Dutch