基調講演：AIによる形式検証と形式検証におけるAIの役割
DAY 1
9:00-
9:45
10年以上前から、形式検証（formal verification）のワークフローは、悪用可能なバグのないソフトウェアを作成するのに十分であることが知られており、また必要であるようにも見える。AIシステムは、これらのワークフローを支援する能力が急速に向上しており、より専門性の低いエンジニアでもこれらのワークフローを利用できるようになっている。AIは他の多くのワークフローも支援可能だが、サイバーセキュリティにおいて実益をもたらすほどに信頼性を高めるためには、依然として何らかの形式検証が必要であると考えられる。また、AIは機能正確性のレベルだけではなく、分散システムの並行処理からハードウェアの電磁気学にいたるまで、他の抽象化レベルでの形式検証も使用できる。数年以内に、形式検証が「実用的」と見なせる範囲は飛躍的に拡大し、サイバー攻撃の多くの形が過去のものとなるだろう。同時に、形式検証とサイバーセキュリティは、ますます強力になるAIシステムが暴走して世界的な惨事を引き起こさないように保証し、確実にする上で重要な役割を果たすことになる。われわれの未来は明るいかもしれないが、そのためにはコミュニティが協力して取り組む必要がある。
-
Location :
-
Track 1(HALL B)
-
-
Category :
-
Keynote
-
-
Share :
Speakers
-
David A. Dalrymple (davidad)
デビッド・A・ダリンプル（davidad）
ARIA（英国高等研究発明庁）の「Safeguarded AI」プログラムのディレクターを務める研究科学者。専門はAIの安全性と計算論的神経科学であり、仮想通貨Filecoinのプロトコル共同発明や、Protocol Labsにおける公共財への資金調達のためのHypercertsメカニズム開発などの実績があるほか、Twitter社ではシニア・ソフトウェア・エンジニアを務め、オックスフォード大学で技術的なAIの安全性に焦点を当てた研究員を務めた経歴を持つ。
ダリンプル氏は、AI技術の安全な導入を目指した、人間が監査可能なAIモデルの開発への貢献で知られており、現在もまた、高い信頼性を持つ倫理的なAI配備の必要性の高まりを背景に、原子力産業や航空産業などに並ぶ強固な安全保証を備えたAIシステムの開発を推進している。