ChatGPT-xのような、チャット方式の対話型AIが世間を騒がしています。確かに、現代社会に大きなインパクトを与えそうです。僕も期待に胸を躍らせているのですが、だいぶニッチな方面への期待です。
今までとても困難だった“機械可読形式証明〈machine-readable formal proof〉を書くこと”が、かなり楽チンになる可能性があります。$`\newcommand{\Iff}{\Leftrightarrow}`$
内容：
シリーズ記事：
- チャットAIで形式証明も自然言語混じりで書ける（はず） （この記事）
- 自然言語証明から形式証明を抽出できる（はず）
- 自然言語ヒント／キュー前提の形式証明の書き方
- 証明支援系がダメだった理由と、AIでブーストする理由
- 自然言語前提の証明記述でも形式的枠組みは必要
- 自然言語混じり形式証明からの多方向翻訳
- 証明と計算は同じこと： 形式証明におけるノードとコネクター
- 自然言語混じり形式証明の意味論
- 自然言語混じり形式証明の意味論と最近の型理論
関連する過去記事：
- フォワード・リーズニングとバックワード・リーズニング
- 「プログラミング ＝ 証明」のはずだが
- 近未来の証明ソフトウェアは‥‥
- 近未来の証明ソフトウェアはこうなる（といいな）
- ヤシコフスキ／カリシュ／モンタギュー形式の証明： 人間可読・将来的機械可読
- ヤシコフスキ／カリシュ／モンタギュー形式をLean 4に手でトランスパイル
機械可読形式証明の現状
機械可読（ソフトウェアが解釈・処理できる）形式証明を書くことは知的な作業に思えます。実際、高度に知的な側面もあるにはあるのですが、時間と労力が矢鱈にかかり、たいして知的でもなくつらい作業がとても多いのです。
証明支援系〈proof assistant〉は人間を支援するソフトウェアのはずですが、実感としては、石頭で物分かりが悪いソフトウェアが証明を理解する支援を人間がしているようです。ソフトウェアは“証明支援される系”です。
人間が四苦八苦して機械に理解してもらうのは理不尽じゃねーか、と思ってしまうわけです。「証明検証系Mizarのジレンマと証明系の村」で、証明検証系Mizarについて、“地獄の使い勝手”と書いています。「フォワード・リーズニングとバックワード・リーズニング」では、現状の証明ソフトウェアが「使いものにならない」と評しています。僕の個人的経験にもとづくバイアスが入っているでしょうが、僕だけでもなく、証明ソフトウェア -- 特にそのタクティク証明の評判は芳しいものではありません。
- Title: A Tutorial Introduction to Structured Isar Proofs
- Author: Tobias Nipkow
- URL: https://courses.engr.illinois.edu/cs576/sp2015/doc/isar-overview.pdf
引用：（ブラケットは檜山が挿入）
a [tactic] proof is a more or less structured sequence of commands that manipulate an implicit proof state. Thus the proof text is only suitable for the machine; for a human, the proof only comes alive when he can see the state changes caused by the stepwise execution of the commands. Such proofs are like uncommented assembly language programs.
[タクティクによる]証明は、暗黙の証明状態を操作する若干構造化された一連のコマンド並びです。したがって、証明テキストは機械にだけ適したものです。人間にとっては、コマンドのステップごとの実行によって引き起こされる状態遷移を目視で確認できる環境においてのみ、証明が理解可能です。このような証明は、コメントのないアセンブリ言語プログラムのようなものです。
- Title: Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
(ICLR 2023 conference paper) - Authors: Albert Q. Jiang 他
- URL: https://arxiv.org/pdf/2210.12283.pdf
引用：
Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts.
証明自動化と証明支援系に関する何十年にもわたる研究にもかかわらず、形式証明を書くことは依然としてつらく困難であり、少数の専門家しかアクセスできません。
機械可読形式証明を書くには、専門的知識・技量だけでなく、苦役に耐える忍耐力と根性が要求されます。ありていに言って、機械〈ソフトウェア〉がバカ過ぎるからです*1。
自然言語での対話をサポートするチャットAIの技術は、証明ソフトウェアを賢くする可能性があります。「こんなこと、人間がやることじゃねーよ」という苦役から開放されるかも知れません。
形式証明の事例
ソフトウェアが自然言語を理解できるとしても、証明を100%自然言語で記述するのは得策ではありません。それだと、人間にとっても不明瞭で分かりにくいものになってしまいます。全体の構造や流れは、人工的なキーワードを使って明示したほうがいいでしょう。ここでは、人工的なキーワードは緑色で表示します。
以下で使う、僕が想定している人間可読・将来的機械可読なフォーマットについては、「ヤシコフスキ／カリシュ／モンタギュー形式の証明： 人間可読・将来的機械可読」に書いています。
例題を説明します； 自然数の大小順序を足し算で言い換えると、
$`\quad n \le m \Iff \exists k \in {\bf N}. n + k = m`$
この足し算による定義にもとづいて、大小順序の推移律を証明します。
入れ子のブロック構造はインデントするほうが見やすいでしょうが、ブロックのbegin/endはキーワードからも判断できるので、律儀にインデントはしてません。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\for}{\Keyword{for } }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\consider}{\Keyword{consider } }
\newcommand{\st}{\Keyword{ st } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\Imp}{ \Rightarrow }`$
$`\for a, b, c \in {\bf N}\\
\letsShow \exists z\in {\bf N}. a + z = b,\; \exists z\in {\bf N}. b + z = c \to\\
\quad \exists z\in {\bf N}. a + z = c\\
\downarrow \text{仮定を再掲}\\
\exists z\in {\bf N}. a + z = b,\; \exists z\in {\bf N}. b + z = c\\
\bullet \text{この2つの存在命題について考えよう}\\
\consider x\in {\bf N} \st a + x = b,\; y \in {\bf N} \st b + y = c\\
\quad \downarrow \text{上の条件の等式から}\\
\quad a + (x + y) = c\\
\quad \downarrow \text{上の } x + y \text{ を } z \text{ として存在限量子で束縛する}\\
\quad \exists z \in {\bf N}. a + z = c\\
\endBlock\\
\bullet \text{以上により}\\
\conclude \exists z\in {\bf N}. a + z = b,\; \exists z\in {\bf N}. b + z = c \to\\
\quad \exists z\in {\bf N}. a + z = c
`$
自然言語（日本語）ヒント部分以外について補足説明します。
- $`\for`$で証明で使用してよい自由変数の型宣言をします。
- $`\letsShow`$ で証明すべきステートメント〈シーケント〉を提示します。この段階で証明要求〈証明責務〉が発生します。
- $`\letsShow`$ ブロックの終了は $`\conclude`$で示します。冗長ですが、$`\conclude`$で証明が済んだ（証明責務が果たされた）ステートメントを再確認しています。人間にとっては、このような冗長性もときに必要です。
- 存在命題が出現したら、$`\consider`$ブロック内で処理します。存在命題で存在が保証された自然数を $`x, y`$ という文字で表します。ただし、$`x, y`$ には条件が付くので $`\st \text{(such that)}`$ で条件を書いています。
自然言語ヒント／自然言語キュー
証明に含まれる日本語の部分は、コメントではなくて機械可読証明の正式な一部と考えます。人間に対しては、日本語の文言が理解を促す注釈になります。機械〈ソフトウェア〉もこの日本語を理解可能だと想定します。日本語はソフトウェアへの指令の意味合いもあるので、自然言語キュー（cue in natural language）とも呼べるでしょう。
下矢印 $`\downarrow`$ または黒丸 $`\bullet`$ に続けて自然言語ヒント／キューを書いています。
- 次の行の命題が正当である根拠〈justification〉を下矢印に続けて書く。
- 証明の方針〈strategy〉や、証明のマクロ構造については黒丸に続けて書く。
ただし、$`\downarrow`$ と $`\bullet`$ の厳密な使い分けルールがなくても、ソフトウェアが“よしなに解釈してくれる”ことを期待しています。
日本語ヒント／キューでは、曖昧な指示語が多用されています。
- この2つの存在命題
- 上の条件の等式
- 以上により
今までの証明ソフトウェアは、このような指示語が使えないので、参照される場所に番号やラベルをふる必要がありました。番号・ラベルをふったほうが明確なときもありますが、「すぐ上の」とか「先に示した」とかは、「それくらい分かれよ！」という気分になります。参照・言及の指示語を理解してくれれば、けっこうありがたいです。
$`\consider`$ブロックは、自然演繹の存在除去規則に従った証明です。そのことを「存在命題について考えよう」と「以上により」で済ませています。この証明パターンは定番なので、この程度のヒントがあれば賢い証明ソフトウェアには十分だと思います。
しかし、今までの証明ソフトウェアは、かなり詳細に使用した推論規則を指定して、決まった記述構文を守る必要があります。
$`\consider`$ブロック内の「上の条件の等式から」の部分を切り出すと次のようになります。
$`\for a, b, c\in {\bf N}\\
\for x, y\in {\bf N}\\
\letsShow a + x = b,\; b + y = c \to a + (x + y) = c\\
\quad \cdots\\
\conclude
`$
$`\cdots`$ の部分の証明は律儀に書くべきでしょうか？ 書かなくても分かるし、$`\text{by auto}`$ のようなコマンドも不要でしょう。「上の条件の等式から」の一言で片付けたいところです。
とんでもなく大変なライブラリ検索
最古参の証明ソフトウェアであるMizarは、証明記述の人間可読性に関しては今でもダントツの一番です。証明本体は読み書きしやすいのですが、インポート宣言に相当する環境〈environ〉部がないと検証〈コンパイル〉できません。環境部には、定理証明で使っている他の定理への参照が入るのですが、「使っている他の定理」を探すのが極めて困難です（「証明検証系Mizarのジレンマと証明系の村」参照）。
初心者が環境部を書くのはまず無理なので、ベテランに書いてもらいます。近くにベテランがいなかったら？ ほとんどの人は諦めて、ごく少数の根性と熱意のある人がMizarユーザーになるのでしょう。
各証明ソフトウェアとも、ライブラリ検索のコマンドやWebサイトを準備はしています。
- Mizar ： http://mmlquery.mizar.org/mmlquery/three.html
- Isabelle ：https://behemoth.cl.cam.ac.uk/search/
- Lean 4 ： https://leanprover-community.github.io/mathlib4_docs//
検索ツールがあるとは言いながら、ソースコード内を文字列検索する原始的方式なので、意図している目的の定理にたどり着くのは容易ではありません。
最も有効で手っ取り早い検索手段は、よく知っている人に聞くことです。チャットAIは「よく知っている人」の代理になると期待できます。ライブラリそのものに出現するワードやフレーズだけではなくて、連想される自然言語などとの関連性も含めてよく知っている人（の代理）が助けてくれるなら、形式証明を書くことは格段に楽になるでしょう。
既存の定理／公理／定義／推論規則などのライブラリにおける正確な綴りを知らなくても、「モノイドの結合律から」「中間値の定理を使えば」「数学的帰納法により」「随伴関手対はモナドを定義するので」のような自然言語ヒント／キューで済むなら、つらくてバカバカしい検索作業から開放されます。
「いずれは改善されるだろう」とずっと待っていたのですが、証明ソフトウェアの使い勝手が良くなる気配がなく、「結局無理なのか」という諦念をいだいていました。が、今度こそ、今度こそ、今度こそ、自然言語ヒント／キューにより使い勝手が良くなると期待してます。
*1:証明ソフトウェアが、最優秀な人材を揃えた開発チームが30年、40年に渡って継続した膨大な努力の結晶であることは承知しています。しかし、技量も根性もない一ユーザーの無責任な感想を言わせてもらえば「バカ過ぎる」なんです。
