形式手法の定義と自然言語の曖昧さ
今回は、形式手法の話をしていけたらいいんですけど、 まず、本当に形式手法というものが全く僕自身分かってないんですよ。
なので、ざっくり形式手法って何ですかね。 はい、まず形式手法ってすっごい広い言葉なんですよ。
これ例えるならば、動物園の動物を全部動物と言ってるようなもので、 本当はいろいろ種類があるわけですよ。象とかキリンとかいるじゃないですか。
そういうふうに、形式手法はいろいろあるんですよ。 あるんですけど、本当に広い、本当にいろんなことが形式手法と呼ばれているので、すごく難しい。
ただ共通しているところを挙げるなら、数学を基盤に置いているってところが共通しているところだと思います。
数学を基盤に置いて、数学を基に何らかを証明していくみたいな話なんですかね。
証明は実は動物の一つみたいな。 そんな感じなんですね。そこも広いんですね。
この形式手法の形式って何かっていうのは、結構大事なポイントだと思っていて、
よく形式的なとか言うじゃないですか。形式的な承認とか。 あんまりよくないですよね。
決まった型があって、それに従っているだけみたいな?
そうそう。決まった手順に沿ってやってるみたいな。 まさに形式手法って、これはそうなんです。
決まった型にはめて決まった手順。 これはどういうことなのかということなんですけど、
今、私たちがよく仕様書を書こうねとか、 要求分析しようねとかっていったときの成果物って、
自然言語の日本語の作文ですよね。 大体。 ドキュメントを書くときに日本語を頑張って書いて、図とかもずっとずつ入れつつ。
例えば最近、最近じゃないかもしれないけど流行ってたPRDとかやってましたよね。 機能要求なんとかドキュメント書みたいな。
プロダクト要求定理書か。 そのPRDはセクションのタイトルが決まっててみたいなとかありましたけど、
でも書いてるのが日本語なんですよ。 日本語で書くと何が問題になるかっていうと、人によって意味の解釈が違ったり、
これは俺はこういう意味だと思ったんだよみたいなことになっちゃうんですよね。 曖昧であるってことですね。
そう、曖昧であるってことです。人によって認識が変わったりとかする。 なので、どうしたらその曖昧さがあると何が起こるかっていうと、
本当はこれ作ってほしかったんだけど、全然違うの来たよみたいな。 カレーライス作ってたら、はやしライス来たみたいな感じになっちゃうんですよ。
だからあれですね。顧客が本当に欲しかったものの決め手みたいな感じになってしまうと。 そうそうそう。
だからそういうふうな解釈のぶれっていうのをなるべく排除するっていうのはどうしたらいいだろうかっていうと、これが形式総合ってことなんですね。
つまりみんなで決まったルールに従って解釈し、そういうことができるようにしようっていうのがその形式総合の一番の信念とかコアの部分なんですね。
誰が描いても同じフォーマットになるというか、同じ内容に、同じものであれば、同じ目的のものであれば同じような形になるということを目指したもの。
そこはちょっと言い過ぎかもしれないですね。 ちょっと違うんですね。
そうちょっと難しいんだけど、例えるなら何か作りたいものがあって私たちはプログラムを書くことがあるわけですよね。
実はプログラムって決まった項群があって決まった手続きで解釈されて決まった結果を出しますよね。
そうですね確実に決まってますね。 なので実はプログラミング言語は形式言語って言われているものの仲間なのです。
一種の形式手法ですか?
実は実際プログラミング言語を使って形式手法みたいなのもできるので、実際そういうものの使い方はあるんです。
例えば私が実例で言うと大きな森で仕様を書いてとかしてた時があります。
大きな森でプログラミング言語ですよね。結構よくML系の関数が書いてるんですけど、それで仕様を書いたりとかしてたので、こういう風な使い方がもちろんできるという感じですね。
一部そういう使い方ができるのでプログラミング言語も仲間で。
仲間、形式言語って言われているものなんですね。
この形式言語っていうのがまさにその形式の意味しているところなんですけど、
例えば仕様をこのプログラミング言語で書いてあげることができれば、みんなが実行すればこういうことかみたいなことがわかる。解釈が揃う。
解釈もできるし、あとバリデーションとかもできますかね。
っていうのが要するに形式手法の大雑把な見た目。
ざっくり言うとそういうことってことですね。
ただプログラミング言語って皆さんが想像してもらえばいいんですけど、
このプログラミング言語を書いた時に何が起こるか全部列挙してくださいって言われたらちょっと困っちゃう時ありませんか。
このプログラミング言語を書いた時に全て列挙してください。
例えば1たす1って書いた時にプリントF1たす1って書いた時に何が起こり得るか全部あげてくださいって言われて。
1たす1と表示されるとかそういうことですか。
そう思うじゃないですか。
だけど例えば標準出力のパイプが詰まっていれば何も表示されないってことが起こる。
何が起こるかっていうことに対して予測が難しいんですね。
プログラミング言語って何が起こり得るかっていう。
それは実行するパソコンのメモリー不足だったりとか。
そうそうそう。いろんなことが現実的なのが絡み合ってあって。
プログラミング言語って何が起こるかっていうのを予測って結構難しいんで。
なので数学を使おうっていうことだったんですよ。
なるほど。数学であれば理想論的に計算することができるからみたいな話なんですかね。
そうそう。数式で。
これもね人によっては起こられるかもしれないんですけど。
数式って人によって解釈がそんなに変わりにくい。
日本語に比べれば変わりにくい。
実際はちょっといろいろとあるんですよ。
例えば人によって使う記号が違うとかよくありますよね。
ありますね。
数学好きって方にもそういうのがよくあるんで。
実は本当に数式を人によって解釈が振れないのは本当か?みたいに言われると困っちゃうんですけど。
一致するかどうかと言われたらね。
日本語よりは揃うだろう。
なので数学っていう言葉をコアに据えて、
数学の言葉で仕様とか要求とかいろんなことを書いてあげようっていうのが
この解釈書の考え方。
ベースとなる考え方ですね。
ちょっと気になったのが、今の話聞いてて思ったのが
日本語っていう前提だったじゃないですか。
日本語はちょっと曖昧になる。
文脈とか、ハイコンテキストな言語だと思うので
文脈によって同じ言葉だったとしても
別の解釈になってしまって結構ありがちだなと思うんですけど。
これが日本語じゃなくて英語になったら変わったりします?
やっぱり変わらないですね。
例えば日本語で
AIとかにいい感じに作っといてって言う人いるかもしれませんけど
いい感じにって何なんちゃって言うと
これは人によって解釈がすごく売れるわけですよね。
同じように英語でいい感じにやっといてって表現できるわけですよ。
そうですね。
公約金かければいい感じにやっといてっていう英語が出てくるわけですよ。
なので基本的なセンスは変わらないってことですね。
じゃあ自由度が高すぎっていうところが問題点ですね。
そうですね。いろんなことを省略できちゃうし
単語の意味だっていろんな意味があるし
難しいねっていうことですね。
やはり数学を用いるっていうところが
書き方に制約があるみたいなところが結構大きいのかなと
若干思いましたね。今の話聞いてて。
その通りです。
数学っていうのは言葉の中にはすごく重要な性質があって
論章っていうのがあるわけですよね。
例えば日本語で論章することできるじゃないですか。
例えばソクラテスは人間である。
人間は死ぬ。だからソクラテスは死ぬみたいな
論章があるじゃないですか。
これはうーん、まあそうだなみたいなことを何となく思うわけですけど
数学はこれがちゃんとこのルールに従って
言わないと論章が成功したことになりませんよっていう
厳密なルールを持っているわけですね。
なるほど。
さっきのソクラテスは人間である。
まさに数学の数式で表すことができて
ソクラテスは人間であるみたいなことを書いて
それでその論章ができるっていうのがあるので
これがまさにさっき言った形式的に物事を解釈していく
ってことに対応しているんですね。
数学基礎論と定理証明支援系
なるほど。ちょっとここに来て新たな疑問が浮かんだんですけど
数学って今言ってるじゃないですか。
この数学って人名の書き方みたいなことですか?
それとも計算式ですか?
数学の書き方みたいなことを
これを数学と認めない人もいるらしいんですけど
数学基礎論とか数理論理学っていう言い方をします。
どんなことがルールとして使えて
正しい論章とは何かみたいなことを定めているのが
この数理論理学とか数学基礎論と呼ばれているものになっていて
その中には計算式、例えばよく算数とかで1たす1が2
これを説明してくださいみたいなこと
言われるじゃないですか。
あれがどうやったらそれが証明できたことになるのか
ルールを決めているのが数学基礎論なんですね。
なのでそのルールが数学の一部であり
どういう書き方を許しているかも数学の一部であり
そんな感じの現象なんですよね。
じゃあここで言っている数学ってのは
数学の根本的なルールの部分ですね。
計算式でxイコールyプラスαとか
そういう話ではないってことですよね。
計算式も数式の一つでもあるので
例えば方程式を解くときに
なぜそれが方程式のその解で言えるのかみたいなことが
結構重要な部分で
決まった手順でやらないと
例えば0で割っちゃって
1たす1イコール3が証明できちゃったみたいなことがあったり
それはどこかでローションが間違っているわけですよ。
それとかっていうのの整合をどう決めるか
っていうのが数学の重要な部分の一つですね。
ただちょっとごめんなさい。
すごく細かいことを言うと
数学がこういうふうに決まった手順でやっていけば
その論章が成功したか失敗したかが分かるっていう風に
言われ始めたのは結構最近の話なんですよ。
そうなんですか?
そうなんです。
昔はもっと感覚的な学問だったんですよ。
最近っていうのはどのぐらい?
モノクロ写真とかがあったわけですね。
なるほど。
それぐらい。
ヒルベルトとかがいた頃なんですけど
ヒルベルトっていう有名な数学者がいて
その人が数学をもっと形式化したいと。
みんなお気持ちだってんじゃねえかと。
なのでちゃんと形式化したら
すごくいい体系ができるんじゃないか。
そしたら数学自体が矛盾してないってことを
示せるんじゃないかみたいな
そういうことを考えた人がいるんですね。
ヒルベルトって人がいて。
その人とかいろんな人の努力によって
今は数学が結構形式化されたんですけど
実は昔は形式化がそんなに十分じゃなかった
っていうのはよくあって。
もうちょっとフワッとしてたみたいな。
もっとフワッとしてました。
例えばリミットって大学にとって並ぶじゃないですか。
並べました。
あれって高校とかだったらリミットになってる
ちょっと覚えてないんですけど
デルタ・エプシロンの方っていうのがあって
それで形式的に定義がついてるんですけど
あの定義がついたら結構後の方です。
それまでは定義ができるまでは
なんとなく定算してた。
多分これに収束するだろうみたいな感じで
そんな?
そんなっていうのがあって
だからデルタ・エプシロンを見つけた人
それで形式化した人は
ちゃんと名前が残ってる。
すごいですね。
その人がリミットを発明したわけじゃないですよ。
リミットは昔からあったんだけど
ちゃんと形式化するならこうだよね
っていうふうにした人がいるってことがあります。
なるほど。
じゃあ今まで使われてきたルールを統合すると
こんな感じで書けそうだよねっていうのを
まとめた人がいる。
今後はこのルールにのっとってやろうよみたいな
そうそう。のっとってやろうよと。
それがその形式的な数学って言われてるようなものなんですけど
ただこの数学の形式化っていうのは
本当に最近になってようやくめちゃくちゃ進み始めた
みたいなものって
それまでは片手で数えられるぐらいしか
こういうふうな形式的な数学で証明されたことが
あんまなかったんですよ。
例えば4色定理って呼ばれてる定理があって
2次元の平面をビチャビチャビチャって分割したら
これで何色の色をやれば
隣接した色が同じ色にならないのか
聞いたことありますね。
4色定理なんですけど
これ証明がクッソ長いんですよ。
人間が合ってるかどうか自信なかったので
イザベルっていうシステムを使って
定理証明支援系を使って
これで証明したんですね。
4色定理は何かずっと
組まなく場合は決してやったぜみたいな
っていうのをやって
こんな感じで結構いくつか残ってるんですけど
AIが来るまではそんなもんだったんですよ。
なんだけど今って
オープンAIが数学の証明をいっぱい
リーンっていう定理証明支援系で解いてやったぜ
みたいなのが出てるじゃないですか。
あれによってめちゃくちゃ難しい数学まで
形式ができちゃったぞみたいなことが
だんだん分かってきた。
なるほど。
今までちょっとフワッとしていた定理の部分が
ガチガチに固められるような形になってきて
っていうのが今。
それがすごく分かりやすい証拠が一個あって
兄弟の餅月教授が
ABC予想っていうすごく難しい数学の問題を
解いたっていうニュースになりましたよね。
だけどあれすごく数学界で議論があって
解けてないっていう人もいて
揉めてるんですよ。
その証明が正しいかどうかの証明ができない
みんなで証明できたっていう防衛が取れていない
だけどリーンとかのやつでやってあげれば
今私たちが認めてるルールを使っても
なおそれを理解できるってことが分かる。
すごく今確かに餅月教授も
リーンでやってみようみたいなことを
おっしゃってましたよね。
そういう風な数学の証明の
白黒つくっていうのが
なってきたってのはつい最近のことだっていうのは
言っておきたいですね。
で、そういった定理とかの書き方だったりとか
そういったところが形式手法のベースになってるよね。
そういうことです。それがベースになっていて
決まった手順で決まった数式を書いて
意味解釈のブレをなくそうってことは
基本的な部分で変わりはないんですね。
形式手法の理学と工学
で、多分一番重要なので
ここだけ押さえておきたいんですけど
今話してた数学の定理の部分とかって
全部工学的というよりかは
理学的なお話で
純粋数学みたいな
大学で行われている数学の
研究なのかなと思ったんですけど
それはあってますか?
半分あってて半分違うかなと思っていて
形式手法も工学的な側面と
理学的な側面の両方があって
例えば理学的な側面だと
より計算機科学に近い
オートマトンとかそういうものとかに近くて
こういうオートマトンを使えば
いい感じに使用技術できるんじゃね?
とかっていうのがもしかしたら
書かれるかもしれないし
そうするとこういう性質が言えるんだよか
みたいなのがあるかもしれない。
それはどっちかというと
理学的な側面を持ってると思ってるし
そうじゃなくて現実にこういう問題があって
数学の力を使えば
ここがこういうふうに解決できるぞとかって
示すのはどっちかというと
工学的ですよね。
なのでどっちの側面もあるという感じですね。
なるほど。
さっき話してた定理の部分のお話に関しては
理学的なところの
工学はあんまり関係ないところですね。
あんまり関係ないですね。
なんだけど形式手法に関しては
理学も工学もどっちも合わせて
どっちも出てきちゃうんですね。
プラスアルファ、工学のほうの分野の部分も
結構あるっていうところですね。
具体的にソフトウェアだったりとか
物理的なところに対して
適応し得るのが形式手法というのが
側面としてあるという。
やっぱりありますね。
そうですよね。
これを聞いてここまで聞いてくれてる人の中で
全然自分工学部だったけど
数学のこと知らんから
形式手法ちょっと自分と違うのかな
みたいなことを思ってしまして
いるかなと思ってここまでで
じゃないんだぞと。
工学的なところが結構あるから
自分のソフトウェアを作る上で
形式手法というのはかなり重要なんだよ
重要な考え方になり得るよね
というところをちょっと理解してもらえなかったから
今言った感じです。
私はもう工学出身なんで
工学の人の気持ちわかるんですけど
私電気工学やってたんですよ。
電気工学って複層数とかっていうのを
数学のやつは道具として使うんですよね。
でも複層数ってすっごく豊かな分野なのに
私はほとんど複層数論よくわかっていない
道具として使えればいいんだよ
みたいな感じだったじゃないですか。
そのノリで形式手法もいいってことですよね。
もう理解しきる必要はない。
使えればいいんだっていう風なノリで
いくことは結構大事だと思ってます。
すごい今聞いてて
大学の頃に応用数学という授業があったんですけど
すごく苦手だったということを思い出しました。
無理だなと思って
物理の方に逃げたんですけど
難しかったんで。
私も数学がそんなに得意な方じゃないんですよ。
これは何か人に言うと
えーって思われるかもしれないですけど
本当に数学得意な人と見比べると
私は全然得意じゃないっていうのがよくわかる。
結構あって。
だけど別に形式手法私使ってるし
使えるっていうのがあるんで
これは同じですよ。
ドリルをどれだけ取れたかみたいな
そんなもんですね。
わかんない部分に関しては
別にそれが道具として使えればいいので
目的を達成する。
形式手法であれば
使用の記述に関して
いろんな人が書いたとしても
いろんな人が読んだとしても
ぶれがないような
認識にぶれがないようなものを
作るっていうような上では
形式手法は有用だから
それを道具として使えるようになっておけば
結構有用だよねっていう。
本当にその通りです。
ただの道具なんですよ。
理解しきる必要はなくて
スパナをどうやって作ってるかを
理解する必要はそんなになくて
スパナが使えればいいんですよ。
だからそういうふうなぐらいで
始めてみればいいと思いますね。
重要ですね。
形式手法とか数学側とか定理側とか
言われると思考停止するんで。
小さなサンプルから始めて
こんなことやってるので
小さいのだったらこれでいいんだ
みたいなとかっていうのを
積み重ねていくと
だんだんとやっぱり分かる範囲が増えていく。
めちゃくちゃ重要ですね。
なので使えるものでするよ
というようなところですね。
形式手法に関して。
AIを使うバイブ形式手法の落とし穴
すごく概念的な形式手法というのは
こういうものだよというところは
分かってきたんですけど
この1回で全部形式手法を語るっていうのは
結構難しいかなと思うので
次回以降にもうちょっと具体的なところ
形式手法をどうやって使っていくのか
みたいな話をどんどんしていければな
とは思っているんですけど
その前に今回
形式手法が実は若干流行っている
みたいなところがある
みたいなことを聞いたんですけど
そうなんですよ
流行ってるというか
バイブ形式手法が流行ってる
別に私がiXで見てると
なんかよくわかんないけど
TLAプラスっていう形式手法を
普通にやらせてみたとか
なんかよくわかんないけど
リニューアルしてみたとか
その特徴が結構あって
初めに実装がある
自分の回で実装があって
後からリーンとかTLAプラスとか
いろんなツールを使って
アロイとかいろんなツールを使って
検証をやれって
AIがユースで検証して
なんかやるみたいな
そんな感じ
ソフトウェアというか
実装があって
それに対してその検証を
形式手法を用いて
AIに検証してもらう
みたいないうことをしている
している
多分ちょっと簡単に見た感じだと
何を検証してるのか
よくわかってなさそうだった
と思っていて
そこは個人的には
モニューントなポイントだったんですよ
すごく外部形式手法をするときに
気をつけなきゃいけないことがあると思っていて
それは何が検査されていて
検査が成功したら
それは何を意味するのか
ってことがすごく大事だと思っているんですよ
例えばテストってあるじゃないですか
単体テストとか書きますよね
単体テストが成功してるってことは
何を意味してるかっていったら
例えば1たす1イコール2だったら
1と1っていうのを足すと
2っていう限界になるよ
っていうのが
1と1と2の例だけでは
っていうのがテストで言えることですよね
だからもしかしたら
1たす2っていうのが3になるってことは
試しじゃないからわからない
っていうふうなことです
つまり何が意味するのかっていうのは
どこまでがカバーされていて
どっからは対象外だったのか
そこの区切りを認識しておくことが大事だ
っていうことになるんですよ
それは
形式手法をすごく論文かけるぐらいまで
細かく見てほしいって意味じゃなくて
ちゃんとAIに何を
この成功したら何が構造されていて
逆に何が見逃されてるのかってことは
ちゃんとAIと問答してください
っていうことなんですよね
例えばリーンで証明しました
じゃあバグでーかみたいなことになって
その認識を合わせるとか
そういうのをちゃんと
AIと問答してくださいって
なるほど
リーンを使って証明されたかといって
それが無の証明な可能性があるってことですよね
そうですそうです
何も別に証明してないけど
証明できましたっていう
謎のものが通ったみたいな
っていう可能性も全然ある
可能性も全然ある
実際オープンAIが出してきた数学の論文の中には
定理が一定のことと
研究者が認識していた定理の形っていうのが
違ってて
違うことを表明しちゃったっていうので
論文を撤回されたのがいくつかありましたね
そういうことが同じことになったわけですよ
AIが認識しているものと
研究者が認識している差分が
あったってこと
そうそう
違ったことを証明しちゃってました
ごめんなさいって言って
論文を取り下げてたのが
確かにいくつかありましたね
それがソフトウェアで起こると
何が起こるかっていうと
全然関係ないソフトウェアのシステムが
うまくいってますみたいなことを報告して
自分のシステムが実際動かなかったみたいな
誤解が発生するわけですよね
私はバイブル形式主義の一番怖いのは
この誤解だと思ってるんですよ
どこまでが保証されてるかってこと
人間が誤解して
バグらないシステムだぜ
理由に証明されてるんだぜ
って実際バグがありました
っていうことをすごく恐れている
形式主義は役に立たないじゃねえか
みたいなこと言われちゃうわけですよ
結果そうなりますよね
リンが使ってたらバグがねえって
言ってたじゃねえかあいつ
みたいなことになるわけじゃないですか
そういうことじゃねえ
いやいやいやいや
ちょっと待て待て待てってなるわけですよ
なんでリンってね
リンとか定理証明支援系って
道具なんですよ
何を証明するかってことは
ちゃんとソフトウェアと繋がってないといけないし
ソフトウェアが動かして
例えばこのコードは
リビーのコードとして万全です
みたいなことを言われたとして
それがちゃんと思った通りのソフトウェアかどうかなんて
何も保証してないわけですよ
リビーとしては解釈できますね
以上のことではない
そういうふうな証明だって
意味ないんじゃないですか
そんなの
信託して書ければいいんだよ
みたいな話があるわけなんで
なので何が保証されていて
何が保証されてないのか
この区切りを人間と
ちゃんと実際が一致するように
理解することがすごく大事だと思います
なるほど
ちなみにこのバイブ形式処方をやっている人たち
たぶん別に国明さんがやっているわけじゃないので
実際のところは分からないかなと思うんですけど
見ている限りでいいんですけど
バイブ形式処方でやって
よしじゃあこれバグなさそうというのを
証明できたって言っている人たちって
そのテストとの違いって
どういう認識だったりするんですかね
いや多分
有限の壁とテストとの使い分け
最近よくテストも
そのエアに書かせたりする人いるじゃないですか
実装先にやって
エンドウィッチンのテストよろしくやれって言って
上やら上ですって言ってやるみたいな
それと同じで
なんかよく分からないけど
やってみたら安心するんじゃないみたいな
そんな感じでやってるんじゃないかなって
気がしていて
そう何か不安だったと
で不安
バグがないことを
保証
テストはバグがないことを保証はできないんですけど
バグがなるべく少なくするように
テストっていうのを書いておけばいいという
キーワードが繋がると
テストを書けばいい
あるいは形式処方をやればいい
っていう風に
飛びつきがちだと思っているんですけど
実際は
もっと入念に準備をしないといけないものではある
ですよね
難しい
ちゃんと人間が認識した上で
AIに対してどこを検査してほしいのか
テストとの境界線だったりとか
そういったところを意識しないと
ちゃんと道具として
使い切れないよね
っていうところがあるよね
本当にそうなんですよ
これは定理証明神経を
自分で書いてみたことある人が
言えることだと思うんですけど
実際定理証明神経書いてみると
手で書けたりとか
なんとなくうまく書ける
1日とかで書けるような
範囲のものっていうのは
大したことがないんですよ
本当に定理証明神経で書けるものって
大したことが証明できない
本当に簡単なことしか証明できない
例えば1たす1が
xたすyがひっくり返して
yたすxになっても
同じであるみたいな
こういうことを
初心者の頃は
頑張って1日中書けて証明するんですよ
でもそれで証明できたら
それだけが至るはずになっちゃうわけですよ
でも
ここから累生すると
AIが
証明バリバリ返ってくるとはいえ
実は証明してる主張って
そんなに強いこと言ってない
っていうのはよくあるんですよね
つまり
AIがどっかで手を抜くんですよ
ここは
諦める
諦める
例えばプログラムでいうと
メモリの空間って有限なわけじゃないですか
2ギガのメモリの人もいるし
4ギガのメモリの人もいるし
2ギガのメモリの人は
今の時いないかもしれないですけど
そういう人たちで
実際メモリをいっぱい使うプログラムだったら
2ギガの方が先にクラッシュするし
4ギガのやつは
実際によって
振る舞いが変わってんじゃん
みたいなことを
リーンが意識してるかって言ったら
絶対意識してないんですよ
そこは対象外です
メモリは無限にあると
仮定してますみたいな
仮定のしれって言うわけですね
そう
だからこういう風に
リーンとかに任せてたとはいえ
どこまでを正確に
プログラムの模倣をしていて
どこからがモデリングして
取捨選択したか
要するにここはいらないって
切り捨てたかっていうのは
すごく抑えておかなきゃいけないところで
大抵はめちゃくちゃ手を抜かれてます
リーンとかで
さっき言った通り
リーンで証明するのって
すごく難しいので
大抵は本当に
すごい手を抜かれてます
だから実はあんまり大したことを
証明してなかったってことは
よくあるわけです
でも本当に
適用範囲によりますね
ちゃんと適する場面で
形式手法を適用して
証明したいところを
ちゃんと証明するっていう
他の部分に関しては
基本的なところとして
今までやってきた
エンドツーエンドのテストだったり
ユニットテストだったり
っていうのを駆使する
それの組み合わせが最適である
そうです
この形式手法と
普通の従来のテストの壁っていうのは
有限の壁っていう風に
私は呼んでいて
いくら結合テストとか
エンドツーエンドテスト
単体テストしても
個別のサンプルを
いくつか試しました
それが100個なのか1000個なのか
1万個なのかわからないけど
有限の数を試しました
でしかないですね
これを全通り確かめました
一般に持っていくのが
形式書
それは数学の証明とかを使うんですね
それはすごく
数学の証明の作業と似てて
例えば
三角形があるとして
その三角形の面積とか
っていうのを考えることがあるじゃないですか
その面積って
例えば高さ1
幅1の二等辺三角形だったら
大きさが2分の1ですよね
それについては2分の1だって
わかったんだけど
これテストがこれと同じ
だけど
この高さ
底辺かける高さ
っていうので
全部その三角形の面積を
表せるんだよ
っていうことは
試すには
本当にいっぱい三角形を
試さないといけない
何らかの三角形が
無限にあるので
試し切ることはできない
だけど
これを
数学の力を使って
証明をすると
全通りの三角形に対して
成り立つということが
確かめられる
これがまさに
ソフトウェアでも
同じことが起こってるわけです
テストは
個別の三角形しか
確かめられないんだけど
だけど
形式手法を使うと
数学の力を借りているので
全部の三角形に対して
それが成り立つ
例えば
パグがないことが
成り立つ
とかってことが
否決できる
っていうのが
その形式手法の
側面の一つですね
なるほど
では
形式手法で扱っている
ものに関しては
全体の証明をして
理論的に
これは証明できたよね
っていうところを
割り出して
具体として
物理的なところ
具体的なところは
ユニットセンスだったり
実際のテストで
回してっていうところが
境界線というか
そうですね
使い分けの
部分なんですね
実際に
定理を証明するとき
実際に
形式手法を使って
証明するときって
やっぱり
何か上手く証明できない
なったら
個別のサンプルで
見るんですよ
あれ
じゃあこのケース
上手くいく
そうですよね
これが判例か
ってなって
前提条件足りなかった
みたいな
そうですよね
そういう意味で
やっぱり
個別にテストして
具体的な例から出発しないと
人間ってやっぱり
分からないことが
結構あるんで
個別の例を試すと
自分の間違ったところ
気づくっていうのは
形式手法でも
すごくよくある
じゃあもう
行ったり来たりしてる
ってことですよね
行ったり来たりしてます
どっちも
そうそうそう
じゃあ
なんかどっちが必要
どっちか片方があるから
いいっていう話でもないし
そうそうそうそう
本当そうなんですよ
難しいなあ
というところが
だからこそ
ちゃんと認識
それを扱う人間が
ちゃんと認識した上で
AIに対して
指摘っていうか
指示を出していかないと
ちょっとずれた方向性に
いってしまうよね
っていうのは
ずれた方向性になって
本当に保証されてることと
実際に保証されてる
と思ってることと
実際に保証されてることに
ずれが生じて
悲劇を起こす
というふうになるんですね
結果的に
いや形式手法
使えないじゃん
だって
あとは
大事故をかます
みたいな
いうことになりかねない
そうそうそうそう
なりかねない
設計段階から証明しやすくする
ということですね
あともう一個だけ
ちょっとこれは
言っておきたいことがあって
さっきの
バイブ形式手法が
すごく良くないなって
思うことの
もう一つの点があって
実装が先にある
っていうのが
良くないと思ってるんですよ
テストもよく言いますよね
先にテストかけて
じゃないと
テスト不能になっちゃうから
ってよく言うと思うんですけど
形式手法も同じなんですよ
なるべく
強いことを言いたい
例えばバグがないとか
絶対
いつかは停止するとか
すごく強いことを
言いたければ
それに応じた
その設計とか
仕様とか
の書き方があって
それを知っておかないと
後で証明するのは
すっげー大変なんですよね
だからそうすると
AIは何をするかっていうと
手を抜き始めるわけですけど
なので
テスト用意な設計と
同じように
証明用意とか
その形式手法用意な
設計とか
仕様とか
っていうのが
あるんですよ
だからその段階から
形式手法を掴んだったら
その段階から
意識した方がいい
っていうのが
すごくあって
でも最初から
ってことですよね
だから
前回の
エンドとエンドテストの
話で
出てきた
後追いテストに
しかならないよね
後追いの確認に
しかならないよね
っていうところと
全く一緒で
後追いの証明に
しかならないし
で
多分後追いすると
1パターンとか
2パターンとか
そういう
すごく狭い領域での
証明みたいな話にも
なってしまいそうで
あんまそれは
意味ないよな
っていう
ところですね
でも最初から
ちゃんと意識して
設計していく
本当に
形式手法設計
っていうか
わかんないですけど
テスト設計的な
アプローチで
同じ形で
最初から
ちゃんと頑張って
頭使わないといけない
っていうのは
変わらない
そうですね
変わらない
ってことですね
なんなら
AIは形式手法を
用意してくれって言ったら
それなりに
やってくれると思うんですよ
だからそのタイミングから
もう形式手法のこと
意識し始める方が
良いということですね
うん
なるほど
じゃあ
難しいなって
思いました
今
やっぱり
テストと一緒で
そうそう
テストと一緒で
ただコツは
人間が保証範囲を判断する
そんなもんなんですよ
上流からやっぱり
やるべきだっていう
その部分が
コツなぐらいで
あとは
AIに
全部
手段とか
お任せしちゃっていいんだけど
どこを保証してほしくて
そういうことは
ちゃんと
伝えるべき
そして
実際に実装されたら
どこまでが
保証されてないのか
ってことを
ちゃんと聞いて
それだったらいいよ
とか
あるいは
ダメだから
もうちょっとやり直してください
とかっていうか
その調整を
ちゃんとすること
この2点が
やっぱり大事だと思うんです
人間が判断
ジャッジする
その品質として
大丈夫かどうか
という
ジャッジするためにも
人間に知識が必要ですね
そこに関しては
確実に
だからこそ
じゃあ
あれですね
次回とかで
やっていく
形式手法の
ちょっと具体的なところ
最初は
どう使うのか
みたいな
どういう場面で
使えるのか
みたいな
いうところから
入っていければな
とは思いますけど
ちょっと具体的なところ
見ていければな
とは思うので
結構
はいどうぞ
ただ
ごめんなさい
これはちょっと
逃げみたいな感じになってますけど
私の形式手法というと
すごくさっき言った
動物園っていうと
霧とか分かるんだけど
像は分かんない
ということがよくあるので
私は私の知ってない
しかおしゃべりできません
そこはちょっと
ご了承ください
いやもちろんそうですね
全てを
知ってるわけじゃないし
別に研究者なわけ
じゃないんでね
はい
できる範囲というか
分かる範囲での
説明というか
具体的なところ
聞いていけたらな
と思うので
はい
じゃあ
次回以降も
よろしくお願いします
はい
ということで
今回はここまでに
したいなと思います
もっと詳しく教えてください
ラジオを略して
くわラジでは
スーパーエンジニアである
国明さんに
一般エンジニアである
辺徳が技術的な質問を
していく番組です
今後もいろんなことを
聞いていけたらな
と思ってますので
お聞きのプラットフォームで
高評価ボロのほう
お願いします
次回以降は
何回かに続けて
形式手法の話
していくかなと
思うので
はい
ぜひ聞いてください
またですね
こんなことを国明さんに
聞いてほしい
みたいなことありましたら
コメントいただけると
とりわけますので
よろしくお願いします
Xなどで
感想もぜひお待ちしております
それでは今回も
ありがとうございました
ありがとうございました
