Learning Structure-Aware Representations of Dependent Types

• URL: http://arxiv.org/abs/2402.02104v2
• Date: Wed, 30 Oct 2024 12:40:30 GMT
• Title: Learning Structure-Aware Representations of Dependent Types
• Authors: Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy,
• Abstract summary: Agda is a dependently-typed programming language and a proof assistant. This paper extends the Agda ecosystem into machine learning territory. We introduce and release a novel dataset of Agda program-proofs.
• Score: 3.7794090250290187
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Federated Retrieval-Augmented Generation: A Systematic Mapping Study [6.108593045873404]
  Federated Retrieval-Augmented Generation (Federated RAG) combines Federated Learning (FL) with Retrieval-Augmented Generation (RAG)<n>RAG improves the factual accuracy of language models by grounding outputs in external knowledge.<n>This paper presents the first systematic mapping study of Federated RAG, covering literature published between 2020 and 2025.
  arXiv  Detail & Related papers  (2025-05-24T23:45:12Z)
• Hadamard product in deep learning: Introduction, Advances and Challenges [68.26011575333268]
  This survey examines a fundamental yet understudied primitive: the Hadamard product. Despite its widespread implementation across various applications, the Hadamard product has not been systematically analyzed as a core architectural primitive. We present the first comprehensive taxonomy of its applications in deep learning, identifying four principal domains: higher-order correlation, multimodal data fusion, dynamic representation modulation, and efficient pairwise operations.
  arXiv  Detail & Related papers  (2025-04-17T17:26:29Z)
• Factored Agents: Decoupling In-Context Learning and Memorization for Robust Tool Use [4.437184840125514]
  We propose a novel factored agent architecture designed to overcome the limitations of traditional single-agent systems in agentic AI. Our approach decomposes the agent into two specialized components: (1) a large language model that serves as a high level planner and in-context learner, and (2) a smaller language model which acts as a memorizer of tool format and output. Empirical evaluations demonstrate that our factored architecture significantly improves planning accuracy and error resilience, while elucidating the inherent trade-off between in-context learning and static memorization.
  arXiv  Detail & Related papers  (2025-03-29T01:27:11Z)
• Generative AI for Software Architecture. Applications, Trends, Challenges, and Future Directions [6.883775050854466]
  We aim to systematically synthesize the use, rationale, contexts, usability, and future challenges of GenAI in software architecture. Our review identified significant adoption of GenAI for architectural decision support and architectural reconstruction.
  arXiv  Detail & Related papers  (2025-03-17T15:49:30Z)
• A Survey of Model Architectures in Information Retrieval [64.75808744228067]
  We focus on two key aspects: backbone models for feature extraction and end-to-end system architectures for relevance estimation. We trace the development from traditional term-based methods to modern neural approaches, particularly highlighting the impact of transformer-based models and subsequent large language models (LLMs) We conclude by discussing emerging challenges and future directions, including architectural optimizations for performance and scalability, handling of multimodal, multilingual data, and adaptation to novel application domains beyond traditional search paradigms.
  arXiv  Detail & Related papers  (2025-02-20T18:42:58Z)
• Deep Learning and Machine Learning -- Object Detection and Semantic Segmentation: From Theory to Applications [17.571124565519263]
  Book covers state-of-the-art advancements in machine learning and deep learning. Focuses on convolutional neural networks (CNNs), YOLO architectures, and transformer-based approaches like DETR. Book also delves into the integration of artificial intelligence (AI) techniques and large language models for enhanced object detection.
  arXiv  Detail & Related papers  (2024-10-21T02:10:49Z)
• Reducing Diversity to Generate Hierarchical Archetypes [2.5069344340760713]
  We present a primitive-based framework to automatically generate hierarchies of constructive archetypes. We prove the effectiveness of our framework through mathematical definitions and proofs.
  arXiv  Detail & Related papers  (2024-09-27T11:06:59Z)
