2024/02/03 by Konstantinos Kogkalidis, Kogkalidis, Konstantinos, Orestis Melkonian +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Machine Learning (cs.LG) #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2402.02104
openalex publication_date 2024/02/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.