AI・LLM デイリーブリーフィング
2026年10月25日（日）｜日本時間 8時時点
今日の最重要ニュースは、AnthropicがClaudeを使い、123のオープンソースライブラリについて、特定条件下でクラッシュしないことを数学的に証明した研究成果です。
約1億8,000万行の形式的証明をAIが生成し、独立した証明器が検証しました。従来のソフトウェアテストを大きく変える可能性があります。
開発基盤では、AWSがGPU管理不要のモデル追加学習機能を一般提供し、Google CloudはAIエージェント専用の実行環境を発表しています。
今回は10月22〜23日の公式発表・技術資料から、前回までと重複しない重要ニュースを5件選びました。10月24〜25日に発表された大型LLMの新モデルについては、今回の調査で確実な一次情報を確認できなかったため、直近の重要な技術リリースを中心に紹介します。
1. 【最重要】Anthropic、Claudeで123のOSSライブラリを形式検証 — 約1億8,000万行の証明を生成
発表：10月22日｜新研究・検証コード公開
Anthropicが、形式検証企業Theoremとの共同研究を発表しました。
Claudeを使い、123のオープンソースライブラリに含まれる239のテスト用エントリーポイントについて、特定の条件下でクラッシュしないことを数学的に証明しています。
対象はコンパイル済みのRISC-Vバイナリで、生成した証明はRocqという形式的証明システムで検証されました。証明の過程では、従来のファジングで長年発見されなかった不具合も検出しています。
なぜ重要か
従来のテストは、有限個の入力に対して正しく動くことを確認する方法です。
今回の技術は、定義した条件を満たすすべての入力について、特定の不具合が発生しないことを証明するものです。
技術・実装ポイント
| 項目 | 研究結果 |
|---|---|
| 対象ライブラリ | 123 |
| 検証したエントリーポイント | 239 |
| 証明コード | 約1億8,000万行 |
| 典型的な証明の規模 | 約60万行 |
| 入力サイズ | 64MB未満 |
| 対象アーキテクチャ | RISC-V |
| 証明システム | Rocq |
仕組みは次のとおりです。
text既存のOSSライブラリ
↓
OSS-Fuzzのテスト
↓
形式的な仕様へ変換
↓
Claudeが証明を生成
↓
Rocqが数学的に検証
↓
証明失敗時は不具合を調査
↓
必要に応じて修正・再証明性能： Claude Opus 5.5は、36件の小規模検証課題において、Opus 5より約40%少ないトークンで半数の課題を証明しました。
コスト： 大規模な証明には数億トークンを必要とする場合があり、一般的なCIへそのまま導入するには費用面の課題があります。
利用条件： 証明の一部、RISC-VとOSの形式的モデル、開発者向けClaude Skillが公開されています。
重要な制限： 今回の証明は、単一スレッド、静的リンク、固定メモリ予算などを前提としています。x86やARMで実行するすべての構成について安全性が保証されたわけではありません。
特に注目したいのは、AIが証明を生成し、その正しさはAIではなく独立した証明器が判定していることです。
2. AWS、SageMaker AIのGPU管理不要な追加学習機能を一般提供
発表・一般提供：10月22日｜新機能リリース
Amazon Web Servicesが、SageMaker AI Serverless Model Customizationの「Training Sessions」を一般提供しました。
GPUインスタンスの選択、分散学習クラスタの構築、障害復旧などをAWSに任せながら、開発者が独自の学習ループを実装できます。
教師ありファインチューニングだけでなく、DPO、GRPO、複数ターンの強化学習にも対応します。Claude CodeやCodexなどから学習処理を支援するAgent Skillsも公開されています。
なぜ重要か
これまで独自モデルの強化学習を実行するには、GPUの確保、学習環境の構築、分散処理の管理が必要でした。
今回の機能では、開発者は報酬関数と学習アルゴリズムの実装に集中できます。
技術・実装ポイント
例えばGRPOでは、次の処理を繰り返します。
text学習対象モデル
↓
複数の回答を生成
↓
テスト・評価プログラム
↓
回答ごとに報酬を計算
↓
勾配を計算
↓
モデルの重みを更新
↓
次の学習ステップ対応モデル： gpt-oss-20b、gemma-4-31B-it、Qwen3.6-27B、Qwen3.8-27B。
API・SDK： SageMaker Python SDKを利用。Python 3.10〜3.12のLinux・macOS環境から開発できます。
学習方式： SFT、DPO、RLVR、RLAIF、Multi-Turn RL。LoRAとフルファインチューニングも選択できます。
料金： SageMakerが処理するトークンに基づく従量課金です。GPU容量を事前予約する必要はなく、外部の報酬関数が評価している間は学習処理の課金メーターが停止します。ただし、報酬関数を実行するAWSリソースなどには別途料金が発生する場合があります。
データ管理： 学習データとチェックポイントは利用者のS3に保存され、IAM、KMS、VPCによる制御が可能です。
10月23日公開の実装例
翌23日には、複数ターンの強化学習を実装するチュートリアルも公開されました。
Wordleを題材にgpt-oss-20bを追加学習したところ、未学習の単語に対する正解率が61%から84%に改善しています。
低い推論努力設定では、15%から69%へ改善しました。学習トークン費用は約339ドルと報告されています。
これは特定のゲーム課題での結果ですが、小型モデルを特定の業務に特化させる設計として参考になります。
3. Google Cloud「Agent Compute Engine」発表 — AIエージェント専用のmicroVM実行環境
発表：10月22日｜プレビューは今後数か月以内
Googleが、AIエージェント専用の実行基盤「Agent Compute Engine」を発表しました。
各エージェントにハードウェアレベルで分離されたmicroVMを割り当て、コード実行、ブラウザ操作、ツール呼び出しを安全に実行します。
最大の特徴は、エージェントがLLMの推論や人間の承認を待っている間、VMを一時停止してリソースを解放できることです。
また、Kubernetes向けのオープンソース実行基盤「Agent Substrate」も紹介しています。
なぜ重要か
AIエージェントは通常のWebアプリケーションと異なり、実際にCPUを使用している時間よりも、LLMの応答や外部ツールを待っている時間が長くなることがあります。
従来のVMやコンテナでは、この待機時間にも計算資源を確保し続ける構成になりがちです。
今回の技術は、エージェントの状態を保持したまま実行環境を停止・再開することで、計算資源の利用効率を高めます。
技術・実装ポイント
textAI Agent
↓
Agent Compute Engine
↓
専用microVM
│
├─ コード実行
├─ ブラウザ操作
└─ ツール呼び出し
↓
LLMの応答待ち
↓
VMを一時停止
↓
必要になったら復元
↓
処理を再開仮想化： Cloud Hypervisor、Google Titanium。
状態保持： チェックポイントとスナップショットによる高速復元。Hyperdiskによるワークスペースの永続化。
認証： microVMごとに独立したIDと短命の認証情報を使用。
監視： Agent Gatewayと統合し、アクセス制御や実行状況を監視できます。
公表された性能
GoogleのAgent Substrateに関する検証結果です。
| 項目 | 結果 |
|---|---|
| 計算資源の収容密度 | 従来比最大10倍 |
| 検証したエージェント数 | 20万 |
| アクティベーション処理能力 | 毎秒500件 |
| 一時停止・復元遅延 | 500ms未満 |
これらはGoogleの特定環境における測定値であり、Agent Compute Engine本体の一般提供性能を保証するものではありません。
API・利用条件： Agent Compute Engine本体は今後数か月以内にプレビュー提供予定です。正式な料金、提供リージョン、一般利用可能なAPI仕様は未発表です。
一方、Agent SubstrateはKubernetes環境で利用できるオープンソース基盤として公開されています。
4. Microsoft、Work IQとDataverseを拡張 — 業務データを理解するAIエージェント
発表：10月23日｜Public Preview
Microsoftが、企業向けAIエージェント基盤「Work IQ」とDataverseの機能拡張を発表しました。
業務データの意味やレコード間の関係をセマンティックモデルとして定義し、CopilotやAIエージェントが共通の業務知識を利用できるようにします。
また、業務ルールを再利用可能な「Business Skills」として管理し、承認条件や権限を考慮した操作を実行できます。
Dataverse Ask APIやMCP Serverの拡張など、開発者向け機能もPublic Previewとして公開されています。
なぜ重要か
企業のAIエージェントでは、LLMがデータを理解できるだけでは不十分です。
例えば「顧客の契約を変更する」という処理では、顧客情報、契約条件、承認権限、変更履歴などを正しく扱う必要があります。
今回の仕組みは、企業の業務ルールとデータ構造を、複数のエージェントが共有するための基盤です。
技術・実装ポイント
Dataverse Ask API： 業務データに対する自然言語の問い合わせを提供。Web APIとDataverse Connectorから利用できます。
MCP： Dataverse MCP ServerからCustom APIを呼び出せるようになりました。
対応開発環境： Claude Code、OpenAI Codex、GitHub Copilotなどとの連携を拡張。
Business Skills： 業務処理を再利用可能なスキルとして定義し、バージョン管理や権限制御が可能です。
ワークフロー： n8nのDataverseノードによる自動化にも対応。
料金： 今回の発表では新機能ごとの統一料金は示されていません。Dataverse、Power Platform、Copilotなどの契約条件を個別に確認する必要があります。
利用条件： Public Previewの機能が含まれるため、本番利用時にはプレビュー機能のサポート条件と管理者による有効化設定を確認してください。
5. 【日本】DAIJOBU、Claudeを活用したWeb・API脆弱性診断サービスを開始
発表・提供開始：10月23日｜国内新サービス
日本のDAIJOBUが、WebアプリケーションとAPIを対象とした新しい脆弱性診断サービスを提供開始しました。
Claudeを使用して検証案の洗い出しと実行を補助し、最終的な診断内容や結果の判断はセキュリティエンジニアが担当します。
特徴は、一般的な脆弱性だけでなく、申請と承認の順序、利用者と管理者の権限差など、業務ロジックに依存する脆弱性を検証することです。
AIを使った自動診断と、人間による業務仕様の理解を組み合わせています。
なぜ重要か
AIによるコード生成が高速化すると、ソフトウェアの品質保証が重要になります。
特に、コード自体に明らかな脆弱性がなくても、業務上の権限や承認手続きに問題がある場合があります。
今回のサービスは、AI駆動開発で見落としやすい業務ロジック上の問題を検証することに重点を置いています。
開発者が見るべきポイント
使用AI： Claude。AIが生成した検証案を専門エンジニアが確認したうえで実行します。
対象： Webアプリケーション、REST APIなどのAPIインターフェース。
検証内容： 認可、権限昇格、承認処理の迂回、他ユーザー情報への不正アクセスなど。
報告： 再現手順、証跡、修正方法を含むレポートを提供。重大な問題は発見後、翌営業日までに通知します。
料金： ライト診断は30万円（税別）から。詳細な診断は個別見積もりです。
API・SDK： 外部開発者が診断処理を直接呼び出すためのAPIやSDKは発表されていません。
データ保護： Claudeには送信データを学習に利用しない契約条件を適用し、AIを使用する範囲は診断開始前に顧客と合意する方針です。
今日いちばん注目すべき1件
Anthropic「Claudeによる大規模な形式検証」
今日の5件では、Claudeによる123のOSSライブラリの形式検証を選びます。
理由は、AIによるソフトウェア開発の品質保証が、従来の「テストを実行して不具合を探す」方法から、数学的な証明によって特定の不具合が存在しないことを確認する方法へ進む可能性を示したからです。
特に重要なのは、証明の正しさをLLM自身に判断させていないことです。
AIが生成した証明を、独立したRocqの証明器が検証しています。
これはCoding Agentの設計にも応用できる考え方です。
textAIがコードを生成
↓
自動テスト
↓
静的解析
↓
形式的な仕様を生成
↓
AIが証明を作成
↓
独立した証明器で検証
↓
CI/CDで合否判定もちろん、今回の研究はまだ一般的なWebアプリケーション全体を形式検証できる段階ではありません。
それでも、形式的に検証できる範囲を広げるための技術的な進展として、非常に重要です。
今日の結論： AIがコードを書く能力だけでなく、そのコードが正しいことを機械的に証明する能力が、今後のソフトウェア開発を変える可能性があります。