• Pangu-Agent: A Fine-Tunable Generalist Agent with Structured Reasoning [50.47568731994238]
  Key method for creating Artificial Intelligence (AI) agents is Reinforcement Learning (RL) This paper presents a general framework model for integrating and learning structured reasoning into AI agents' policies.
  arXiv  Detail & Related papers  (2023-12-22T17:57:57Z)
• Retrieval-Enhanced Machine Learning [110.5237983180089]
  We describe a generic retrieval-enhanced machine learning framework, which includes a number of existing models as special cases. REML challenges information retrieval conventions, presenting opportunities for novel advances in core areas, including optimization. REML research agenda lays a foundation for a new style of information access research and paves a path towards advancing machine learning and artificial intelligence.
  arXiv  Detail & Related papers  (2022-05-02T21:42:45Z)
• Unified Instance and Knowledge Alignment Pretraining for Aspect-based Sentiment Analysis [96.53859361560505]
  Aspect-based Sentiment Analysis (ABSA) aims to determine the sentiment polarity towards an aspect. There always exists severe domain shift between the pretraining and downstream ABSA datasets. We introduce a unified alignment pretraining framework into the vanilla pretrain-finetune pipeline.
  arXiv  Detail & Related papers  (2021-10-26T04:03:45Z)
• Incorporating Linguistic Knowledge for Abstractive Multi-document Summarization [20.572283625521784]
  We develop a neural network based abstractive multi-document summarization (MDS) model. We process the dependency information into the linguistic-guided attention mechanism. With the help of linguistic signals, sentence-level relations can be correctly captured.
  arXiv  Detail & Related papers  (2021-09-23T08:13:35Z)
• Structure-Aware Feature Generation for Zero-Shot Learning [108.76968151682621]
  We introduce a novel structure-aware feature generation scheme, termed as SA-GAN, to account for the topological structure in learning both the latent space and the generative networks. Our method significantly enhances the generalization capability on unseen-classes and consequently improve the classification performance.
  arXiv  Detail & Related papers  (2021-08-16T11:52:08Z)
• Iterated learning for emergent systematicity in VQA [3.977144385787228]
  neural module networks have an architectural bias towards compositionality. When learning layouts and modules jointly, compositionality does not arise automatically and an explicit pressure is necessary for the emergence of layouts exhibiting the right structure. We propose to address this problem using iterated learning, a cognitive science theory of the emergence of compositional languages in nature.
  arXiv  Detail & Related papers  (2021-05-03T18:44:06Z)
• Few-Shot Named Entity Recognition: A Comprehensive Study [92.40991050806544]
  We investigate three schemes to improve the model generalization ability for few-shot settings. We perform empirical comparisons on 10 public NER datasets with various proportions of labeled data. We create new state-of-the-art results on both few-shot and training-free settings.
  arXiv  Detail & Related papers  (2020-12-29T23:43:16Z)
• Exploring Probabilistic Soft Logic as a framework for integrating top-down and bottom-up processing of language in a task context [0.6091702876917279]
  The architecture integrates existing NLP components to produce candidate analyses on eight levels of linguistic modeling. The architecture builds on Universal Dependencies (UD) as its representation formalism on the form level and on Abstract Meaning Representations (AMRs) to represent semantic analyses of learner answers.
  arXiv  Detail & Related papers  (2020-04-15T11:00:07Z)
• A Dependency Syntactic Knowledge Augmented Interactive Architecture for End-to-End Aspect-based Sentiment Analysis [73.74885246830611]
  We propose a novel dependency syntactic knowledge augmented interactive architecture with multi-task learning for end-to-end ABSA. This model is capable of fully exploiting the syntactic knowledge (dependency relations and types) by leveraging a well-designed Dependency Relation Embedded Graph Convolutional Network (DreGcn) Extensive experimental results on three benchmark datasets demonstrate the effectiveness of our approach.
  arXiv  Detail & Related papers  (2020-04-04T14:59:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.