Imandraを用いて形式検証を触ってみた

概要

この記事では、形式検証の概要や意義について説明するとともに、形式検証ツールImandraの使用例を紹介します。読者の想定としては、形式検証やImandraに馴染みのない方を考えています。

形式検証について

情報化が進んだ現代、プログラムにおけるバグは社会に深刻な悪影響を及ぼすことがあります。特に医療・航空・宇宙・金融等、安全性や正確性が重要視される分野ではなおさらです。また最近では、AIが生成したプログラムにおいて、いわゆる「ハルシネーション」（生成内容が正しくない現象）が発生し、常に正しいプログラムが生成されるわけではないという課題も浮き彫りになっています。

このような課題に対する解決策の一つとして注目されているのが、形式検証です。形式検証は、プログラムが特定の仕様を満たしていることを数学的に証明する手法です。一般的なテストでは作成したテストケースに対してしかプログラムの正当性を保証できませんが、形式検証を用いると任意の入力値に対してもプログラムの正当性を保証することが可能となります。

Imandraについて

Imandraは、プログラムの形式検証を支援するツールで、関数型言語OCamlをベースに開発されています。Imandraでは、プログラムやその仕様をOCamlで記述し、数学的手法を用いてその正当性を検証します。

公式サイトでは、近年のAI技術の普及に伴う課題に対応するため、AI生成コードに関連する問題点とそれに対する形式検証の有効性が強調されています。

実際にImandraを触ってみる

今回は、Imandraが提供するJupyter Notebook形式のオンライン環境を利用して、簡単な形式検証を試してみました。

検証対象のプログラム・仕様

プログラム

以下の条件を満たす関数$\mathit{sum}$

• 入力: 整数$n$
• 出力:
  • $n \leq 0$ の場合、$0$
  • $n \gt 0$ の場合、$1$から$n$までの総和 $1 + 2 + \cdots + n$

検証したい仕様

任意の整数$n$に対し、$n \leq \mathit{sum}(n)$ が成り立つ

OCamlでの実装

(* 検証対象のプログラム *)
let rec sum n =
  if n <= 0 then
    0
  else
    n + sum (n - 1)

(* 検証したい仕様 *)
verify (fun n -> n <= sum n) [@@auto]

検証結果

中央にProvedと表示されていることから、このプログラムが仕様を満たしていることをImandraが証明したことが分かります。さらにログを見ると、数学的帰納法に基づき以下の2つの命題に分割して証明したことを確認できます。¹

• (Subgoal 1.2) $n \leq 0$ ならば $n \leq \mathit{sum}(n)$
• (Subgoal 1.1) $n \gt 0$ かつ $n - 1 \leq \mathit{sum}(n-1)$ ならば $n \leq \mathit{sum}(n)$

このように、Imandraを用いることで簡単にプログラムの正当性を保証することができました。

エラー検出の例

次に、else節内の+演算子を誤って-に書き換えてしまった場合を試してみましょう。

(* 検証対象のプログラム *)
let rec sum_err n =
  if n <= 0 then
    0
  else
    n - sum_err (n - 1)

(* 検証したい仕様 *)
verify (fun n -> n <= sum_err n) [@@auto]

Imandraはこのプログラムが仕様を満たさないことを検出し、反例として $n=2$ の場合を提示します。このようにして、潜在的なバグを未然に防ぐことができます。

最後に

この記事では、形式検証とその重要性、さらにツールImandraを用いた具体例を紹介しました。形式検証は、特に安全性や正確性が求められる分野で大きな価値を持つ手法です。

この記事では簡単な例しか扱いませんでしたが、Imandra公式サイトのデモページではさらに応用的で興味深い例も紹介されていますので、ぜひそちらも参考にしてみてください。

• Analysing Web-app Authentication Logic
• Solving Sudoku with Imandra
• Verifying Merge Sort in Imandra
• 等々

1. それぞれの命題の証明の詳細に関しては、ログに記載されていないため省略します。 ↩