Learning-based congestion controllers offer better adaptability compared to traditional heuristic algorithms. However, the inherent unreliability of learning techniques can cause learning-based controllers to behave poorly, creating a need for formal guarantees. While methods for formally verifying learned congestion controllers exist, these methods offer binary feedback that cannot optimize the controller toward better behavior. We improve this state-of-the-art via C3, a new learning framework for congestion control that integrates the concept of formal certification in the learning loop. C3 uses an abstract interpreter that can produce robustness and performance certificates to guide the training process, rewarding models that are robust and performant even on worst-case inputs. Our evaluation demonstrates that unlike state-of-the-art learned controllers, C3-trained controllers provide both adaptability and worst-case reliability across a range of network conditions.

翻译：相较于传统启发式算法，基于学习的拥塞控制器展现出更优的适应性。然而，学习技术固有的不可靠性可能导致学习型控制器表现不佳，这催生了对形式化保证的需求。虽然形式化验证已习得拥塞控制器的方法存在，但这些方法仅能提供二元反馈，无法引导控制器优化至更优行为。我们通过C3改进了这一现状——这是一个将形式化认证概念融入学习循环的新型拥塞控制学习框架。C3采用能够生成鲁棒性与性能证书的抽象解释器来指导训练过程，奖励即使在最坏输入条件下仍保持鲁棒与高性能的模型。评估结果表明，与现有先进的学习型控制器不同，经C3训练的控制器能在各类网络条件下同时提供适应性与最坏情况可靠性。