定理証明支援系についての問題意識

定理証明支援系 (proof assistant / interactive theorem prover) というのは、専用の言語で書いた証明を機械にチェックさせるツール、およびその証明の記述を支援するツールです。Rocq（旧名Coq）、Agda、Lean、Isabelleなどが有名です。

この記事では、定理証明支援系について私が感じている問題意識を説明します。私自身は定理証明支援系のヘビーユーザーではないので、もっと勉強したり、定理証明支援系を使い込んだりすれば答えが見つかるのかもしれません。詳しい方からのフィードバックを頂けると嬉しいです。

このブログでは、過去に定理証明のできる依存型プログラミング言語Idrisを使った定理証明を扱いました。10年以上前ですが……。

私は過去にCoq（現Rocq）による定理証明の動画を作ったこともあります（2021年ごろ）。私自身がCoqの初心者なので、内容は初歩的なものです。

証明の可読性

まず、証明の可読性についての問題意識を述べます。

Rocqでは、証明の本体はtacticと呼ばれる命令の羅列として書くことが多いです。もちろん、カリー・ハワード対応に基づいているので、証明を表す項 (proof term) を書いて証明とすることもできますが、よっぽど簡単なものでない限りtacticを使うことが多いと思います。

例えば、私が動画で実演した定理の証明は、テキストだとこんな感じになります：

Theorem thm3b : forall (n : nat) (k : Z), (Z.of_nat n < k)%Z -> binom n k = 0.
Proof.
induction n.
(* n = 0 *)
intro.
case k.
discriminate.
trivial.
discriminate.
(* Induction step *)
intros.
cbn.
rewrite (IHn k).
rewrite Nat.add_0_r.
rewrite (IHn (Z.pred k)).
trivial.
assert (Z.succ (Z.of_nat n) < k)%Z.
rewrite <- Nat2Z.inj_succ.
exact H.
apply Zlt_succ_pred.
exact H0.
apply (Z.lt_trans (Z.of_nat n) (Z.of_nat (S n)) k).
rewrite Nat2Z.inj_succ.
exact (Z.lt_succ_diag_r (Z.of_nat n)).
exact H.
Qed.

これを見て、証明がどのように進んだのかわかりますか？おそらく、実際にRocqを動かさないと証明の内容がわからない人が大半なのではないかと思います。

「テキストファイルに記述されるのが、tacticの羅列という人間可読性の低いデータで良いのか？」というのが私の問題意識の一つです。

証明を書く時はRocqの支援があるので、人間から証明支援系にtacticで指示を出すという形で良いのでしょう。そして、「正しさを検証できる証明」という意味ではtacticの羅列は十分に役割を果たしているのでしょう。でも、証明を書き下すことの意義はそれだけでしょうか？いくつかの観点から考えてみます。

【観点その1】証明が持つ情報というのは正しいかどうかのゼロイチではなく、アイディア等を読み取るために読むという場合もあると思います。そういう場合に無味乾燥なtacticの羅列だけだと不便そうです。ただ、この点に関しては「自然言語によるコメント等で証明のスケッチを書いておく」という対処方法があります。

【観点その2】現代においては、証明を読む可能性がある主体は「定理証明支援系のような機械」と「人間」の2択ではありません。LLMのような機械が証明を「学習」に使いたいかもしれません。そのとき、tacticの羅列は学習データとして有益なのでしょうか？もちろん、必要に応じて「定理証明支援系によって文脈をアノテーションした証明」を学習データとして使えば済む話ですが、それなら「アノテーションした証明」を人間にも見せてくれよ、と思ってしまいます。

【観点その3】私はWeb記事「週刊 代数的実数を作る」・同人誌「代数的数を作る」のように、「数学をプログラムで実装したものをWeb記事や同人誌にする」というようなことをしています。Web記事も同人誌も、第一義的には人間が読むためのものです。そういう場に、tacticの羅列を載せることは適切でしょうか？適切ではないというのなら、紙面には何を載せるべきでしょうか？

一つのやり方は、「証明の（自然言語による）スケッチだけを紙面に載せて、完全な（形式化された）証明はGitHubからダウンロードしてもらう」という形になるでしょう。実際に、私が持っている本の中では「Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System」はそんな感じです（実際の証明はFlocqというパッケージにあります）。

しかし、私の個人的意見かもしれませんが、「この本の内容は完全ではないのでオンラインで別途補足資料を入手してください」というのは読者に手間をかけさせる「甘え」であり、可能なら避ける方策を考えるべきだと思います。この思いから、私の直近の同人誌「作ってわかるTeX言語」では紙面に全てのソースコードを載せるようにしました。

