We introduce NeuroSynt, a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis problem. To ensure soundness, the neural engine is coupled with model checkers verifying the predictions of the underlying neural models. The open-source implementation of NeuroSynt provides an integration framework for reactive synthesis in which new neural and state-of-the-art symbolic approaches can be seamlessly integrated. Extensive experiments demonstrate its efficacy in handling challenging specifications, enhancing the state-of-the-art reactive synthesis solvers, with NeuroSynt contributing novel solves in the current SYNTCOMP benchmarks.
翻译:我们提出了NeuroSynt,一种面向反应式综合的神经符号组合求解器框架。该求解器的核心在于神经方法与符号方法在反应式综合问题求解上的无缝集成。为确保可靠性,神经引擎与模型检查器耦合,以验证底层神经模型的预测结果。NeuroSynt的开源实现提供了一个反应式综合的集成框架,其中可以无缝集成新的神经方法和最先进的符号方法。大量实验表明,其在处理复杂规范方面具有显著效果,能够增强现有最先进的反应式综合求解器,并在当前的SYNTCOMP基准测试中贡献了新的可解案例。