投稿者: 774 - ページ 3

フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか

2026年9月21日2026年9月7日 by 774

AI が正しい文章やコードを生成できることと、その成果物が正しいと確定できることは別の問題である。生成結果がもっともらしく見えること、過去より正答率が高いこと、別の AI が正しいと評価したことは、いずれも成果物そのもの … 続きを読む

2026年9月15日2026年9月6日 by 774

RAG を設計するとき、最初に決めたくなるのは、文書をどの大きさで区切るかである。200 token なのか、500 token なのか、あるいは段落や節を単位にするのか。文書を短く切れば、一つの断片に含まれる話題が限定 … 続きを読む

2026年9月15日2026年9月5日 by 774

AI の出力を評価するとき、「評価が上がった」と「性能が上がった」は同じ意味に見えやすい。強化学習では、望ましい出力へ高い報酬を与え、その報酬が大きくなる方向へモデルを更新する。評価が正しさを十分に表しているなら、この方 … 続きを読む

2026年9月16日2026年9月4日 by 774

AI が生成したものを人間が評価し、問題がなければ使う。生成 AI の利用を考えるとき、この役割分担は分かりやすい。文章やコードでは、少なくとも多くの場合、外部へ作用させる前に内容を確認できるためである。ところが、AI … 続きを読む

2026年9月3日 by 774

2023 年、Kenneth Li らは、オセロの着手列から次の合法手を予測する Transformer を調べた。モデルに与えられるのは、盤面の画像でも、各マスが黒・白・空きのどれであるかを記録した状態表でもない。オセ … 続きを読む

2026年9月21日2026年9月2日 by 774

生成 AI を導入すると、組織はそれまで持っていなかった生産能力を外部から追加できるように見える。コードを短時間で生成し、既存コードを説明し、仕様書やテスト項目の下書きを作り、複数の実装案を比較できる。人間が一つずつ読み … 続きを読む

2026年9月1日 by 774

テストがすべて通ったコードは、正しいコードだと言えるだろうか。人間がソフトウェアを開発してきた時代から、答えは「必ずしもそうではない」だった。ソフトウェアに求められる仕様は、入力と出力の対応だけではない。境界値で正しく … 続きを読む

2026年9月1日 by 774

転職しました。

2026年8月31日 by 774

技術を使うとき、その内部で何が起きているかを完全に理解している場面は、実際にはそれほど多くない。スマートフォンを一つ操作するだけでも、無線通信、暗号、半導体、オペレーティングシステム、アプリケーション、クラウドサービスま … 続きを読む

2026年8月30日 by 774

情報という言葉は、しばしば「何が記録されているか」という内容と結び付けて考えられる。文章なら文字列、計算機ならビット列、DNA なら A、T、G、C の塩基配列である。この見方では、情報を保存するとは内容を失わずに保持す … 続きを読む