契約プログラミングや形式検証の静的検査が遅い/重いのはGeminiさんが言う通りの弱点ではあるだろうけど、でも、『LLMがコードを読んで考える』よりは少ない計算量になりそうな気がするけどどうなんだろう？＞＜
ほぼそのままGeminiに聞いてみたけど、形式検証は決定論的な検証で、LLM論は確率論的な検証になるので、原理的に(？)決定論的な検証の方が計算量が少なくなる(？)ので、オレンジが言う通り、形式検証の静的検査が重いといってもLLMがコードを読む為の計算量よりは少ないので、LLMが形式検証環境を使うと計算量を大幅に削減できる可能性が高いかも(意訳) みたいな感じだった＞＜
フォロー
で、その返答のなかで興味深い部分が＞＜；(強調は『』に置き換え)
"LLMの役割の最適化:
LLMは、要件定義の解釈、高レベルな設計、全体構造の生成、自然言語に近いコメントの付与など、『創造性や柔軟性が求められるタスク』に集中し、『厳密な論理的整合性のチェックやバグ検出は形式検証ツールに任せる』という分業が可能になります。これにより、それぞれのツールの得意分野を活かし、全体の計算リソースを効率的に配分できます。"
「LLMは、創造性や柔軟性が求められるタスクに集中し」
って、人間の存在価値・・・・＞＜；