神经证明网
Neural Proof Nets
摘要：
线性逻辑和线性λ演算在自然语言形式和意义的研究中有着悠久的传统。在线性逻辑的证明演算中，证明网特别令人感兴趣，它提供了一种有吸引力的推导几何表示，不受传统证明理论格式的官僚复杂性的影响。基于集合论学习的最新进展，我们提出了一种基于Sinkhorn网络的证明网络的神经变体，这使我们能够将解析转换为提取句法原语并将其排列成对齐的问题。我们的方法诱导了一个批处理效率，端到端的差异化架构，实现了一个正式接地，但高效的神经符号解析器。我们测试了我们的方法，一个数据集的类型逻辑推导的书面荷兰语，在那里它设法正确地将原始文本句子转换成证明和线性λ演算的条款，准确率高达70%。
英文摘要：
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%.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
