arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2402.02104cs.LGcs.PL
收藏

依赖类型的结构感知表示学习

Learning Structure-Aware Representations of Dependent Types

Aalto University(阿尔托大学);University of Bologna(博洛尼亚大学);Input Output (IOG)(Input Output(IOG));University of Gothenburg(哥德堡大学);Chalmers University of Technology(查尔姆斯理工大学)

Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy

AI总结:

该研究发布首个支持机器学习应用的大规模精细Agda程序-证明数据集,提出基于结构原则的新型神经架构以表示依赖类型程序,在前提选择任务中超越强基线,打通了Agda生态与机器学习领域的资源互通。

摘要:

Agda是一种依赖类型编程语言与证明助手,在证明形式化和编程语言理论中至关重要。本文将Agda生态系统拓展至机器学习领域,同时也为机器学习从业者提供Agda相关资源。我们提出并发布了一个全新的Agda程序-证明数据集,它精细且规模足够大,可支持各类机器学习应用,是同类中的首个数据集。利用该数据集在子类型层面详述证明状态的超高分辨率特性,我们提出一种新型神经架构,旨在基于结构而非标称原则忠实地表示依赖类型程序。我们在前提选择设置中实例化并评估了该架构,取得了颇具前景的初步结果,性能超越了强基线。

英文摘要:

Agda is a dependently-typed programming language and a proof assistant, pivotal in proof formalization and programming language theory. This paper extends the Agda ecosystem into machine learning territory, and, vice versa, makes Agda-related resources available to machine learning practitioners. We introduce and release a novel dataset of Agda program-proofs that is elaborate and extensive enough to support various machine learning applications -- the first of its kind. Leveraging the dataset's ultra-high resolution, which details proof states at the sub-type level, we propose a novel neural architecture targeted at faithfully representing dependently-typed programs on the basis of structural rather than nominal principles. We instantiate and evaluate our architecture in a premise selection setup, where it achieves promising initial results, surpassing strong baselines.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