基于 SMT 的机器人转移修复

状态机是机器人行为的常见模型。转移函数常依赖参数化条件来建模控制器的前置条件，其中参数的正确取值取决于与环境或特定机器人相关的因素。在缺乏特定校准流程的情况下，机器人专家必须通过一系列试错实验费力地调整参数。在此过程中，识别机器人何时采取了错误动作以及应做什么直截了当，但找到正确的参数值可能很困难。我们提出一种称为交互式基于 SMT 的机器人转移修复的替代方法。在执行期间，我们记录转移函数的执行轨迹，并请机器人专家识别少数机器人发生错误转移及正确转移应为何处的实例。用户根据这些待修复错误类型提供修正，系统对轨迹的自动分析针对每次修正部分求值转移函数。该约束系统随后被表述为一个 MaxSMT 问题，其解是对参数的最小调整，以满足最大数量的约束。为识别准确捕捉用户意图并泛化至新颖场景的修复，通过迭代向 MaxSMT 问题添加约束以产生备选修复集合来探索解。我们在包括机器人足球与自动驾驶的多个领域的状态机上测试，并针对求解器选择与优化超参数评估基于求解器的修复。我们的结果表明，SRTR 能够快速、以少量修正修复多种状态机与错误类型，同时不会过度修正状态机而损害泛化性能。