Learning Structure-Aware Representations of Dependent Types
Authors: Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy
NeurIPS 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We introduce and release a novel dataset of Agda program-proofs...we propose a novel neural architecture targeted at faithfully representing dependently-typed programs...We instantiate and evaluate our architecture in a premise selection setup, where it achieves promising initial results, surpassing strong baselines. and 5 Experiments & Results, Table 1: Model performance under different ablations across all evaluation sets. |
| Researcher Affiliation | Collaboration | 1Aalto University 2University of Bologna 3Input Output (IOG) 4University of Gothenburg 5Chalmers University of Technology |
| Pseudocode | No | The paper describes its architecture and various components (e.g., Efficient Attention, Structured Attention, Variable Representations) but does not include any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | Source code, configuration files and scripts supporting experiment execution are available at https://github.com/konstantinos Kokos/quill. |
| Open Datasets | Yes | Concisely, we train using Info NCE on a size-constrained subset of the Agda standard library. The extraction algorithm is developed against version 2.6.3 of Agda5 and applied on version 1.7.2 of the Agda standard library6 an open-source, community-developed collection of definitions and proofs for general purpose coding and proving with Agda. Footnote 6 provides a URL: https://github.com/agda/agda-stdlib/releases/tag/v1.7.2. It also mentions Unimath [Rijke et al.] and Type Topology [Escard o and contributors] Agda libraries for additional evaluation sets, both with citations. |
| Dataset Splits | Yes | We fix an 85%-15% training-evaluation split over the 818 files extracted from the Agda standard library. and this amounts to 481 training and 92 evaluation files, counting 15,244 and 4,120 holes respectively. |
| Hardware Specification | Yes | We train on a single A100 for 100 epochs |
| Software Dependencies | No | The extraction algorithm is developed against version 2.6.3 of Agda5. While Agda's version is specified, other software dependencies like PyTorch, used implicitly through mentions of Adam W and other components, are not explicitly listed with their versions. |
| Experiment Setup | Yes | We extensively detail our exact experimental setup in Appendix B. Concisely, we train using Info NCE on a size-constrained subset of the Agda standard library. and Table 2: Hyperparameter setup which includes detailed model and optimization hyperparameters. |