Learning Structure-Aware Representations of Dependent Types

TL;DR

A novel neural architecture targeted at faithfully representing dependently-typed programs on the basis of structural rather than nominal principles is proposed, which achieves promising initial results, surpassing strong baselines.

Abstract

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.

Figures (6)

• Figure 1: Agda code formalizing the commutativity of addition.
• Figure 2: Tokenized view of lemma types from Figure \ref{['figure:agda-example']}; see Appendix \ref{['appendix:tokenization']} for details.
• Figure 3: Empirical distributions of the standardized scores of relevant and irrelevant lemmas from the stdlib:id evaluation set.
• Figure 4: JSON extract of the Agda code of Figure \ref{['figure:agda-example']}.
• Figure 5: Statistics of the extracted data relevant to our experimental setup.