Higher-order logic HOL offers a very simple syntax and semantics for
representing and reasoning about typed data structures. But its type system
lacks advanced features where types may depend on terms. Dependent type theory
offers such a rich type system, but has rather substantial conceptual
differences to HOL, as well as comparatively poor proof automation support. We
introduce a dependently-typed extension DHOL of HOL that retains the style and
conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL
and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a
theorem prover for DHOL.

介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。

依赖类型高阶逻辑中的定理证明 —— 扩展预印本

Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended  Preprint

Neural Architecture Search (NAS) algorithms automate the task of finding
optimal deep learning architectures given an initial search space of possible
operations. Developing these search spaces is usually a manual affair with
pre-optimized search spaces being more efficient, rather than searching from
scratch. In this paper we present a new framework called Neural Architecture
Type System (NeuralArTS) that categorizes the infinite set of network
operations in a structured type system. We further demonstrate how NeuralArTS
can be applied to convolutional layers and propose several future directions.

该论文介绍了一种称作神经网络类型系统的新框架，该框架可以将无限的网络操作分类到结构化类型系统中，以便于进行神经架构搜索及优化，并通过卷积层展示了其应用及未来方向。

用类型理论对神经架构搜索进行结构化

NeuralArTS: Structuring Neural Architecture Search with Type Theory

We present a semantic parser for Abstract Meaning Representations which
learns to parse strings into tree representations of the compositional
structure of an AMR graph. This allows us to use standard neural techniques for
supertagging and dependency tree parsing, constrained by a linguistically
principled type system. We present two approximative decoding algorithms, which
achieve state-of-the-art accuracy and outperform strong baselines.

我们提出了一种语义解析器，可以将字符串解析为 AMR 图的组成结构的树形表示，利用语言学原则约束标准神经技术进行超标记和依存树解析。我们提出了两种近似解码算法，实现了最先进的准确度并优于强基线。

带有类型语义代数的 AMR 依存解析

AMR Dependency Parsing with a Typed Semantic Algebra

The wealth of structured (e.g. Wikidata) and unstructured data about the
world available today presents an incredible opportunity for tomorrow's
Artificial Intelligence. So far, integration of these two different modalities
is a difficult process, involving many decisions concerning how best to
represent the information so that it will be captured or useful, and
hand-labeling large amounts of data. DeepType overcomes this challenge by
explicitly integrating symbolic information into the reasoning process of a
neural network with a type system. First we construct a type system, and
second, we use it to constrain the outputs of a neural network to respect the
symbolic structure. We achieve this by reformulating the design problem into a
mixed integer problem: create a type system and subsequently train a neural
network with it. In this reformulation discrete variables select which
parent-child relations from an ontology are types within the type system, while
continuous variables control a classifier fit to the type system. The original
problem cannot be solved exactly, so we propose a 2-step algorithm: 1)
heuristic search or stochastic optimization over discrete variables that define
a type system informed by an Oracle and a Learnability heuristic, 2) gradient
descent to fit classifier parameters. We apply DeepType to the problem of
Entity Linking on three standard datasets (i.e. WikiDisamb30, CoNLL (YAGO), TAC
KBP 2010) and find that it outperforms all existing solutions by a wide margin,
including approaches that rely on a human-designed type system or recent deep
learning-based entity embeddings, while explicitly using symbolic information
lets it integrate new entities without retraining.

DeepType 是一种将符号信息显式地集成到神经网络推理过程中的模型，它通过构建类型系统并将其用于限制神经网络输出的符号结构来解决判断结构以及有效地捕捉信息的问题。在实验中，它用于 Entity Linking 任务，优于人工设计类型系统或最近使用深度学习相似性度量的方案，同时使用符号信息可以无需重新训练即可集成新实体。