C3: Learning Congestion Controllers with Formal Certificates
This addresses the need for reliable congestion control in networking, offering a solution that combines adaptability with formal guarantees, though it is incremental by building on existing verification methods.
The paper tackles the problem of unreliable learning-based congestion controllers by introducing C3, a framework that integrates formal certification into the learning loop, resulting in controllers that provide adaptability and worst-case reliability across various network conditions.
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.