AWS 自动推理检查：一场有赞助的政策验证演示

自动推理使用形式逻辑分析陈述，实现复杂政策可能需要大量专家工作。在这段 2024 年与 AWS 合作的视频中，我介绍一项旨在降低相关工作门槛的预览功能。

语言模型可以辅助编程和处理自然语言，但也可能产生幻觉。我想知道形式化检查能否帮助依据明确规则评估回答，尤其是在错误后果严重的场景中。

一个简单例子是：如果下雨意味着地面潮湿，而地面潮湿意味着轮胎抓地力下降，就可以串联这些蕴含关系。实际政策系统包含更多条件、例外和相互影响。

航空公司退款政策可能有很多页资格规则。访问控制政策也涉及许多服务和权限；建模或实现出错可能带来严重后果。

我转述 Amazon 对 IAM 权限推理系统建设的描述：它涉及逻辑学家、工程师、数年工作和大量开支。这是对该特定项目的描述，并非对所有形式化验证项目的衡量。

挑战在于用概率模型帮助构建规则，再用形式逻辑进行检查。数学证明能在给定形式化规则和假设下确立结论，但本身不能证明翻译后的规则完全符合原始文件。

AWS 在 re:Invent 宣布了 Amazon Bedrock Guardrails 中的 Automated Reasoning checks 预览版。我介绍如何利用自然语言政策提出变量和逻辑规则，供后续测试。

我的例子是一项带薪休假政策，其中的资格条件涉及雇佣状态、职级和任期等。演示文件虽然简短，真实政策却可能包含相互影响的限制和例外。

我上传政策文件，说明预期用途是回答员工的资格问题。演示中的政策创建界面会从源文件中提取候选规则和变量。

生成的政策列出了规则和带类型的变量。检查这些提取结果很重要：如果遗漏或错误翻译了条件，对形式化政策而言合乎逻辑的结论仍可能歪曲原文。

我测试一个声称临时承包人员符合资格的答案。工具将答案标为无效，并展示相关条件和变量，供人检查推理依据。

解释还假设了问题中没有说明的员工职级。我修改变量描述，要求明确给出职级，而不是作出这一假设，然后再次测试。

兼职承包人员的例子因不满足全职要求而被标记，我也展示了一个正面测试。这些例子说明，政策测试和人工审查可以发现表述中的假设或不足。

我乐观地认为自然语言辅助能够减少构建形式规则的工作量。但视频中关于接近完美真实性的更广泛说法需要谨慎看待：准确性取决于政策、转换、输入和检查范围。

我将这种方法与上下文依据或检索进行比较。后者可以提供来源材料，却不会自动根据形式规则证明结论。两种方法用途不同，输入或解释出错时都可能失败。

最后，我请观众查看 AWS 公告，并感谢 AWS 的合作。展示的功能在当时处于预览阶段；这个演示不能保证所有幻觉都会消失。