Isabelle/Isar勉強会を社内で開催しました

こんにちは、SWETグループの鈴木穂高（@hoddy3190）です。

SWETグループのメンバー向けにIsabelle/Isar勉強会を開催しました。本記事では、勉強会の概要の紹介と、勉強会の資料の公開をします。

もしよろしければご活用ください。

Isabelleとは

Isabelleは、定理証明支援ツールの1つです。数学の授業で証明を解く時、暗記した定義や定義を引き出して仮定や結論をみて試行錯誤しながら適用して解いていっていたと思います。Isabelleを使うと、利用できる定理を提示してくれたり、自動で定理を適用して証明を進めてくれたり、誤った証明を指摘してくれたりします。

Isabelleの大きな特徴として強力な自動証明が挙げられます。自動証明機能の典型例であるSledgehammerは、証明したい論理式を与えれば自動で定理を適用して証明を解き進めてくれます。公理系も選択可能です。よく使われるのはHOLですが、他にもFOLやZFなどを扱えます。 Isabelleの実績として、オペレーティングシステムの機能に関する証明に使われました。¹

Isabelleには証明の記述方法が2種類あります。apply-scriptsとIsarです。今回の勉強会で用いているのはIsarです。Isarは今何を証明しているのかを宣言して証明を書くためapply-scriptsより読みやすいという特徴があります。

業務でのIsabelleの用途

仕様と実装に正当性関係が成り立つことを証明するのに使えます。仕様と実装の正当性関係とは、実装が仕様を満たしているかどうかの関係のことを言います。

私はSWETグループにて仕様の欠陥をなるべく早くみつける取り組みにチャレンジしています。詳細はこちらの記事の「発表内容」のスライド資料または動画をご覧いただければと思いますが、簡単にいうと仕様を形式仕様記述するというアプローチで取り組んでいます。

正当性関係が成り立っていることは論理式で表せますので、仕様と実装が形式的に書かれていれば、実装が仕様を満たしているかをIsabelleのような定理証明支援ツールを使って証明ができます。私はOCamlで記述した仕様と実装をIsabelleが読める形にトランスパイルして、正当性関係が成り立つことを証明しました。

Isabelle/Isar勉強会の概要

正当性関係が成り立っているとはどういうことなのかは、Isabelleを使って証明を進めることで理解が深まります。さらには証明の手順が分かると、正当性関係が成り立つことを証明されるのを見越して、仕様はこう書けばよい、仕様に対して実装はこう書けばよいといった勘所も養われます。このようなメリットのため、SWET内でIsabelle/Isarを学ぶための勉強会を開催しました。

勉強会は毎週1時間リモートミーティングで開催しました。参加メンバーの人数は5,6人です。参加メンバー全員がIsabelleをapply-scriptsで使ったことがある方でした。実はこの勉強会よりも前に、Isabelleの基本的な使い方や、仕様と実装をIsabelleで記述し正当性関係に関する証明のやり方を学ぶ別の勉強会があり全員そこの参加者でした。ただ本資料はIsabelle初学者でも分かるように作っています。

1時間の勉強会の内容は、座学と練習問題です。座学では毎回私が資料をベースに説明をし参加メンバーと質疑応答を行います。その後用意してある練習問題を参加メンバーに解いてもらいます。毎回平均して30分ほど座学、残り30分ほどは演習問題を解く時間でした。時間内に解ききれなかった練習問題は可能であれば別途各自で時間をみつけて次回の勉強会までに解いてもらうようにしました。勉強会は合計7回開催しました。

参加メンバーからのフィードバックとして次のようなものが得られました：

簡単な定理から徐々に証明していく形だったので、以前の勉強会に付いていけてなくても何とかなったのが良かったです。
apply-scriptsのほうが慣れている分楽な気がします。一方、apply-scriptsは確かにIsabelleを動かさないと何をしているのかがわからないですが、Isarだと読むだけでわかりそうでそこはよさそうに思います。

Isabelle/Isar勉強会の資料と練習問題

資料
資料中に出てくるサンプルと練習問題
- https://github.com/DeNA/IsarTutorial/blob/main/IsarTutorial.thy
練習問題解答例
- https://github.com/DeNA/IsarTutorial/blob/main/IsarTutorial_Answer.thy

Isabelleの特徴は先に述べたとおり強力な自動証明ですが、今回の練習問題では自動証明は極力使わないよう解答してもらいました。基本的な定理を理解した上で、定理を使って少しずつゴールをrefineしていくことがIsabelle/Isarに慣れるためには必須だと思ったからです。ですから、もし練習問題を解く際は極力自動証明を使わないことをお勧めします。