AdaのSPARKみたいな形式検証をプログラミング言語環境側に用意してあったら、ハルシネーションの大半にAIが自身で気づけるかもだし、形式検証とAIって相性どうだと思う？＞＜(意訳)って、Geminiさんに聞いてみたら、
「(形式検証で検出できる範囲において)単にハルシネーションに気づけるだけではなく、AIが形式検証エラーのメッセージを読むことで自律的に学習出来るので、SPARKみたいな形式検証とAIの組み合わせはすごくいいはず。でも、規模が大きいプロジェクトでは、AIが出力する契約プログラミングのコードが膨大になって、形式検証の実行に時間がかかってボトルネックになりそう」(意訳)
みたいに言われた＞＜