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, 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.
Code (2)
Similar Papers 제목 키워드 기반
Neuron: Learning Context-Aware Evolving Representations for Zero-Shot Skeleton Action Recognition
Zero-shot skeleton action recognition is a non-trivial task that requires robust unseen generalization with prior knowledge from only seen classes and shared semantics. Existing methods typically build the skeleton-seman…
Action RecognitionNARA: Anchor-Conditioned Relation-Aware Contextualization of Heterogeneous Geoentities
Geospatial foundation models have primarily focused on raster data such as satellite imagery, where self-supervised learning has been widely studied. Vector geospatial data instead represent the world as discrete geoenti…
Self-Supervised LearningRepresentation LearningAn Empirical Study of Span Representations in Argumentation Structure Parsing
For several natural language processing (NLP) tasks, span representation design is attracting considerable attention as a promising new technique; a common basis for an effective design has been established. With such ba…
Semi-Supervised Deep Learning for Multiplex Networks
Multiplex networks are complex graph structures in which a set of entities are connected to each other via multiple types of relations, each relation representing a distinct layer. Such graphs are used to investigate man…
Deep LearningRepresentation LearningDoes BERT agree? Evaluating knowledge of structure dependence through agreement relations
Learning representations that accurately model semantics is an important goal of natural language processing research. Many semantic phenomena depend on syntactic structure. Recent work examines the extent to which state…
Sensitivity