長々と書きましたが、形式的証明と「紙面に載せられる」という性質は両立しないのか？ということです。【観点その3終わり】

tacticを使うのは「proof termをそのまま書くと冗長になりすぎるから」「高度な自動化機能を使いたいから」あたりが理由なのかなあと推測していますが、それにしたってもうちょい人間可読性のある見せ方（普通のプログラムに対するJupyter NotebookやDoxygenのような）があるといいんじゃないかなあと素人として思います。

観点その3については、紙媒体やPDFを諦めて、私が4年前に作ったような「動画」、あるいはWebでのインタラクティブな形式に注力するという手もあるかもしれません。

もちろん、世の中の定理証明支援系はRocqだけではなく、違った証明の書き方ができるものもあります。Agda, Mizar, Isabelle/Isarあたりは見る価値がありそうだと思っています。

証明の可搬性

世の中の定理証明支援系は、それぞれ異なる基礎に基づいていたりします。RocqとLeanはどちらも型理論ベースですが、型の宇宙の階層のやり方が違う、みたいな話をどこかで見ました。型理論ベースじゃない定理証明支援系のことはよく知りません。

何が問題かというと、基礎が異なると「あるシステム向けに書いた証明を別のシステム向けに機械的に翻訳する」ということが難しくなるのではないか、ということを懸念しています。証明の可搬性（ポータビリティー）の問題です。

まあ、「こいつは一流の定理証明支援系になれると信じているから、必要な定理は全部俺が証明してやる」という気概があれば証明の移植が機械的にできなくても問題ないのかもしれません。しかし、そういう気概のあるユーザーが都合よく現れるとは限らないので、一般論としてユーザーの少ない新興システムが不利になりそうです。

私はプログラミング言語を作る（あるいはその妄想をする）のが好きなので、「プログラムの性質を証明できる新言語（特に、システムプログラミング言語）を作れないか」と考えることがあります。その場合、定理証明に必要な全ての道具（型理論ベースだったらtermination checker、宇宙の階層、定理の検索システムなど）をすべて自前で揃え、その上で必要な定理も証明するのは大変そうです。できれば、RocqやLeanなどの既存の定理証明支援系を利用したいところです。そのように言語を跨いで定理を利用するのはどの程度可能なのでしょうか？

普通のプログラミングだったら、FFI (foreign function interface) という仕組みで既存の言語で書かれた実装を移植せずに別の言語から利用することができます。なので、新しく作った言語で書かれた資産が少なくても、新言語である程度のアプリケーションを作ることができます。つまり、Foreign Function Interfaceならぬ、Foreign Proof Interfaceはできないのでしょうか？（まあ、FFIだって型システムの高度な機能を別言語に持ち越すことは多くの場合できないのですが。）

一つの答えは、「既存の定理証明支援系の型システムと互換性があるようにターゲット言語の型システムを設計する」ということでしょう。Dependent Haskellの動機の一つが、Agdaのプログラムを持ってくること、みたいな話をどこかで読んだ気がします。

ChatGPTにも聞いてみたら、次のような答えが返ってきました：

（略）

🔄 移植や相互運用の試み

✅ 中間表現・共通言語の提案

  • Dedukti: 複数の証明系のカーネルを翻訳して検証できる中間言語（λΠ-calculus modulo rewriting）。
    • Coq・HOL・F*・Leanの一部から変換可能。
  • Logipedia: Deduktiを活用し、複数の証明系を横断するリファレンスライブラリを構築中。
  • OpenTheory: HOLファミリー間の証明共有のための中間フォーマット。

（略）

（質問文：「定理証明支援系はRocq（旧Coq）やLean、Agda、Isabelleなど多数ありますが、一つの証明支援系で書いた証明を他の定理証明支援系で利用することはできますか？」）

これらは実在するプロジェクトのようです。なので、「証明の相互運用」というアイディア自体はすでにあるということになります。

まあ、AIが進歩すれば形式的な証明の間の翻訳を自動でやってくれる、みたいな未来はありそうです。何もないところから証明を捻出するよりは簡単なはずです。

これから見てみるべきもの

問題意識があった時にやるべきことは、先行事例の調査です。

証明の可読性という観点から、以下のことを試すべきかもしれません：

  • Agda, Mizar, Isabelle/Isarなどに入門する
  • RocqやLeanで、tacticをなるべく使わない書き方を試してみる

証明の可搬性、新言語（特に、システムプログラミング言語）での利用を考えると、以下を見てみるべきかもしれません：

  • Dedukti, OpenTheory等を見てみる
  • F* (F star) 界隈のLow*などを見てみる

まあ私にはやりたいことがたくさんあるので、定理証明支援系に対してどの程度時間を割けるのかは分かりませんが……。

Spread the love