ChatGPTに形式手法でより複雑な問題を解かせる
- 2023/03/26
- 16:33
一発ネタです。
状態空間や時相論理を考慮する必要がある問題
では、頭の体操がてらこんな問題を考えてみましょう。
この記事の要約はこんな感じです。
- ChatGPTは論理的思考力が依然弱いですが、形式手法を組み合わせることで補える（かも）
状態空間や時相論理を考慮する必要がある問題
では、頭の体操がてらこんな問題を考えてみましょう。
以下の様なシステムを考えてください。
- 変数a, b, swがあります。
- 変数a, bの初期値は0で、0→1→2→0と同期しながら繰り返し変化します。
- b=1なら、aは変化しません。
- a=bなら、bは変化しません。
- swはon, offの二つの値を持ち、初期値はoffです。
- swはa=b=2ならon、a=b=1ならoffとなります。
これはモデル検査の多くの論文や書籍で紹介されている有名な問題で、もちろん答えはNoです。
紙とペンがあれば答えを出せると思いますが、以下に解説を載せておきます。
(a, b, sw)
0, 0, off
1, 0, off
2, 1, off
2, 2, off
0, 2, on //ここからループ開始
1, 0, on
2, 1, on
2, 2, on
0, 2, on
以下ループとなり、常にsw=onとなる。
この例題はかなり簡略化されていますが、プログラムを行う上でループ、デッドロック、非安全な状態遷移などを見つけたい機会は多いはずです。
では、GPT4はこの問題を解けるでしょうか？下の回答を見てください。
うーん、ムチャクチャだぞ。
残念ながら、現状のLLMはこの規模の状態空間すら正しく認識できないようです。
勿論この程度の問題であれば、将来出て来るであろうGPT5、6なら解けるようになる可能性は大いにあります。
しかし、この程度の問題を解くためにスーパーハイパーウルトラ巨大言語モデルを用いるのは、アリの巣駆除に核兵器を使うようなナンセンスなやり方に感じます。
そこで、今回はもう少し効率のいいやり方として、形式手法を使う方法を考えます。
今回はNuSMVを使ってみます。
NuSMVにした理由は、UPPAALやSPINと比較してライセンス的に使いやすいからです。
以下の質問を与えてみました。
いちいち文法の解説はしませんが、正しいソースコードが出ています。
自然言語で問題を解かせるとおかしくなるのに、ソースで出させると正しくなるのは興味深い結果でした。
そして、以下がNuSMVの出力です。（上に書いた解説と同じ反例が出ていると思います。）
最後に、この結果をGPT4に教えてあげます。
反例を教えてあげると、それが何を意味しているのか理解できるようです。
この事例から、以下の様な洞察が得られるのではないかと考えました。
- 現状のLLMですら、時相論理を使って状態空間を探索するような問の求解には不十分。
- 状態空間を探索するような問は、LLMよりも形式手法の方が計算効率が遥かに良い。
- LLMは問を形式手法の記述に直すことができ、解析結果を解釈することもできる。
例えば、GPTが答えを生成する前に事前にNuSMVを用いて検証を行うようにすることで、推論能力をより高めるといった使い方が考えられます。
これは、計算能力を高めるために計算機のAPIを使わせることと発想としては本質的に変わりませんが、遥かに強力なはずです。
ただ、結局のところ形式手法の文法で表現されたモデルや時相論理式が正しい事を確かめる術はないんですがね。
それでは。
