NRI: Collaborative Research: Modeling and Verification of Language-based Interaction

今天的许多自主系统，如个人或服务机器人，主要设计为独立和孤立地执行任务。将这些机器人与人类合作伙伴集成在一起往往会导致性能低下，因为机器人不知道如何解释人类交互，也无法将来自该交互的信息与保证机器人性能的模型合并。这项研究汇集了刚刚达到足够成熟的集成水平的关键要素：首先，自然语言处理和概率建模来捕获人类输入，其次，对人-机器人组合系统进行概率综合和验证，以确保正确的性能。其结果将是能够实现机器人与人类之间正确、有效和自然互动的理论和软件。这项研究将影响大多数未来需要与人类互动的自主系统，包括服务机器人、个人机器人和行星机器人。本研究的目标是开发用于综合和验证基于自然语言交互的完整的人加机器人系统的模型和算法。正在开发的算法用于自然语言的概率建模和推理，包括将语言的组成部分植根于物理世界和人类的期望。这些模型将允许开发控制综合的规范分布，这反过来将使按结构校正控制器的开发和验证达到特定的概率水平。未来几年将考虑通过人机互动对话来解决冲突，并考虑通过“开放世界”的情景来实现在线学习新模型。预计这项研究将在许多自主系统中实现高可靠性和高性能，因为它与人类的内在交互。成果包括开放源码数据和软件；社区讲习班；以及在独特的机器人语言、建模和验证领域的本科生和研究生教育。

Many autonomous systems today, such as personal or service robots, are designed primarily to perform tasks independently and in isolation. Integrating these robots with human partners can often result in poor performance, as the robot does not know how to interpret human interaction, and cannot merge information from this interaction with a model that guarantees robot performance. This research brings together key elements that are just now reaching a sufficient level of maturity for integration: firstly, natural language processing and probabilistic modeling to capture human input, and secondly probabilistic synthesis and verification of the combined human-robot systems to ensure correct performance. The outcome will be theory and software to enable correct, effective and natural interactions between robots and humans to be realized. This research will impact most future autonomous systems which require interactions with humans, including service, personal and planetary robots. The goal of this research is to develop models and algorithms for synthesizing and verifying an integrated human-plus-robot system based on natural language interaction. Algorithms are being developed for probabilistic modeling and inference of natural language, including the grounding of the constituents of the language into the physical world and the human's expectations. These models will enable the development of a distribution over specifications for control synthesis, which will in turn enable the development and verification of correct-by-construction controllers to a particular level of probability. The out years will consider interactive human-robot dialogue to resolve conflicts, and "open world" scenarios to enable on-line learning of new models over time. It is expected that this research will enable high reliability and performance in many autonomous systems because of the inherent interaction with humans. Outcomes include open source data and software; community workshops; and undergraduate and graduate student education in the unique area of language, modeling and verification for robotics.