Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
本文提出了一种针对受控执行的机械化代数语义，该语义使用交互树和共归纳法在 32 个 Rocq 模块中形式化，建立了一个对称幺半范畴，其中治理被公理化、具有组合性且与可表达性同终，从而确保所有可构造程序均受治理，同时保持图灵完备性并排除未中介的输入/输出。
原始论文根据 CC0 1.0（http://creativecommons.org/publicdomain/zero/1.0/）发布到公有领域。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在构建一个能够思考、交谈、记忆事物，甚至能走出家门去采购杂货或给朋友打电话的复杂机器人。你希望这个机器人极其聪明且能力出众，但同时必须确保它在执行任务时，绝不会做出任何危险、违法或违反规则的事情。
本文提出了一种为这类机器人设计“大脑”和“规则”的新方法。作者并非仅仅寄希望于机器人会表现良好，而是在其行动周围构建了一座数学堡垒。他们将此称为“受控执行”（Governed Execution）。
以下是他们核心思想的分解，辅以简单的类比：
1. 问题：人工智能的“狂野西部”
目前，我们主要通过两种方式控制人工智能：
- “过滤器”方法： 我们训练人工智能变得礼貌，或者在其发言后过滤其回答。这就像试图通过拖地来止住漏水的水龙头。它无法阻止水流出，只是试图事后清理。
- “护栏”方法： 我们在机器人周围设置围栏。但通常，这些围栏只是建议或软性规则，机器人可能会意外（或故意）跨越它们。
作者认为，我们需要一种系统，其中的规则被硬编码进机器人行动能力的本质结构中。如果机器人试图在未获许可的情况下行动，它在字面意义上就无法做到。
2. 解决方案：“三脚凳”（代数）
作者创建了一个名为治理代数（Governance Algebra）的数学框架。将其想象为一个三脚凳，只有三条腿完美平衡，系统才能运作。如果缺少任何一条腿，整个结构就会倒塌。这三条腿是：
- 安全性： 机器人必须在获得“许可单”（即治理检查）后，才能采取行动。
- 透明性： 如果机器人确实获得了许可，规则不应改变它做什么，而只应确保它先进行了检查。（它不应减慢机器人的速度或改变其回答，仅确保其安全）。
- 恰当性： 规则必须具有一致性。如果两个机器人做同样的事情，规则必须以完全相同的方式对待它们。
3. “交互树”：机器人的思维过程
为了证明这行之有效，他们将机器人的思维表示为一棵巨大的树。
- 树枝： 每次机器人思考时，它都会分叉成树枝。
- 树叶： 最终的动作（例如“给朋友打电话”或“写入文件”）。
- 树干： 机器人到达那里所走的路径。
在他们的系统中，这棵树的每一个分支在生长之前，都必须通过一道安全门（即治理算子）。如果某个分支试图不经过安全门就生长，这棵树将直接拒绝存在。
4. “双重保障”：ID 徽章与保安
本文引入了一种巧妙的两部分安全系统：
- ID 徽章（能力）： 在机器人开始行动之前，它会获得一张 ID 徽章，上面列明了它被允许执行的确切操作（例如：“可以读取文件”，“不能删除文件”）。这是一份静态列表。
- 保安（治理）： 随着机器人的移动，一名保安会检查每一步。即使机器人持有 ID 徽章，如果保安认为该特定动作在当下看起来可疑，也会将其拦下。
本文证明，这两者必须同时发生。你不能只依赖 ID 徽章（因为机器人可能会混淆），也不能只依赖保安（因为保安可能会遗漏某些内容）。它们协同工作，确保每一个动作都既经过授权又经过检查。
5. “共界边界”：完美匹配
这是本文最令人兴奋的部分。作者证明了一个“完美匹配”定理。
- 主张： 在他们的系统中，机器人能够构建的一切自动就是安全的。
- 类比： 想象一个玩具工厂，你只能建造那些附带安全证书的玩具。你无法意外地制造出不安全的玩具。如果某样东西不安全，工厂机器甚至不会让你开始建造它。
- 结果： “安全”区域和“可能”区域的大小完全相同。不存在机器人可以冒险行事的“灰色地带”。如果机器人能够表达一个想法或执行一个动作，那么它必然受到治理。
6. “黑盒”证明
作者不仅写下了这些内容，还使用名为 Rocq 的工具构建了一个庞大的数字证明机器，包含超过 12,000 行代码和 454 个数学证明。
- 他们证明，如果遵循他们的规则，机器人不可能意外地做出坏事。
- 他们证明，机器人仍然足够聪明，可以执行复杂任务（它是“图灵完备”的，意味着它可以解决计算机能解决的任何问题）。
- 他们甚至构建了一个“账本”（类似于防篡改日记），记录每一次许可检查和行动，因此如果任何人日后试图作弊，日记将证明其行径。
总结
本文指出：“我们为人工智能的行动构建了一个数学牢笼。在这个牢笼内，人工智能可以随心所欲地做任何事，但在物理上它不可能做出任何不安全的事情。规则不仅仅是建议；它们是这一特定系统的物理定律。”
他们已在数学上证明了这一点，通过数百万个随机场景进行了测试，并表明“安全”版本的人工智能与“不安全”版本的工作速度一样快。这是一种在不使人工智能变得危险的前提下，使其变得强大的方法。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。