机器推理面临的三大挑战
生成式AI使得过去几年成为了我30多年机械推理生涯中最令人振奋的时期。为什么？因为计算机行业甚至普通大众现在都渴望讨论我们这些从事逻辑研究的人多年来一直热衷的理念。语言、语法、语义、有效性、可靠性、完备性、计算复杂性甚至不可判定性等挑战，过去对大众来说太过学术和晦涩。但这一切都改变了。对于那些刚刚发现这些主题的人：欢迎！请进，我们渴望与您合作。
我认为分享在AI系统（例如基于生成式AI的聊天机器人）中实现正确推理时最棘手的三个方面会很有用。事实上，Bedrock Guardrails中自动推理检查功能的推出正是受到这些挑战的推动。但我们远未完成：由于这些问题的固有难度，我们作为一个社区（以及我们自动推理检查团队）将在未来数年持续应对这些挑战。
挑战一：从自然语言到结构化语言的转换
人类通常使用不精确和模糊的语言进行交流。我们常常能够从上下文中推断出消除歧义的细节。在某些真正重要的情况下，我们会尝试相互澄清（“你的意思是…"）。而在其他情况下，即使我们真的应该澄清，我们也不会这样做。
这常常是混淆和冲突的根源。想象一下，雇主将员工HR福利的资格定义为"拥有0.2全职等效（FTE）或以上的雇佣合同”。假设我告诉你我"花费20%的时间在工作上，除了去年我请假帮助家人从手术中恢复的那段时间"。我有资格获得福利吗？当我说"花费20%的时间在工作上"，这是否意味着根据合同条款，我花费了20%的工作时间？
我的陈述有多种合理的解释，每种解释对福利资格都有不同的结果。我们在自动推理检查中做的一件事是使用互补方法，多次尝试在自然语言和查询谓词之间进行转换。这是一种常见的访谈技巧：以不同方式询问相同信息，看看事实是否保持一致。在自动推理检查中，我们使用形式逻辑系统的求解器来证明/反驳不同解释的等价性。如果翻译在语义层面存在差异，使用自动推理检查的应用程序可以要求澄清（例如"您能确认您拥有20%或以上全职工作的雇佣合同吗？"）。
自动推理检查使用大型语言模型生成自然语言到形式语言的几种可能翻译。自动推理检查会标记翻译之间的差异，客户可以通过自然语言交互解决这些差异。
挑战二：定义真理
让我始终感到惊讶的是，群体在规则含义上达成共识有多么困难。复杂的规则和法律常常包含细微的矛盾，这些矛盾可能一直未被注意，直到有人试图就它们的解释达成共识。例如，英国1988年的《版权、设计和专利法》包含一个内在矛盾：它将可版权作品定义为源自作者原创智力创作的作品，同时为不需要创造性人类输入的作品提供保护——这种不一致在AI生成作品的时代尤其明显。
第二个麻烦来源是我们似乎总是在改变规则。例如，美国联邦政府的每日津贴率每年都会变化，这需要不断维护依赖这些值的任何系统。
最后，很少有人真正深入了解他们应该遵守的所有规则的边界情况。考虑驾驶时戴耳机的问题：在美国某些州（例如阿拉斯加）这是非法的；在某些州（例如佛罗里达）只戴一个耳机是合法的；而在其他州（例如德克萨斯）实际上这是合法的。在一项非正式调查中，我的朋友和同事中很少有人对他们最近驾驶汽车的地方关于驾驶时戴耳机的合法性有自信的理解。
自动推理检查通过帮助客户在其感兴趣的领域（无论是税法、HR政策还是其他规则系统）定义真理应该是什么，并提供随着规则变化而随时间完善这些定义的机制，来应对这些挑战。随着基于生成式AI的聊天机器人的出现，让我们许多人着迷的一个想法是，复杂的规则系统可以通过自然语言查询向普通大众开放。未来，聊天机器人可以直接且易于理解地回答诸如"在日本东京驾驶时可以掉头吗？“这样的问题，而通过应对定义真理的挑战，自动推理检查可以帮助确保答案是可靠的。
挑战三：确定性推理
想象我们有一套规则（我们称之为R）和一个我们想要验证的陈述（S）。例如，R可能是新加坡的驾驶法规，S可能是关于新加坡交叉路口掉头的问题。我们可以通过以各种方式组合布尔变量，将R和S编码成计算机理解的布尔逻辑。
假设编码R和S只需要500位——大约63个字符。这是极少量的信息！但即使我们对规则系统的编码小到可以放入一条短信中，我们需要检查的场景数量也是天文数字。原则上，我们必须考虑所有2^500种可能组合，才能权威地声明S为真陈述。如今一台强大的计算机在您眨眼的时间内可以执行数亿次操作。但即使我们拥有世界上所有的计算机以这种极速运行，从时间开始到现在，我们仍然远未检查完所有2^500种可能性。
幸运的是，自动推理社区已经开发了一类称为SAT求解器的复杂工具，使得这种组合检查在许多（虽然不是所有）情况下成为可能且非常快速。自动推理检查在检查陈述有效性时使用这些工具。
不幸的是，并非所有问题都能以发挥SAT求解器优势的方式进行编码。例如，想象一个规则系统有这样的规定：“如果每个大于2的偶数都是两个质数之和，则预扣税率为30%；否则为40%"。问题在于，要知道预扣税率，你需要知道是否每个大于2的偶数都是两个质数之和，而目前没有人知道这是否为真。这个陈述被称为哥德巴赫猜想，自1742年以来一直是一个未解决的问题。虽然我们不知道哥德巴赫猜想的答案，但我们知道它要么为真要么为假，所以我们可以明确地说预扣税率必须是30%或40%。
思考自动推理检查的客户是否可能定义一个依赖于自动推理检查输出的策略也很有趣。例如，策略能否编码规则"当且仅当自动推理检查说不允许时，才允许访问”？在这里，没有正确的答案是可能的，因为该规则通过递归引用其自身的检查过程创造了矛盾。我们最多只能回答"未知”（事实上，自动推理检查在这种情况下会这样回答）。
像自动推理检查这样的工具对此类陈述既不能返回"真"也不能返回"假"的事实，最早由库尔特·哥德尔在1931年发现。我们从哥德尔的结果知道，像自动推理检查这样的系统不能同时具备一致性和完备性，所以它们必须选择其一。我们选择了一致性。
这三个困难——将自然语言转换为结构化逻辑、在不断变化且有时矛盾的规则背景下定义真理，以及应对确定性推理的复杂性——不仅仅是我们尝试构建具有健全推理的AI系统时面临的技术障碍。它们是深深植根于我们技术局限性和人类系统复杂性的问题。
随着2025年8月6日在Bedrock Guardrails中推出自动推理检查，我们通过结合互补方法来应对这些挑战：应用交叉检查方法从模糊的自然语言转换为逻辑谓词，提供灵活框架帮助客户开发和维护规则系统，以及在使用复杂SAT求解器的同时仔细处理无法获得明确答案的情况。在我们努力改进产品在这些挑战上的性能时，我们不仅是在推进技术，还在深化对塑造推理本身的基本问题的理解，从哥德尔的不完备性定理到法律和政策框架的不断演变性质。
鉴于我们对提供健全推理的承诺，AI领域的前路充满挑战。我们接受挑战！