# Neural Proof Nets

arXiv: https://arxiv.org/abs/2009.12702 · HTML: https://mlsanity.com/paper/2009.12702/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Sep 2020.

## Built on by (most cited first, 8 of 8)

- [Is Neuro-Symbolic AI Meeting its Promise in Natural Language Processing? A Structured Review](https://mlsanity.com/paper/2202.12205/) (2022)
- [Unlocking the Potential of Generative AI through Neuro-Symbolic Architectures: Benefits and Limitations](https://mlsanity.com/paper/2502.11269/) (2025)
- [Improving BERT Pretraining with Syntactic Supervision](https://mlsanity.com/paper/2104.10516/) (2021)
- [Geometry-Aware Supertagging with Heterogeneous Dynamic Convolutions](https://mlsanity.com/paper/2203.12235/) (2022)
- [Structural Ambiguity and its Disambiguation in Language Model Based Parsers: the Case of Dutch Clause Relativization](https://mlsanity.com/paper/2305.14917/) (2023)
- [SPINDLE: Spinning Raw Text into Lambda Terms with Graph Attention](https://mlsanity.com/paper/2302.12050/) (2023)
- [A Logic-Based Framework for Natural Language Inference in Dutch](https://mlsanity.com/paper/2110.03323/) (2021)
- [Perspectives on neural proof nets](https://mlsanity.com/paper/2211.04141/) (2022)

## Abstract (arXiv)

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 AEThel, 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%.