NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

要約

リアクティブ合成用のニューロシンボリック ポートフォリオ ソルバー フレームワークである NeuroSynt を紹介します。
ソルバーの中核には、反応性合成問題を解決するためのニューラル アプローチとシンボリック アプローチのシームレスな統合があります。
健全性を確保するために、ニューラル エンジンは、基礎となるニューラル モデルの予測を検証するモデル チェッカーと結合されています。
NeuroSynt のオープンソース実装は、新しいニューラル アプローチと最先端のシンボリック アプローチをシームレスに統合できる、リアクティブ合成のための統合フレームワークを提供します。
広範な実験により、NeuroSynt が現在の SYNTCOMP ベンチマークにおける新しいソルバーに貢献し、最先端の反応性合成ソルバーを強化して、困難な仕様を処理する際の有効性が実証されました。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google