Introduction
The rapid growth of AI and data-intensive computing has placed enormous pressure on energy consumption.
We target two contributors: first, the inefficiency of the underlying hardware components, such as the architecture of network switches and CPU interconnects; second, the overuse of large models for a significant majority of tasks. This project aims at a sustainable approach: use lightweight AI-guided searches combined with formal methods to discover provably correct, energy-efficient hardware designs.
Designing optimal circuits underlying the core logic of hardware is both important and notoriously difficult. Taking sorting networks as a canonical example. Existing approaches are mostly search-based, and they differ in how the search is guided through the space that is impossible to exhaust in practice. For example, evolutionary approaches [3,4] apply random mutation to candidate networks and select improved descendants to guide the next generation of search. More recently, reinforcement learning (RL)-guided searches such as AlphaDev [5] use neural networks to guide Monte Carlo tree search (MCTS), with discovered faster algorithms integrated into the LLVM standard C++ library. Scalability remains a fundamental limitation: to the best of our knowledge, the sorting networks with the fewest comparators and layers are currently known only up to 12 inputs and 17 inputs, respectively.
The project aims to integrate formal methods into such searching approaches. In the approaches above, correctness is typically checked post-hoc or via execution-based testing. The idea is to seriously integrate formal methods (FM) into the pipeline. Here are some promising ideas: FM can provide semantically grounded intermediate evaluation to densify reward signals, prune provably incorrect branches early for effectiveness, and replace hand-crafted heuristics with principled correctness reasoning. Furthermore, one can use FPGAs to accelerate both the search and verification steps [6], creating a closed loop between design search, formal verification, and real energy measurement.
References:
[1] Knuth, Donald E (1998). The Art of Computer Programming: Sorting and Searching, volume 3.
[2] Bundala, Daniel, and Jakub Závodný (2014). "Optimal sorting networks." International Conference on Language and Automata Theory and Applications.
[3] Koza, John R (1999). Genetic programming III: Darwinian invention and problem solving. Vol. 3.
[4] Valsalam, Vinod K., and Risto Miikkulainen (2013). "Using symmetry and evolutionary search to minimize sorting networks." The Journal of Machine Learning Research.
[5] Mankowitz, Daniel J., et al. (2023). "Faster sorting algorithms discovered using deep reinforcement learning." Nature.
[6] Papaphilippou, Philippos (2026). "Highly Parallel Sorting Network Verification Using FPGAs." Chips.