@inproceedings{
kogkalidis2024learning,
title={Learning Structure-Aware Representations of Dependent Types},
author={Konstantinos Kogkalidis and Orestis Melkonian and Jean-Philippe Bernardy},
booktitle={The Thirty-eighth Annual Conference on Neural Information Processing Systems},
year={2024},
url={https://openreview.net/forum?id=e397soEZh8}
}
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.
Learning Structure-Aware Representations of Dependent Types
Konstantinos Kogkalidis Orestis Melkonian Jean-Philippe Bernardy