あと、MatzとDHHは先見の明が無さすぎると思う＞＜
(両者とも意訳するとAIが扱うプログラミング言語に静的型検査が不要である主旨の事を言ってる)
オレンジ自分で先見の明って言っていいと思う＞＜
LLMs are making formal software verification feasible at a much larger scale \ Anthropic https://www.anthropic.com/research/formal-verification
orange
さんがブースト
ちなみに、本家本元である(？)Ada/SPARK環境自体に関しては、LLMさん的には参考できるコードがほとんど無いので(だって、兵器やら原発やら宇宙機やらの機密がいっぱいな分野向けの言語だし)、学習がほとんど出来てなくて、基本的な構文に関してでさえもハルシネーションを起こしまくり＞＜；
なので、既にLLMが得意な言語で型がそれなりにしっかりしてる言語向けの形式検証環境を用意するのがよさそうだし、
つまり、C#版のSPARKという選択肢は有力ではないか？＞＜；
orange
さんがブースト
オレンジが「AIの時代こそ契約プログラミングと形式検証ツールの復権を！＞＜；」って言っても誰も見向きしないであろうから、
プログラミングパラダイム界隈の有名人(？)の誰かが「・・・もしかして、AIの時代こそ、契約プログラミングと形式検証によって計算リソースを削減できるんじゃね？」って気づいてほしい＞＜；
orange
さんがブースト
orange
さんがブースト
で、その返答のなかで興味深い部分が＞＜；(強調は『』に置き換え)
"LLMの役割の最適化:
LLMは、要件定義の解釈、高レベルな設計、全体構造の生成、自然言語に近いコメントの付与など、『創造性や柔軟性が求められるタスク』に集中し、『厳密な論理的整合性のチェックやバグ検出は形式検証ツールに任せる』という分業が可能になります。これにより、それぞれのツールの得意分野を活かし、全体の計算リソースを効率的に配分できます。"
orange
さんがブースト
ほぼそのままGeminiに聞いてみたけど、形式検証は決定論的な検証で、LLM論は確率論的な検証になるので、原理的に(？)決定論的な検証の方が計算量が少なくなる(？)ので、オレンジが言う通り、形式検証の静的検査が重いといってもLLMがコードを読む為の計算量よりは少ないので、LLMが形式検証環境を使うと計算量を大幅に削減できる可能性が高いかも(意訳) みたいな感じだった＞＜
orange
さんがブースト
契約プログラミングや形式検証の静的検査が遅い/重いのはGeminiさんが言う通りの弱点ではあるだろうけど、でも、『LLMがコードを読んで考える』よりは少ない計算量になりそうな気がするけどどうなんだろう？＞＜
orange
さんがブースト
つまり、AI支援型プログラミングの時代こそ、形式検証や契約プログラミングが優れてるかもしれないので、なんか10年くらい前にブームが終わってしまった(？)契約プログラミングを、今こそ復権させるべき！！！＞＜；
orange
さんがブースト
AdaのSPARKみたいな形式検証をプログラミング言語環境側に用意してあったら、ハルシネーションの大半にAIが自身で気づけるかもだし、形式検証とAIって相性どうだと思う？＞＜(意訳)って、Geminiさんに聞いてみたら、
「(形式検証で検出できる範囲において)単にハルシネーションに気づけるだけではなく、AIが形式検証エラーのメッセージを読むことで自律的に学習出来るので、SPARKみたいな形式検証とAIの組み合わせはすごくいいはず。でも、規模が大きいプロジェクトでは、AIが出力する契約プログラミングのコードが膨大になって、形式検証の実行に時間がかかってボトルネックになりそう」(意訳)
みたいに言われた＞＜
orange
さんがブースト
コーディングエージェントの現状の整理とエンジニアの仕事の変化について https://azukiazusa.dev/blog/coding-agents-and-developers-work
いま話題の(？)これ読んでて思いついたけど、
AIの自立型プログラミングでのハルシネーション抑制に、AdaのSPARKのように『契約プログラミングの記述を使った形式検証環境』をプログラミング言語側に用意したら、『形式検証で検出できる範囲のハルシネーションによる誤り(＝実行時にエラーを起こして停止するような誤りの大半)』は、AIがSPARKみたいなのを動かして形式検証エラーのエラーメッセージを読む事で自分で自分のハルシネーションに気づけるようになると思うんだけどどうだろう？＞＜
orange
さんがブースト
決定論的に検証できるツールがあるからこそ、ゆるふわである人間が安全にプログラミングできるというのは、確率論的でゆるふわなLLMによるプログラミングでも同じで、型検査や形式検証を行えばLLMさんも自分が書いたコードの誤り（矛盾）に気付けるかも＞＜
orange
さんがブースト
LLM側が決定論的じゃない問題って、プログラミング言語側が決定論的であるならば結果的に全く問題ないとオレンジは考えていて、
だからこそ、LLMを活用したプログラミングにこそ、静的型付けや形式検証（や契約プログラミング）が重要になってくるかもって気がしてる＞＜
LLMs are making formal software verification feasible at a much larger scale \ Anthropic https://www.anthropic.com/research/formal-verification
そこまでする(出来る)なら、SPARKに書き換えちゃえばいいじゃん・・・＞＜
「バグのないソフトウェア」の実現を目指してAnthropicが「AIを用いて数学的にバグがないことを証明する」という手法を開発 - GIGAZINE https://gigazine.net/news/20261023-anthropic-formal-verification/
・・・・？＞＜
orange
さんがブースト
「RSA-260」ついに解けた Xに“130ケタの数字”投稿、世界が注目 マスク氏「文字数増やしてよかった」（ITmedia NEWS） - Yahoo!ニュース
https://news.yahoo.co.jp/articles/d494e0bfa5872669dffe3a7b293e766bb898ee24
これからふと思って色々試したりして知ったけど、
RSAの計算が成り立つ最小限である4bitのRSAって作ろうとすると、必ず秘密鍵と公開鍵が同じになって「暗号とは？＞＜；」となる珍妙なものができる？＞＜；
本来推測不可能な秘密鍵にわずか1バイトの値を使っていたeMudhraがSSL/TLS証明書事業から撤退 - GIGAZINE
https://gigazine.net/news/20261023-emudhra-exit-ssl-tls/
海外で『鉄拳6』の勝手移植が誕生、これを契機として日本と海外ユーザーの海賊版に対するスタンスの違いが浮き彫りに、認識の違いはどこから来るのか考察が続々 - Togetter
https://togetter.com/li/2761835
これどちらにも100パーセントは同意しないけど、「じゃあ海外のやつらはクリエーターの立場ならどうするんだ？」という意見に関しては、『作者が昔作ったゲームをタダで配って』そして『パブリッシャーが慌てて止めたりする』という事例を何度か見てるので、そもそもそこから違うんじゃねって気がしてる＞＜
- ＠orange_in_space
2017年 4月に登録
