关键字: [Amazon Web Services re:Invent 2024， 亚马逊云科技， Bedrock Guardrails， Automated Reasoning Checks， Factual Accuracy， Soundness， Transparent Explanations， Responsible Ai Applications]
导读亚马逊云科技在Amazon Bedrock Guardrails中推出了自动推理（AR）检查。在本次会议中，了解AR如何通过AR Check（一种新的Amazon Bedrock Guardrails策略）帮助构建透明、负责任的生成式AI应用。该策略使用可靠的数学技术来减少幻觉、验证生成式AI响应，并以可审核的方式解释它们。了解Amazon Bedrock Guardrails策略如何帮助用户在高度监管的主题上生成更准确的LLM响应，如操作工作流程、人力资源政策等。学习AR检查的不同使用场景，以及如何立即开始使用。
演讲精华以下是小编为您整理的本次演讲的精华。
在人工智能领域，一个关键时刻在亚马逊云科技 re:Invent 2024大会上展开，亚马逊云科技产品经理Stefano和杰出科学家Byron共同推出了一项突破性功能，名为Automated Reasoning检查。这一创新解决方案内置于Bedrock Guardrails套件中，旨在解决行业面临的最紧迫挑战之一:大型语言模型(LLM)经常出现的事实错误或幻觉。
Stefano首先回顾了导致这一突破的历程。随着生成式人工智能的兴起，95%的首席信息官认识到它有可能彻底改革客户支持并提高生产力。然而，当组织热切拥抱LLM时，他们遇到了一个严峻障碍——模型容易出现细微的幻觉，导致其输出无法用于面向客户的应用。
为了说明这一问题的严重性，Stefano举了一个生动的例子。他让一个LLM将一段文字浓缩为一个句子，虽然模型抓住了原文的本质，但却幻想出一个细节，错误地声称这段友谊是通过解决“Advent of Code谜题”而巩固的。这种看似无伤大雅的不准确之处凸显了在关键应用中依赖LLM的危险，因为这些应用对精确性有很高要求。
对幻觉的担忧在整个行业引起共鸣，2022年的一项调查显示，高达59%的受访者将其列为使用LLM面临的主要挑战，较2025年的24%有显著增加。然而，Stefano迅速澄清，他仍然是LLM的坚定拥护者，认识到它们巨大的潜力，并将幻觉视为一种可取的特质，有助于培养创造力并使人们能够委派复杂、模糊的决策。
正是在准确性和创造力之间寻求微妙平衡，催生了Automated Reasoning检查功能。Stefano概述了这一突破性功能所依赖的三大核心优先事项:准确识别事实陈述并提出更正建议;在面对错误陈述时保持理性，选择承认缺乏理解而不是验证错误(soundness);通过提供数学可证的解释，确保决策的透明度(transparency)。
杰出科学家Byron随后上台，深入探讨Automated Reasoning的内在机理，这一学科也被称为符号人工智能或形式化验证。他阐明了Automated Reasoning与机器学习的根本区别:后者是基于从数据中学习，而Automated Reasoning能够同时准确讨论所有可能的数据，即使是无限集合。
为了说明这一概念，Byron举了一个Python循环的例子，展示了Automated Reasoning如何仅在几毫秒内就证明循环会终止，这是通过穷举测试无法实现或计算量过大的壮举。这一非凡成就是通过将程序翻译成形式逻辑，并采用Satisfiability Modulo Theory (SMT)求解器来推理无限可能状态集合而实现的。
Stefano随后展示了Automated Reasoning检查在Bedrock Guardrails套件中的实际应用。该工具能够从自然语言策略中提取规则和变量，将它们翻译成形式逻辑，并检查一致性。用户可以使用自然语言与工具交互，系统会无缝地将查询翻译成形式逻辑，并为其有效性决策提供解释。
一个现场演示突出展示了Automated Reasoning检查的强大功能。该工具能够根据提取的规则验证或否定回答，提供未陈述的假设或更正建议，并提供可审计的推理过程日志。这种透明度是该功能的基石，使用户能够审查和理解每个有效性决策背后的基本原理。
Stefano强调，Automated Reasoning检查的反馈可以通过多种方式加以利用，例如提示LLM重写答案、以程序方式注释答案，或生成澄清问题或表单以收集缺失信息。这种灵活性使开发人员能够根据具体用例和要求，量身定制Automated Reasoning检查的集成方式。
在整个演讲过程中，Stefano和Byron都强调Automated Reasoning检查在验证可归结为是/否或总是/从不的事实知识方面的适用性，例如人力资源政策、法律、法规和操作流程。相反，他们承认这种方法在处理定性用例、概率计算或开放式描述时存在局限性，因为固有的模糊性使形式化验证的效力降低。
随着会议临近尾声，Stefano重申了Automated Reasoning检查的总体目标:赋予开发人员构建准确、合理和透明的人工智能应用程序的能力。通过利用符号人工智能技术，这一突破性功能旨在根据知识库的形式化表示来验证LLM响应的事实准确性，在创造力和精确性之间寻求微妙的平衡。
Stefano和Byron为与会者留下了丰富的资源，包括深入探讨Automated Reasoning和Bedrock Guardrails套件内部细节的链接。他们邀请大家加入Guardrail预览计划，鼓励与会者通过他们的亚马逊云科技账户团队着手开启这一变革性的旅程。
在不断演进的人工智能领域，Automated Reasoning检查的推出标志着一个重要里程碑，见证了不懈的创新追求和对负责任人工智能的坚定承诺。当组织应对幻觉带来的挑战时，这一突破性功能为他们指明了希望之路，一条通往充分发挥生成式人工智能潜力的道路，同时坚守事实准确性和透明度的最高标准。
下面是一些演讲现场的精彩瞬间：
演讲者概述了本次会议的结构，包括分享这个想法背后的故事、介绍自动推理检查、由Byron深入探讨该技术、进行实际演示，并留出时间进行问答环节。
演讲者分享了他们探索生成式人工智能、教育领导层以及确定员工入职培训、客户支持和自动化复杂决策等使用案例的经历。
Andy Jassy在reInvent2024演讲中强调，对于人工智能系统的自动推理检查，事实准确性、合理性和透明度至关重要。
他强调了人工智能语言模型在处理事实知识与定性和概率任务方面的优势和局限性。
亚马逊云科技利用SMT求解器(用于符号人工智能和无限域推理的现成工具)来自动验证程序和服务的属性。
在一段引人入胜的叙述中，Stefano和Byron揭示了Automated Reasoning Checks的力量，这是亚马逊云科技 Bedrock Guardrails中一项开创性的功能。这项创新技术利用符号人工智能和形式逻辑原理，确保大型语言模型(LLM)输出的事实准确性，解决了困扰人工智能行业的关键问题——幻觉。
Stefano回顾了导致这一突破的历程，源于意识到尽管LLM非常有创造力，但它们的幻觉在需要准确性的情况下构成了重大挑战。Automated Reasoning Checks旨在实现平衡，保留LLM的创造力，同时确保事实正确性，使其非常适合人力资源政策、法律和操作流程等领域。
Byron深入探讨了自动推理的复杂性，通过编码示例说明了其强大功能，揭示了它如何能在仅仅几毫秒内数学证明关于无限集的断言——这是通过穷尽测试无法实现的壮举。他解释了自动推理如何弥合机器学习和符号人工智能之间的差距，为neuro-symbolic AI铺平了道路，这是这两个学科的融合。
然后，Stefano演示了Automated Reasoning Checks的实际应用，展示了它如何根据预定义的策略验证LLM输出、识别未陈述的假设或事实错误，并提供透明的解释。这种反馈使开发人员能够完善LLM响应、以编程方式对其进行注释或生成澄清问题，确保交付准确可靠的人工智能应用程序。
最后，Stefano和Byron强调了他们致力于实现准确、可靠和透明的人工智能解决方案的承诺，并为与会者留下了宝贵的资源，以进一步探索自动推理并加入Bedrock Guardrails预览。
亚马逊云科技（Amazon Web Services）是全球云计算的开创者和引领者。提供200多类广泛而深入的云服务，服务全球245个国家和地区的数百万客户。做为全球生成式AI前行者，亚马逊云科技正在携手广泛的客户和合作伙伴，缔造可见的商业价值 – 汇集全球40余款大模型，亚马逊云科技为10万家全球企业提供AI及机器学习服务，守护3/4中国企业出海。
