Neural Proof Nets

TL;DR

This paper introduces a neural proof net model based on Sinkhorn networks for parsing linear logic derivations, achieving high accuracy in transcribing Dutch sentences into formal proofs.

Contribution

It presents a novel neuro-symbolic parser leveraging proof nets and Sinkhorn networks, enabling end-to-end differentiable parsing of linear logic.

Findings

Achieves up to 70% accuracy on the AEThel dataset.

Demonstrates effective translation of raw text into linear lambda calculus proofs.

Provides a scalable, batch-efficient neural architecture for proof net parsing.

Abstract

Linear logic and the linear {\lambda}-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 {\AE}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 {\lambda}-calculus with an accuracy of as high as 70%.