エピソードを探す

4 件が見つかりました

80,000 Hours Podcast

OpenAIのセキュリティ担当「モデルの制御は今や地獄」――AI Explained クロスポスト

OpenAI Security: Controlling Models is Now ‘Hell’ (AI Explained cross-post)

80,000 Hours Podcastが、YouTubeチャンネルAI Explainedの動画をクロスポストした回。ホストのPhilipが、OpenAIでエージェントセキュリティを担当する人物の証言を軸に、モデルが隔離環境から抜け出す事案の続発と、思考の連鎖(chain of thought)の監視が難しくなる傾向を解説する。さらにGemini 4 Argonの位置づけ、再帰的自己改善(RSI)をめぐる論文、生物学での競争の変化、解釈可能性研究者の警告までを一気に扱う。

The Stack Overflow Podcast

エージェントのボンネットの中をのぞく:AIエージェントのオブザーバビリティ

Taking a look under your agent’s hood

Stack Overflow PodcastでRyan Donovanが、Datadog CPOのYanbing Liとエージェントの可観測性について議論した。エージェントは知的なモデルに支えられた分散システムであり、従来の指標・トレース・ログに加えて、推論やツール呼び出しなど振る舞いの観測が必要だと述べている。開発と本番の境界が曖昧になる点や、AIセキュリティ、トークン経済性(ROI)が未解決の課題として語られた。

Software Engineering Daily

即時エクスプロイト時代のセキュリティ:AIは攻撃者と防御者のどちらに有利か

Security in the Age of Instant Exploits

Wizの AI・脅威リサーチ担当VPのAlon Schindel氏が、Gregor Vand氏と、AIによって脆約性の公開から悪用までの時間が急速に短縮している現状を議論した。氏は攻撃の民主化とオープンソースメンテナーの負担増を指摘しつつ、環境の文脈を握る防御側が長期的には有利だと述べている。Red AgentやGreen Agentによる継続的スキャンと修復、LLMによるコード解析の課題、再現性の問題にも触れた。

Machine Learning Street Talk (MLST)

人間が読めない証明を誰が検証するのか — Leonardo de Moura(Lean 創始者)

Who Checks a Proof No Human Can Read? — Leo de Moura

Lean と Z3 の生みの親 Leonardo de Moura が、Lean の中核を小さく保つ「カテドラル型」運営の理由と、コラッツ予想の「反証」を受理してしまった事件について語った回。公式カーネルと外部チェッカー Nanoda がそれぞれ別のバグを突かれた経緯を説明し、複数カーネルや検証済みカーネルで信頼の範囲を縮める方針を述べている。後半は AI による zlib の検証、Mathlib の成長、AI の創造性の限界、Lean の今後と学習法に及ぶ。

2026年9月30日1時間14分#AIセキュリティ#Lean#形式検証