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.