ICMLJun, 2017

使用形式化数学开发无缺陷的机器学习系统

PDF
TL;DR通过可交互的证明助手，开发者能够证明机器学习系统的正确性，这种方法暴露了所有的实现错误，并通过 Certigrad 实现了优化的随机计算图，并生成了一个机器可验证的证明，证明了系统采样的梯度是数学梯度的无偏估计方法。
machine learninginteractive proof assistantsystem correctnesscertigradunbiased estimates
发现论文，激发创造
  • 利用神经网络生成正确性证明

    本文提出了一个使用机器学习技术的证明搜索系统 Proverbot9001，它能够自动化之前需要手动完成的证明，有效地产生了 27.5% 的证明陈述，在 Coq 中产生了 4 倍的提高。

    Jul, 2019

  • 机器学习系统认证的形式和实践要素

    该论文将机器学习应用于自主飞行中的视觉着陆，并建立了一个模型无关且工具独立的认证框架，以解决机器学习模型的可信度与航空认证之间的挑战。

    Oct, 2023

  • 可信的正式自然语言规范

    该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

    Oct, 2023

  • 学习证明：定义与实践

    此研究的目的是实现机器学习中证明训练过程的机制 ——proof-of-learning。作者观察到随机梯度下降算法具有积累秘密信息的性质，并构建了一种自然的证明机制来证明一个实体已经正确地完成了模型参数优化过程，进而保护模型的知识产权。同时，该证明机制也保持了训练过程的可用性，可以在多方争议模型所有权的情况下使用。实验证明，该机制在硬件和软件环境的变化下仍能保持鲁棒性。

    Mar, 2021

  • 关于正式（非）证明学习证明中鲁棒性的根本限制

    本文对 Proof-of-learning（一种基于机器学习的训练检查点建立验证机制）进行了形式化分析，发现其存在容易被攻击者欺骗的漏洞，并提出在保护 Proof-of-learning 的真实性方面需要更多地借助密码学的方法。

    Aug, 2022

  • 强化学习定理证明

    提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

    May, 2018

  • 比较可微分逻辑用于学习系统的研究预览

    通过将背景知识编码为逻辑约束，用可微分逻辑指导学习过程，创造性地满足约束的机器学习模型进行了比较和评估，并提出了未来工作的开放问题。

    Nov, 2023

  • 深度神经网络验证的认证证明检查器

    本文介绍了一种基于 Imandra 的 DNN 验证证明检查器的新实现，该实现通过使用 Imandra 的两个关键功能：无限精度实数算术和形式化验证基础设施来提高数字稳定性和验证性能，并在实现验证正确性属性和性能优化方面继续开展工作。

    Jul, 2023

  • 面向基于机器学习的分布式系统的认证

    本文分析了目前认证方案存在的挑战和不足，讨论了开放的研究问题，并针对基于机器学习的分布式系统提出了第一个认证方案。

    May, 2023

  • 通过高斯过程回归形式化验证未知动态系统

    本文提出了一个基于高斯过程回归的验证框架，将连续空间系统抽象为有限状态不确定马尔可夫决策过程，利用模型检测工具验证抽象的不确定性，并将结果扩展到基础的部分可观测系统，有效地应用于线性、非线性和切换系统等多种情况下。

    Dec, 2021