“Lightweight Online Learning for Sets of Related Problems in Automated Reasoning” by Haoze Wu, Christopher Hahn, Florian Matthias Lonsing, Makai Mann, Raghuram Ramanujan, and Clark Barrett. In Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), (Alexander Nadel and Kristin Yvonne Rozier, eds.), Oct. 2023, pp. 23-33. Ames, IA.
We present Self-Driven Strategy Learning (SDSL), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems. SDSL does not require offline training, but instead automatically constructs a dataset while solving earlier problems. It fits a machine learning model to this data which is then used to adjust the solving strategy for later problems. We formally define the approach as a set of abstract transition rules. We describe a concrete instance of the SDSL calculus which uses conditional sampling for generating data and random forests as the underlying machine learning model. We implement the approach on top of the KISSAT solver and show that the combination of KISSAT+SDSL certifies larger bounds and finds more counter-examples than other state-of-the-art bounded model checking approaches on benchmarks obtained from the latest Hardware Model Checking Competition.
BibTeX entry:
@inproceedings{WHL+23,
author = {Haoze Wu and Christopher Hahn and Florian Matthias Lonsing
and Makai Mann and Raghuram Ramanujan and Clark Barrett},
editor = {Alexander Nadel and Kristin Yvonne Rozier},
title = {Lightweight Online Learning for Sets of Related Problems in
Automated Reasoning},
booktitle = {Proceedings of the {\it 23^{rd}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '23)},
pages = {23--33},
publisher = {TU Wien Academic Press},
month = oct,
year = {2023},
doi = {10.34727/2023/isbn.978-3-85448-060-0_10},
note = {Ames, IA},
url = {https://repositum.tuwien.at/handle/20.500.12708/188730}
}
(This webpage was created with bibtex2web.)