形式検証の最前線

2026年、大規模言語モデルは、長年未解決だった数学の問題を解けるほどに進歩した。その一方で、AIによる脆弱性の発見や攻撃コードの作成も高度化し、AIを用いたサイバー攻撃の脅威が深刻化している。では、近年のAIの定理証明能力の進歩を利用して、実際に使われているソフトウェアのセキュリティを保証し、この問題に対処できないだろうか。 本講演では、多くのデバイスで実際に使われているC言語製ハイパーバイザーpKVMを対象に、AIを活用した形式検証手法を紹介する。我々の手法では、検証のためにソフトウェアを一から作り直すのではなく、既存のCコードに対してセキュリティに関する性質を直接証明する。 AIエージェントの進歩により、形式検証の主なボトルネックは、証明の構築から、ソフトウェアの振る舞いを正確に仕様として記述し、検証対象のシステムを忠実にモデル化する作業へと移りつつある。この課題に対処するため、我々はCerberusによるC言語の形式意味論を基盤とし、分離論理に基づく検証システムCNを開発し、利用する。このシステムは、テスト、SMTを用いた半自動検証器、Leanに基づく高度な推論を統合したものである。これにより、人間が仕様を記述・レビュー・改良する負担を減らしながら、AIエージェントが与えられた性質をできる限り自律的に証明できる環境を実現する。本講演では、このシステムを実際に使って得られた経験についても紹介する。

TBA

信号時相論理（Signal Temporal Logic: STL）は、自律移動ロボットの満たすべき時間的・空間的なタスクを形式的な仕様として記述することができる。また、ロバストネススコアとよばれる量的なセマンティクスによって、そのSTL仕様がどの程度満たされるかを評価できる。本講演では、ロボットの軌道計画問題を対象として、STLによる仕様記述とニューラルネットワーク（NN）制御器について紹介する。より具体的には、状態を入力として制御入力を出力するNN制御器を考え、システムのダイナミクスのもとで生成される軌道がSTL仕様を満たすように、ロバストネススコアを用いて学習させる。さらに、複雑かつ長時間のタスクへの対応に向けて、STL仕様の構造を陽に考慮したMixture-of-Experts（MoE）アーキテクチャに基づくNN制御器を紹介する。

Natural-language robot commands can admit different logical scopes, leading to well-formed but behaviorally different control specifications. Using Combinatory Categorial Grammar (CCG), we translate timed commands into a set of Signal Temporal Logic (STL) candidates. A constrained CCG parser retains alternative syntactic analyses, task-typed composition assigns explicit temporal meanings, and meaningpreserving rewrites group duplicate STL candidates while retaining links to their source parse trees. This allows a designer to inspect scope choices and diagnose unsupported commands before committing to a planning specification. In direct comparison with a large-language-model (LLM) API, the methods often produce identical candidate sets when both return outputs, while the API covers a broader range of commands.

Cyber-physical systems (CPS), which integrate computational control with physical processes, require high reliability because they are often deployed in safety-critical domains. Ensuring that such systems satisfy their formal specifications is challenging, since modern CPS often contain complex or opaque components, such as deep neural networks, whose internal structures are not fully accessible. Moreover, obtaining formal specifications themselves can be challenging, as requirements are often described only informally or implicitly. In this talk, we discuss how active automata learning can address these challenges by learning formal models of black-box systems and implicit specifications. Black-box checking (BBC) is a workflow for systematic testing of black-box systems by learning an approximate automaton for the system under test using active automata learning and verifying it using model checking. This talk presents how to use BBC for specification-based testing of CPS and several techniques to improve its efficiency. Supervisory control theory provides a framework for synthesizing supervisors that restrict system behavior to satisfy given specifications. We discuss supervisory control with implicit specifications, where active automata learning is used to infer a formal specification. These two applications illustrate the usefulness of automata learning in both formal verification and control of discrete-event systems.

Partial observability is a central notion in the verification and control of systems whose internal states cannot be directly observed. For partially observable Markov decision processes (POMDPs), the standard belief construction transforms the system into a fully observable Markov decision process over belief states, preserving the maximal expected reward. In this talk, we present a coalgebraic framework that generalizes the belief construction beyond probabilistic systems. The construction combines coalgebraic determinization with a belief decomposition, which reorganizes branching states according to their observations. We establish conditions under which this construction preserves semantics, and further identify when the resulting belief system can be treated as fully observable without changing its semantics. Our framework recovers the standard equivalence between POMDPs and belief MDPs and yields a new equivalence result for weighted transition systems.

Finding Lyapunov functions to certify the stability of control systems has been an important topic for certifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces the transparency. Hence, a method for black-box systems would have much wider applications.

Our work stems from the idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a non-statistical upper bound on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination.

Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. In comparison with the existing black-box approach, our approach at the best case requires less than 0.01% of samples.

Linuxカーネルドライバにおける参照カウントバグは、様々なセキュリティ脆弱性につながる。本研究では、Linuxドライバのインターフェースを活用して参照カウントの検証を assertion検査問題に帰着させることで、これらのバグを検出する新しいツールDrvHornを提案する。Linuxカーネルの効率的なモデル化とスライシングにより、DrvHornはLinuxカーネルv6.6の全platform driverを対象に545件のバグを発見し、そのうち424件は未知のバグであった。また、偽陽性率は29.9%と、先行研究より低かった。新たに発見したバグの根本原因を修正する45件のカーネルパッチが mainlineにマージされた。 加えて、Googleで取り組んでいる定理証明を用いた形式検証にも補足的に触れる

AIの強力さとあやふやさが社会一般に知られた結果，形式手法・論理的手法が提供できる価値に対して，社会的関心が急速に高まっています．ここで重要なのは，我々がこれら手法について (1) 社会にどう説明するか，また (2) 社会の中でどう使うか，です．この２点について，大学発スタートアップを通じた研究成果の社会応用の現場で得られた知見をお話します． また，AI の影響は理論研究コミュニティでも絶大であり，各研究者が自らの役割の再検討を迫られるとともに，国際学会等の仕組みが大きく変わろうとしています．大きな国際学会の PC co-chair として，この荒波にもまれている現在進行形の経験から，知見をいくつかお話します．(トークは一部日本語です)