フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか
AI が正しい文章やコードを生成できることと、その成果物が正しいと確定できることは別の問題である。生成結果がもっともらしく見えること、過去より正答率が高いこと、別の AI が正しいと評価したことは、いずれも成果物そのもの … 続きを読む
RAG の設計は「最適なチャンクサイズ」では終わらない
RAG を設計するとき、最初に決めたくなるのは、文書をどの大きさで区切るかである。200 token なのか、500 token なのか、あるいは段落や節を単位にするのか。文書を短く切れば、一つの断片に含まれる話題が限定 … 続きを読む
AI は正しさではなく、評価の通り方を学ぶことがある
AI の出力を評価するとき、「評価が上がった」と「性能が上がった」は同じ意味に見えやすい。強化学習では、望ましい出力へ高い報酬を与え、その報酬が大きくなる方向へモデルを更新する。評価が正しさを十分に表しているなら、この方 … 続きを読む
人間の役割は、評価からゲート判断へ広がる
AI が生成したものを人間が評価し、問題がなければ使う。生成 AI の利用を考えるとき、この役割分担は分かりやすい。文章やコードでは、少なくとも多くの場合、外部へ作用させる前に内容を確認できるためである。 ところが、AI … 続きを読む
AI は「次の単語を予測しているだけ」なのか
2023 年、Kenneth Li らは、オセロの着手列から次の合法手を予測する Transformer を調べた。モデルに与えられるのは、盤面の画像でも、各マスが黒・白・空きのどれであるかを記録した状態表でもない。オセ … 続きを読む
AI は組織の強さも弱さも増幅する
生成 AI を導入すると、組織はそれまで持っていなかった生産能力を外部から追加できるように見える。コードを短時間で生成し、既存コードを説明し、仕様書やテスト項目の下書きを作り、複数の実装案を比較できる。人間が一つずつ読み … 続きを読む
AI がテストを通しても、「正しい」とは限らない
テストがすべて通ったコードは、正しいコードだと言えるだろうか。 人間がソフトウェアを開発してきた時代から、答えは「必ずしもそうではない」だった。ソフトウェアに求められる仕様は、入力と出力の対応だけではない。境界値で正しく … 続きを読む
近況
転職しました。
分からない技術を、分からないまま使うための条件
技術を使うとき、その内部で何が起きているかを完全に理解している場面は、実際にはそれほど多くない。スマートフォンを一つ操作するだけでも、無線通信、暗号、半導体、オペレーティングシステム、アプリケーション、クラウドサービスま … 続きを読む
DNA 複製から見える、情報を時間へ展開する構造
情報という言葉は、しばしば「何が記録されているか」という内容と結び付けて考えられる。文章なら文字列、計算機ならビット列、DNA なら A、T、G、C の塩基配列である。この見方では、情報を保存するとは内容を失わずに保持す … 続きを読む