Canopy: Property-Driven Learning for Congestion Control

TL;DR

Canopy introduces a property-driven framework that combines learning with formal reasoning to enhance the reliability and adaptability of congestion control algorithms, ensuring safety and robustness in worst-case network scenarios.

Contribution

This paper presents Canopy, a novel framework that integrates formal verification with learning to improve congestion control, providing quantitative certification and worst-case guarantees.

Findings

Canopy-trained controllers outperform existing methods in worst-case scenarios.

The framework achieves a balance between adaptability and reliability.

Formal reasoning guides the learning process for safer controllers.

Abstract

Learning-based congestion controllers offer better adaptability compared to traditional heuristics. However, the 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 Canopy, a new property-driven framework that integrates learning with formal reasoning in the learning loop. Canopy uses novel quantitative certification with an abstract interpreter to guide the training process, rewarding models, and evaluating robust and safe model performance on worst-case inputs. Our evaluation demonstrates that unlike state-of-the-art learned controllers, Canopy-trained controllers provide both adaptability and worst-case reliability across a range of network conditions.