arXiv:2505.00622v1 交叉类型 摘要：随着机器学习在自主系统中的应用越来越广泛，神经网络控制器的验证已经成为一个活跃的研究领域。现有的工具和年度验证竞赛表明，这项技术很快就会在实际应用中取得成效。我们的应用源自微飞器领域，这些微飞器被动地由风携带，可能在天气或污染监测方面有多种用途。具体来说，我们研究了模仿Alsomitra macrocarpa散布体的厘米级生物启发滑翔无人机。在本文中，我们提出了一种新的案例研究，旨在验证基于神经网络控制器的Alsomitra启发式无人机，以严格遵循目标轨迹。我们证明了我们的系统与现有的VNN和ARCH竞赛基准存在显著差异，并表明结合使用工具对未来验证此类系统充满希望，前提是某些缺点能够得到克服。我们提出了一种用于稳健训练回归网络的新方法，并在Vehicle和CORA中研究了该案例研究的形式化。我们的验证结果表明，所研究的训练方法确实会提高该应用中神经网络控制器的性能和鲁棒性，但在范围和实用性方面仍有限制。这主要是由于Vehicle和CORA两者的系统性局限性以及我们系统的复杂性限制了可达性的规模，而这在本文中得到了详细研究。如果这些局限性能够克服，这将使工程师能够开发出安全且可靠的可提高人们生活质量并减少我们对环境影响的技术。