Leanとは？AIが書いた数学の証明を機械で確かめる仕組み
OpenAIが公開した数学の原稿集には、主な結果の約4割にLeanの証明が付いています。Leanとその検査道具Comparatorが機械で保証する範囲と、人が読まないと分からない範囲を説明します。
AIAI
AI
AIレッドチーミングとは？AIの弱点を攻撃者目線で探す評価手法
レッドチーミングは、攻撃者の役を味方が演じてAIの弱点を本番前に探す評価手法です。探す対象はプロンプトからシステム全体に及び、ガードレールやベンチマークとは役割が違い、一度で終わらない点も押さえどころ。
AIベンチマーク汚染とは？AIの高得点を疑うための基礎知識
ベンチマーク汚染とは、テスト問題が学習データに紛れ込んでAIのスコアが実力より高く出る現象です。GSM1kの検証結果と、汚染に強い評価の作り方、スコアの読み方を整理しました。
AIRAG評価とは？検索と生成を分けて測る指標の基本
RAGの精度を「なんとなく」で判断していませんか。検索側のコンテキストリコール／プレシジョンと、生成側の忠実性／応答関連性に分けて測る、RAG評価の基本を整理しました。
AIリランキングとは？RAGの検索結果を並べ替えて精度を上げる
ベクトル検索で拾った候補をクロスエンコーダで採点し直すリランキングの仕組みを、一次検索との役割分担・100件だけ並べ替える理由・Cohere Rerankの使い方から整理しました。
AI知識カットオフとは？AIが最近の話を知らない理由
AIが最近の出来事を知らない理由、知識カットオフを整理しました。公式ドキュメントが併記する「信頼できるカットオフ」と「学習データのカットオフ」の違いから、足りない知識を外から渡す考え方まで。
AIRLHFとは？人間の好みでAIの答えを整える仕組み
RLHFは人間の評価を報酬に変えてAIの答え方を寄せる学習方法です。3段階の流れ、なぜ模範解答ではなく順位を集めるのか、DPOのような後継手法までを一次論文つきで整理しました。
AIKVキャッシュとは？LLMが長い文脈で重くなる仕組みを整理
会話が長くなるとAIの応答が重くなるのはなぜか。KVキャッシュが何を保存しているのか、文脈が伸びるとメモリがどれだけ増えるのか、削るための3つの方向までを順番に整理します。
AItop-pとtop-kとは？AIの言葉選びを絞る仕組み
生成AIのパラメータ top_k と top_p は、次の1語の候補をどこまで残すかを決めるつまみです。個数で切るか確率の総量で切るかの違いと、同じしきい値でも残る候補数が変わる理由を、実際に計算した数値で整理しました。
AI蒸留とは？大きなAIモデルの知識を小さなモデルへ移す仕組み
AIの蒸留（ディスティレーション）を整理しました。教師モデルの確率分布を手本に小さな生徒モデルを訓練する仕組み、ファインチューニングや量子化との違い、モデル選びで気をつけたい点まで一次資料つきでまとめます。
About Me
かもめ／2児のパパエンジニア
いま知りたいこと・学んでいることを調べてまとめたノートと、実際にやってみたことの記録です。あとで読み返すために書いています。
AIやクラウド、テックリードの勉強、子育て世帯の暮らし、APEX・鳴潮・RED STONEのプレイ記録など。
＊くわしいプロフィールは「More」から「かもめの歴史」へ。