Amazon Science

Amazon is investing in the Lean Focused Research Organization

8.5内容质量

TL;DR · AI 摘要

亚马逊投资Lean Focused Research Organization推动Lean编程语言发展，通过数学证明确保AI代理安全性和软件正确性。

核心要点

  • 亚马逊为Lean FRO提供长期资金支持，推动Lean编程语言的全球普及。
  • Lean已应用于Bedrock AgentCore、SampCert和AWS Neuron等关键产品，验证分布式协议正确性。
  • 亚马逊通过独立FRO确保透明度，允许外部验证AI安全关键应用的证明工具。

结构提纲

按章节快速跳转。

  1. §投资背景

    亚马逊因AI代理承担高风险决策而投资Lean FRO，传统测试方法已不适用。

  2. ·Lean编程语言

    Lean通过数学证明确保软件正确性，支持大规模现代软件验证。

  3. ›应用案例

    Lean被用于Bedrock AgentCore安全验证、SampCert隐私保证和AWS Neuron芯片编译。

  4. ·投资模式

    亚马逊通过独立FRO而非内部开发，确保透明度和可信度。

思维导图

用一张图看清主题之间的关系。

查看大纲文本（无障碍 / 无 JS 友好）
  • Lean编程语言在AI安全中的应用
    • 亚马逊投资FRO
      • 长期资金支持
      • 独立组织确保透明度
    • 核心优势
      • 数学证明软件正确性
      • 支持分布式协议验证
    • 应用领域
      • AI代理安全
      • AI芯片编译
      • 隐私保证

金句 / Highlights

值得收藏与分享的关键句。

#Lean#AI安全#亚马逊#编程语言
打开原文

亚马逊正在投资 Lean 专注研究组织 - 亚马逊科学

自动化推理

亚马逊正在投资 Lean 专注研究组织

随着 AI 代理承担更高风险的决策，Lean 编程语言使得能够通过数学证明其行为安全成为可能。

作者

Byron Cook

,

Shawn Bice

2026 年 7 月 26 日

2 分钟阅读时间

分享

  • 复制链接
  • 邮件
  • X
  • 领英
  • Facebook
  • Line
  • Reddit
  • QZone
  • 新浪微博
  • 微信
  • WhatsApp

分享到微信

x

关键要点

  • 亚马逊为 Lean 专注研究组织（FRO）提供长期的财务支持，以推动 Lean 的发展，这是一种能够实现软件正确性数学证明的编程语言。
  • 亚马逊在多个产品中使用基于 Lean 的验证技术，包括用于代理安全的 Bedrock AgentCore、用于差分隐私保证的 SampCert 以及用于 AI 芯片编译的 AWS Neuron，科学家们使用 LLM-Lean 组合来证明复杂分布式协议的正确性。
  • 亚马逊通过独立的 Lean FRO 而非内部开发支持 Lean 的发展，以确保透明度和可信度，使客户、审计师和监管机构能够独立验证安全关键型 AI 应用的证明工具。

这个回答有帮助吗？

我们想向您介绍一项投资以及我们为什么对此感到兴奋。随着 AI 代理越来越多地做出涉及资金流动、理赔批准和关键基础设施运营的决策，传统的软件测试方法已不再足够。测试只能检查您想到的情况，但有一种根本不同的方法：数学证明，它能够确定无论系统接收到什么输入，系统都不会表现出错误行为。

Lean 是一种编程语言，有潜力在现代软件规模上使正确性证明变得实用。现在，亚马逊正在为构建它的团队——Lean 专注研究组织（FRO）——提供大量且长期的财务支持，使证明技术能够为全球每位开发者所用。这是 FRO 历史上最大的一笔捐赠。

Lean 专注研究组织正在构建使现代软件规模的数学证明变得实用的工具。

Lean 已在数学、计算机科学、物理学和其他许多领域催生了一个充满活力的用户社区。它促成了 Mathlib 的诞生，这是一个全面的数学形式化库，激发了形式化证明的进一步努力。它在 AI 推理能力的发展中也发挥了关键作用：Lean 中形式化证明的 AI 生成已成为训练低错误率模型的关键方法，以至于它们现在能够正确解决研究级问题。

但对我们亚马逊而言，Lean 最令人兴奋的是它在代理安全和神经符号 AI 方面的潜在作用：将生成式 AI 与 Lean 的数学严谨性相结合，将有助于实现经过验证且值得信赖的 AI 代理。Lean 团队在行业跟上之前就推动了这一愿景，而这一愿景对我们自身的代理安全战略变得越来越重要。例如，Amazon Bedrock AgentCore 中的 Policy 使用基于 Lean 的验证技术来证明保持 AI 代理在指定边界内的策略语言的正确性。我们尚未看到其他任何人提供这种类型的数学保证。

Lean 还支撑着诸如 SampCert（数学保证 AWS Clean Rooms 的差分隐私保护机制有效）和 AWS Neuron（编译到亚马逊 AI 加速芯片）等系统的正确性证明。最近有科学家使用结合 Lean 的大语言模型（LLM），在远少于手动验证所需的时间内证明了 Amazon Aurora 的段修复协议的正确性，而该协议是我们最关键的分布式协议之一，对数据持久性要求最高。应用范围正在迅速扩展，这仅仅是开始。

Lean 语言如何将数学引入编程，又将编程引入数学

该函数式编程语言的应用包括形式化数学、软件和硬件验证、数学与代码合成的人工智能，以及数学和计算机科学教育。

你可能会好奇，为什么亚马逊希望在 FRO（亚马逊外部）开发 Lean？答案是：当你能够亲自评估证明背后工具时，更容易信任这些证明。客户、审计师和监管机构可以独立检查和验证社区治理工具中的工作成果，这种透明度正是安全关键型 AI 所必需的。

这在内部同样重要。随着开发者社区（包括我们的工程师）的壮大，Lean 的实用性也随之提升，为所有人提供更多的库、更多的工具以及更多形式化证明。出于这两个原因，我们发现 Lean 的基础研究必须通过 Lean 专注研究组织（Lean Focused Research Organization）在开放环境中进行。

研究领域

  • 自动推理

标签

  • 形式化验证
  • 负责任的人工智能
  • 大语言模型（LLMs）
  • 生成式 AI
  • 亚马逊云服务（AWS）

关于作者

亚马逊副总裁兼杰出科学家 Byron Cook 是形式化验证领域的领军人物，因其在 SAT、SMT 和符号模型检测方面的贡献而闻名，这些技术已应用于生物系统、计算机操作系统、编程语言和安全领域。Byron 在亚马逊的自动推理工作，使云服务的安全性达到更高水平，并带来了新的客户功能。

亚马逊云服务副总裁 Shawn Bice 领导 AI 服务和自动推理团队。Shawn 推动科学和产品团队将神经符号 AI（结合大语言模型与形式化验证）引入开发者工具，使每位开发者都能构建具有可证明正确性的可信 AI 代理。