MMApr, 2021

基于类型 lambda 演算的交互式 shell 方案

PDF
TL;DR本文介绍了 Favalon，一个基于 lambda 演算构建的函数式编程语言，用作交互式 shell 的替代品。Favalon 通过类型推理、灵活的运行时类型元数据和 shells 使用的相同技术，与现有库和命令的类型化版本无缝集成在一起。通过自定义函数，Favalon 的大部分语法可定制化，使得任何熟悉命令行 shell 的人都可以扩展它。此外，Favalon 的类型推理引擎可以分离出其运行时库并轻松地用于其他应用。
发现论文，激发创造
  • FVEL：基于定理证明的大型语言模型互动式形式验证环境

    提出了 FVEL，一种与大型语言模型一起进行交互式形式验证的环境，通过将给定的代码转化为 Isabelle 并利用神经自动定理证明来进行验证，利用 Isabelle 中的规则和定理，通过 FVELER 数据集进行评估，结果表明 FVEL 可在 SV-COMP 中解决更多问题并减少证明错误。

    Jun, 2024

  • 无 Lambda 高阶逻辑叠加

    本研究介绍了反证完成的超位置演算法，用于意图性和外延句子 $\lambda$- 自由高阶逻辑，这两种形式允许部分应用和应用变量。 这些演算法由一个术语排序参数化，无需完全单调，从而可以采用 $\lambda$- 自由高阶词典路径和 Knuth-Bendix 排序。作者们在 Zipperposition prover 中实现了这些演算法，并在 Isabelle/HOL 和 TPTP 基准测试中评估它们。 它们似乎是通向完全高效自动定理证明程序的一个重要的步骤。

    May, 2020

  • 扇贝：神经符号编程语言

    Scallop 是一种结合深度学习和逻辑推理的语言，支持广泛的神经符号应用，并通过基于关系数据模型的灵活符号表示、基于 Datalog 的声明性逻辑编程语言以及基于证明半环理论的自动和高效可微分推理框架来实现这些目标。我们评估了 Scallop 在 8 个神经符号应用程序中的表现，结果表明，Scallop 能够在各种具有挑战性的 AI 任务中表达算法推理，为机器学习程序员提供了简洁的接口来整合逻辑领域知识，并在准确性方面产生与现有最先进模型相当或更优的结果，在运行时间和数据效率、可解释性和泛化性方面的结果均优于这些模型。

    Apr, 2023

  • Julia: 技术计算的快速动态语言

    本篇论文介绍了一种新型动态语言 Julia，它采用现代的编程语言技术进行设计，旨在实现高性能并支持表达式编程模型和成功的类型推断，从而使其适用于科学计算和技术计算领域，并尝试平衡高生产力和高性能。

    Sep, 2012

  • 比较和评估扩展 Lambek 演算

    该论文通过建立 Lambek calculus 的扩展和变体的两个统一框架，利用证明网和图重写规则建立逻辑框架，用于在不同的语言分析框架之间架起桥梁，强调区别，帮助识别问题。

    Jun, 2015

  • 自然演绎作为高阶归结

    开发了交互式定理证明器 Isabelle，以 Horn clause 表示每个推理规则，使用基于类型的 λ 演算表示逻辑语法，支持多个逻辑系统并具有逻辑编程潜能。

    Oct, 2000

  • 使用线性时间微积分理论模拟动态系统

    本文研究在一个规范上执行广泛的推断任务的可行性，通过将 IDP3 扩展到与动态规范相关的领域中使用的多种推断技术。

    May, 2014

  • 反应式概率编程

    本文介绍了 ProbZelus—— 第一种同步概率编程语言，其在控制软件中提供概率结构以建模不确定性，并进行推理，这使得它适用于设计反应式概率应用程序和高效的内存推理。

    Aug, 2019

  • 单子化深度学习

    使用 Scala 语言的 DeepLearning.scala 框架提供了一种创新的自动微分方法，允许用户以直观简洁的方式创建复杂的神经网络，并保持类型安全。

    Jul, 2023

  • 基于 Transformer 模型的简单类型 lambda 演算类型推断：代码深度学习案例研究

    本文探讨了使用 transformer 模型对 typed lambda 演算进行类型推导的问题，并对优化器的选择以及 warm-up 的影响进行了实验，发现 Adafactor 比 Adam 和 RAdam 更有效。

    Mar, 2023