オレンジが「AIの時代こそ契約プログラミングと形式検証ツールの復権を！＞＜；」って言っても誰も見向きしないであろうから、
プログラミングパラダイム界隈の有名人(？)の誰かが「・・・もしかして、AIの時代こそ、契約プログラミングと形式検証によって計算リソースを削減できるんじゃね？」って気づいてほしい＞＜；
で、その返答のなかで興味深い部分が＞＜；(強調は『』に置き換え)
"LLMの役割の最適化:
LLMは、要件定義の解釈、高レベルな設計、全体構造の生成、自然言語に近いコメントの付与など、『創造性や柔軟性が求められるタスク』に集中し、『厳密な論理的整合性のチェックやバグ検出は形式検証ツールに任せる』という分業が可能になります。これにより、それぞれのツールの得意分野を活かし、全体の計算リソースを効率的に配分できます。"
ほぼそのままGeminiに聞いてみたけど、形式検証は決定論的な検証で、LLM論は確率論的な検証になるので、原理的に(？)決定論的な検証の方が計算量が少なくなる(？)ので、オレンジが言う通り、形式検証の静的検査が重いといってもLLMがコードを読む為の計算量よりは少ないので、LLMが形式検証環境を使うと計算量を大幅に削減できる可能性が高いかも(意訳) みたいな感じだった＞＜
契約プログラミングや形式検証の静的検査が遅い/重いのはGeminiさんが言う通りの弱点ではあるだろうけど、でも、『LLMがコードを読んで考える』よりは少ない計算量になりそうな気がするけどどうなんだろう？＞＜
つまり、AI支援型プログラミングの時代こそ、形式検証や契約プログラミングが優れてるかもしれないので、なんか10年くらい前にブームが終わってしまった(？)契約プログラミングを、今こそ復権させるべき！！！＞＜；
AdaのSPARKみたいな形式検証をプログラミング言語環境側に用意してあったら、ハルシネーションの大半にAIが自身で気づけるかもだし、形式検証とAIって相性どうだと思う？＞＜(意訳)って、Geminiさんに聞いてみたら、
「(形式検証で検出できる範囲において)単にハルシネーションに気づけるだけではなく、AIが形式検証エラーのメッセージを読むことで自律的に学習出来るので、SPARKみたいな形式検証とAIの組み合わせはすごくいいはず。でも、規模が大きいプロジェクトでは、AIが出力する契約プログラミングのコードが膨大になって、形式検証の実行に時間がかかってボトルネックになりそう」(意訳)
みたいに言われた＞＜
茨城南部っぽい揺れだったけど、茨城北部だった＞＜
どこいな＞＜
コーディングエージェントの現状の整理とエンジニアの仕事の変化について https://azukiazusa.dev/blog/coding-agents-and-developers-work
いま話題の(？)これ読んでて思いついたけど、
AIの自立型プログラミングでのハルシネーション抑制に、AdaのSPARKのように『契約プログラミングの記述を使った形式検証環境』をプログラミング言語側に用意したら、『形式検証で検出できる範囲のハルシネーションによる誤り(＝実行時にエラーを起こして停止するような誤りの大半)』は、AIがSPARKみたいなのを動かして形式検証エラーのエラーメッセージを読む事で自分で自分のハルシネーションに気づけるようになると思うんだけどどうだろう？＞＜
FreePats project - World and Rare Percussion
https://freepats.zenvoid.org/Percussion/world-and-rare-percussion.html
『10インチモニター搭載メカニカルキーボード』を発売 | サンコー株式会社のプレスリリース
https://prtimes.jp/main/html/rd/p/000000312.000111905.html
おもしろそうだけど、DellやhpのRyzen 3のラップトップが買えるお値段＞＜；
orange
さんがブースト
学生ごとにケースバイケースでなにか、となるやそれはもう口頭試問になっちゃうなぁ。
もうだったらペーパーテストにしてしまったほうが理解度・習熟度は担保される気がする。演習科目だとやや反則だけど。
たとえば、
課題は「hogefugaを行うプログラムを自分で調べて作ってきてください」で、それを提出した後に、「使用したアルゴリズムは何という名前で、どのような仕組みで目的を達成するアルゴリズムですか？ 簡潔に説明してください」みたいな感じの問題を出す感じ＞＜
「自分の頭で考えること」を学ぶ - いつか博士になる人へ
https://www.ki1tos.com/entry/2020/04/14/174739
何日か前にこれを読み返して思いついたけど（あんまり直接は関係ないんだけど）
課題とテストを分けるって方式にする手もありそう＞＜
課題は行って持ってくるけど、課題に関する問題は提出後に出題されるので、問題への回答部分で不正ができない方式＞＜
つまり自分が提出した課題に対する理解がなければ答えられない問題を後から出して、課題ではなくて後からのテストのほうで評価する方式＞＜
orange
さんがブースト
製作課題をスキップしてもよい、その場合は65点を上限とする。
製作課題に取り組むなら上限なし。ただし生成AIの書いたものをそのまま使った場合は不正行為、とか。
orange
さんがブースト
もうこれからは最終課題をやるかどうかを学生に選んでもらおうかなぁ。
生成AIのお出ししてきたものを真面目に採点するの時間の無駄だし。
orange
さんがブースト
まぁ、それですらうまく見つけられなかったりするけど、最近だと生成AIの出力をまんま提出して終わりにされてしまうから、持ち帰りの課題は成立しなくなるかも知れない。
orange
さんがブースト
認知特性とかはあるんだと思うんだよね。あとはまぁそもそも読むのが負担、という人もいるだろうし、あと検索サイトがいまいち役に立ちない(あるいは使い方を分かっていない)のもあると思う。
学生のケースでいうと、学生が探すようなトラブルシュートはともかくとして、自由製作課題とかで○○の作り方、みたいなチュートリアルを探してまんまやるだけで済まそうとしてたり。
普通に番組なフォーマットな（？）海外公共放送が制作したドキュメンタリーとかも有用だけど、それはそれでテキスト化には限界があるから（記録映像と証言映像が中心だから）であって・・・＞＜
- ＠orange_in_space
2017年 4月に登録
