【CODE BLUE 2024】デビッド・A・ダリンプル / David A. Dalrymple (davidad) - 講演関連資料 / Presentation resources -
●講演概要 / Abstract
[ja] 基調講演：AIによる形式検証と形式検証におけるAIの役割
10年以上前から、形式検証（formal verification）のワークフローは、悪用可能なバグのないソフトウェアを作成するのに十分であることが知られており、また必要であるようにも見える。AIシステムは、これらのワークフローを支援する能力が急速に向上しており、より専門性の低いエンジニアでもこれらのワークフローを利用できるようになっている。AIは他の多くのワークフローも支援可能だが、サイバーセキュリティにおいて実益をもたらすほどに信頼性を高めるためには、依然として何らかの形式検証が必要であると考えられる。また、AIは機能正確性のレベルだけではなく、分散システムの並行処理からハードウェアの電磁気学にいたるまで、他の抽象化レベルでの形式検証も使用できる。数年以内に、形式検証が「実用的」と見なせる範囲は飛躍的に拡大し、サイバー攻撃の多くの形が過去のものとなるだろう。同時に、形式検証とサイバーセキュリティは、ますます強力になるAIシステムが暴走して世界的な惨事を引き起こさないように保証し、確実にする上で重要な役割を果たすことになる。われわれの未来は明るいかもしれないが、そのためにはコミュニティが協力して取り組む必要がある。
[en] Keynote: AI for formal verification; formal verification for AI
For over a decade, it has been known that formal verification workflows are sufficient to create software that is free of exploitable bugs. It also appears to be necessary. AI systems are increasing rapidly in their ability to assist in these workflows, and to make them accessible to increasingly less specialist engineers. While AI can also assist with many other workflows, formal verification in some form still seems to be necessary to make AI reliable enough to provide a net benefit to cybersecurity. AI could also be used to formally verify at other levels of abstraction than functional correctness, from the concurrency of distributed systems down to the electromagnetics of the hardware. In a small number of years, this will vastly expand the scope of what can be considered “practical” to formally verify, and most forms of cyberattack will become history. At the same time, formal verification and cybersecurity have crucial roles to play in ensuring and assuring that increasingly powerful AI systems do not go rogue and cause a global catastrophe. Our future could be bright, but our communities need to work together.
●略歴 / Bio
[ja] デビッド・A・ダリンプル（davidad）
ARIA（英国高等研究発明庁）の「Safeguarded AI」プログラムのディレクターを務める研究科学者。専門はAIの安全性と計算論的神経科学であり、仮想通貨Filecoinのプロトコル共同発明や、Protocol Labsにおける公共財への資金調達のためのHypercertsメカニズム開発などの実績があるほか、Twitter社ではシニア・ソフトウェア・エンジニアを務め、オックスフォード大学で技術的なAIの安全性に焦点を当てた研究員を務めた経歴を持つ。
ダリンプル氏は、AI技術の安全な導入を目指した、人間が監査可能なAIモデルの開発への貢献で知られており、現在もまた、高い信頼性を持つ倫理的なAI配備の必要性の高まりを背景に、原子力産業や航空産業などに並ぶ強固な安全保証を備えたAIシステムの開発を推進している。
[en] David A. Dalrymple (davidad)
David A. Dalrymple is a highly regarded research scientist currently leading the Safeguarded AI program at ARIA (the UK’s Advanced Research and Invention Agency). His expertise lies in AI safety and computational neuroscience, and he is known for his contributions to developing mathematically grounded, human-auditable AI models. These models aim to ensure safe deployment of AI technologies while maximizing their potential to benefit society.
Dalrymple has an impressive background that includes co-inventing the Filecoin protocol and developing the Hypercerts mechanism for public goods funding at Protocol Labs. He has also worked as a Senior Software Engineer at Twitter and held a research fellowship at Oxford University focused on technical AI safety
In his current role, Dalrymple is exploring the development of AI systems with strong safety guarantees, comparable to those in industries like nuclear power and aviation. His work is vital in addressing the growing need for reliable and ethical AI deployment in critical contexts.
●講演動画 / Presentation video
●写真 / Photo
●レポート記事 / Reports
[ja] [レポート]基調講演：AIによる形式検証と形式検証におけるAIの役割 - CODE BLUE 2024（Developers IO / クラスメソッド）