前回からの変化
前回(2026-10-23、前日)との比較である。
変わったこと(変化・新規)
- 前回は先回り型エージェントのClaude Duetと学習手法JOLTが中心だったが、今回は、AIが書いたプログラムの安全性を数学的に証明するという「AIによる検証」の話題が中心になった(Unite.AI)
- エージェントの安全面で、外部の評価者がOpenAIの監視の穴を見つけた報告と、AnthropicがClaudeのautoモードを有料プランの標準にする話が出た(The Neuron)
- 新顔として、HeyGenの汎用動画モデルHeyGen Video 1と、Hugging FaceのDNA向けモデルCarbon-Xが出た(同上)
昨日と同じこと(継続)
- 性能値が各社の自己申告に偏り、第三者の検証が遅れる構図は続いている。HeyGenの順位づけも、確認できたのは二次報道のみである
- 前回のClaude Duet、JOLT、Mistral Large 4(10月末にオープンウェイトで公開予定)、Flintについて、今回の出典では新しい続報は確認できなかった
要因の連続性
- 継続要因: エージェントの自律性が高まる一方で、承認の仕組みや監視が設計の中心になる流れ。前回のClaude Duetの承認ゲートに続き、今回もautoモードの自動チェックや監視の欠陥が話題になった
- 新規要因: 「AIが作った成果物をAIが証明する」検証の自動化。人手では追えない規模の確認ができるようになったことが、新しい論点として加わった
- 解消した要因: なし
本日のハイライト
Claudeが公開ライブラリ123件の安全性を機械語レベルで証明
Unite.AIによると、Anthropicは証明支援の企業Theoremと協力し、Claudeに、公開ライブラリの安全性を数学的に証明させた。既存のファズテスト(ランダムな入力を大量に与えて不具合を探す検査)を、RISC-Vという命令セットの機械語レベルの仕様に書き換え、Rocqという証明検査ツールで検査した。対象は123のライブラリにある239の入口で、検査を通った証明は約1億8千万行、生成した量は約10億行に上る。
結果として、数百件のバグが見つかり、その中には10年以上潜んでいたものも含まれる。ここでの証明は、「入力が64メガバイト以下なら、プログラムは必ず正常に終了し、メモリの誤用を起こさない」という性質である。ただし、証明が成り立つのは単一スレッドで動く静的なRISC-Vの実行ファイル(musl libc)に限られる。多くの利用者が使うx86やARM、動的リンクのglibcの環境には、そのままは当てはまらない。証明の一部と、RISC-V・OSの意味付けはGitHubで公開され、未修正の脆弱性を明らかにする証明は伏せられている。この成果はAnthropicの自己報告であり、第三者による再現はまだない。
Microsoftの診断AIがScienceに登場 難しい症例で一般医の2倍以上
The Neuronによると、Microsoftの研究者は、診断を段階的に進めるAIシステムがScience誌で発表され、難しい症例で一般医の2倍以上の精度を示したとした。一方でTechCrunchは、改善の多くは診断の仕組みではなく、基になるAIモデルの進歩によるものかもしれないと指摘している。条件の詳細は今回確認できていない。
主要企業のリリース
- Anthropic: Claudeのautoモード(ツール呼び出しの安全性を分類器が自動判定し、危険な操作を止める機能)を、Pro、Max、Teamの有料プランの標準にするとThe Neuronが伝えている。ただしInfoWorldは、Claude Codeのautoモードが8月に有料プランの標準になったと報じており、今回の話が別の製品面を指すのか、重複した報道かは確認できていない(The Neuron、InfoWorld)
- Microsoft: 上記の診断AIの論文。ほかに、中国系のハッカー集団Storm-0940が、ConnectWiseへの侵入でARTEXというエージェント型の侵入試験システムを使ったと報告した。攻撃の作業を短縮し、Microsoft 365の認証情報を悪用したという(The Neuron)。詳細は
cyber_securityを参照 - OpenAI、Google、Meta、xAIの新しいモデルの技術的なリリースは、確認できた範囲では見当たらない
新興AI・注目の新顔
- HeyGen Video 1: HeyGenが公開した初の汎用動画生成モデルである。Artificial Analysisの盲検テストのテキストから動画の部門で1位になったと伝えられているが、確認できたのは二次報道のみで、一次情報は未確認である(The Neuron)
- Ideogramのベクター生成: 文章の指示から拡大しても劣化しないSVGファイルを生成でき、既存の画像のベクター化にも対応する。文字や色のグラデーションも扱えるとされる。一次情報は未確認(同上)
- Carbon-X: Hugging Faceが公開したゲノム研究向けのモデルで、DNAの配列を解析し、新しい配列を生成でき、自然言語で操作できると伝えられている。基になったCarbonは、Apache 2.0ライセンスで重みと学習コードを公開した、500M・3B・8Bの3種類のDNA基盤モデルで、Carbon 3Bは既存のEvo2 7Bと同等の勝率を約275倍の処理速度で出すと開発側が説明している(自己報告)。Carbon-Xの公開形態や入手先は今回確認できなかった(The Neuron、Runtime Wire)
AI開発手法
AIが書いたコードを証明で検証する
上のClaudeの検証は、開発手法としても読める。テストで見つからなかった不具合を、仕様(何が起きてはならないか)を明示して証明で潰す方法である。再現に必要な条件は、既存のファズテストの入口があることと、証明検査ツールを動かす計算資源である。今回の規模は、生成に約10億行を要しており、個人が手元で試せる水準ではない(Unite.AI)。
エージェントの監視は第三者の目で点検する
METRとRedwood Researchの外部評価者は、OpenAI社内に3週間入り、エージェントの不整合を見つける内部の監視システムを点検した。複数の脆弱性が見つかり、その1つはエージェントが数百件の行動を監視から隠せるものだったという。エージェントを運用する場合、ログや監視の仕組み自体を外部から点検することが、設計の要になる(The Neuronの報道。評価の詳細は未確認。The Neuron)。
AIを使った新サービス
- 1Passwordが、AIエージェント向けの認証情報の保護基盤を公開した。エージェントがパスワードを直接見ずに作業できる仕組みとされる。詳細は一次情報を確認できていない(The Neuron)
- 米国の大手銀行が、第三者のAIエージェントが顧客口座にアクセスするリスクへの対応を進めている。銀行は、ある操作が顧客の指示なのか、エージェントが範囲を超えて動いたのかを判別する必要があるとされる(同上)
トレンドのAI活用法
特筆すべきトレンドなし。
LLM性能比較・得意分野
新しい比較情報なし。HeyGen Video 1の順位は、二次報道のみで評価条件を確認できていない。Carbonの速度比較は開発側の自己報告である。Microsoftの診断AIの精度は論文の報告で、条件の詳細は未確認である。
研究・技術
Claudeの形式検証は、AIが生成した証明を、証明検査ツールが機械的に確かめるため、人手で巨大な証明を一行ずつ審査せずに済む点が新しい。近いうちに道具として広く使えるかは、対応する実行環境の範囲が広がるかにかかる(見立て)。MicrosoftのKannan-Lovász-Simonovits予想の解決は、人が方向づけたAI研究の成果として報告されているが、今回は詳細を確認できていない(The Neuron)。
