Learning Structure-Aware Representations of Dependent Types
<|reference_start|>Learning Structure-Aware Representations of Dependent Types: 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, detailing 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 strong initial results.<|reference_end|>
@article{kogkalidis2024learning,
    title={Learning Structure-Aware Representations of Dependent Types},
    author={Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy},
    journal={arXiv preprint arXiv:2402.02104},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.02104},
    primaryClass={cs.LG cs.PL}
}