Amazon Web Services ブログ

Isabelle/HOL: Nitro Isolation Engine を支える定理証明支援系

Amazon Web Services (AWS) は、定理証明支援系 Isabelle/HOL を用いて Nitro Isolation Engine (NIE) の正当性とセキュリティ保証を検証し、世界初の形式的に検証されたクラウドハイパーバイザーを実現しました。本記事では、ブール論理から一階述語論理、高階論理、依存型理論に至る数理論理の言語階層を解説し、Isabelle/HOL が備える数学的な記述の表現力、自動化、スケーラビリティのバランスや、sledgehammer やロケールなどの主要機能、seL4 や CRDT などの応用事例を紹介します。

Outpost VFX が ビジュアルエフェクト向けに AI モデルのトレーニングを AWS で加速した方法

本記事では、Outpost VFX が AWS インフラを活用してトレーニング速度を 8 倍に向上させ、顔置換ワークフローを刷新した方法、単一 GPU の限界を克服するために実装した技術アーキテクチャ、そして AWS マルチ GPU トレーニングで得られた具体的な成果について紹介します。

【開催報告】AWS Summit Japan 2026 物流業界向けブース展示「スマートグラス×生成AIエージェントで倉庫業務を革新」

こんにちは、ソリューションアーキテクトの田邊です。2026 年 6 月 25 日から 26 日にかけて幕張メッ […]

Reimagine your mainframe applications with Agentic AI and AWS Transform

エージェンティック AI と AWS Transform でメインフレームアプリケーションを再構想 (reimagine) する

本ブログでは、reimagine パターンによってメインフレームのレガシーアプリケーションをモダナイズする AWS のアプローチの概要を説明し、組織がレガシー COBOL アプリケーションをモダンなクラウドネイティブアーキテクチャに変換する方法を紹介します。

週刊生成AI with AWS – 2026年7月20日週

週刊生成AI with AWS, 事例と Summit 開催報告が揃った 2026 年 7 月 20 日号 – 弁護士ドットコム株式会社様の AWS DevOps Agent 活用事例と、株式会社NTTドコモ様・KDDI株式会社様・ソフトバンク株式会社様の展示レポートを紹介。また、9 社合同 AI-DLC Unicorn Gym や Claude・Kiro 実践ワークショップなどのブログ記事も。サービスアップデートでは Claude Opus 5 の AWS 提供開始や Amazon CloudWatch のコーディングエージェントインサイトをはじめとする 12 件を紹介。

← Older posts
Newer posts →