このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

近未来の証明ソフトウェアは‥‥

雑記／備忘

twitterで昔の論文に言及したのですが、出版年をえらく間違えてました → https://twitter.com/m_hiyama/status/1635154485101359104 「53年前」と言ってますが、実際は27年前でした。

上記URLのページが以下のようだったので、1970年の論文かと勘違いしました。ごめんなさい。



それはともかく、昔の論文を眺めて何を感じたかを記します。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\calc}{\Keyword{calc } }
\newcommand{\endcalc}{\Keyword{end } }
\newcommand{\theorem}{\Keyword{theorem } }
`$
内容：

グランディ／センタのサンプル

冒頭に挙げたグランディ／センタ*1*2の論文では、構造化運算的証明〈structured calculational proof〉と呼ばれる半形式的証明記述フォーマットを提案しています。「半形式的フォーマット」とは、完全に形式的（機械可読）ではないけど、人間にとっては十分に明確であり、機械可読形式への翻訳も容易だろうと期待できるフォーマットのことです。

グランディ／センタのサンプルを、わずかに構文を変えて引用します。

$`\theorem \text{sample } (k : \mrm{Nat}) : \mrm{even}\; ( k^3 + k) :=\\
\calc \\
\mrm{even} ( k^3 + k)\\
\updownarrow //\text{ Extract the common factor.}\\
\mrm{even} (k\cdot (k^2 + 1) ) \\
\updownarrow //\text{ Distribute even over }\cdot \text{ .}\\
\mrm{even}(k) \lor \mrm{even}(k^2 + 1) \\
\updownarrow //\text{ Simplify the right disjunct.}\\
\quad \calc \\
\quad \lnot \mrm{even}(k^2 + 1)\\
\quad \updownarrow //\text{ Since }\mrm{even}(i + 1) \text{ is }\lnot \mrm{even}(i)\\
\quad \lnot \mrm{even}(k^2 )\\
\quad \updownarrow //\text{ The defiition of square}\\
\quad \lnot \mrm{even}(k \cdot k )\\
\quad \updownarrow //\text{ Distribute }\mrm{even} \text{ over }\cdot \text{ .}\\
\quad \lnot (\mrm{even}(k)\lor \mrm{even}(k))\\
\quad \updownarrow //\text{ Disjunction is idempotent.}\\
\quad \lnot \mrm{even}(k)\\
\quad \endcalc\\
\mrm{even}(k) \lor \lnot\mrm{even}(k)\\
\updownarrow //\text{ The law of the excluded middle.}\\
\top\\
\endcalc`$

見やすいようにキーワードは緑色にしています。$`\calc \endcalc`$ のあいだに運算的証明〈calculational proof〉を書いています。運算的証明を入れ子にもできます。運算的証明とは、1行に1つの命題を書いていくスタイルの証明です。上の行から下の行が導けるときは行間に下矢印 $`\downarrow`$ 、下の行から上の行が導けるときは行間に上矢印 $`\uparrow`$ 、両方向に互いに導ける（つまり同値）なときは行間に上下矢印 $`\updownarrow`$ を書くことにします。

行間の矢印記号の右脇はコメントです。コメントは自然言語で書いてあります。現在の証明ソフトウェアは自然言語を解釈できないので、人間対人間のコミュニケーションにしか使えません。自然言語を理解可能な人間にとっては、コメント付きの運算的証明は十分に明確であり、分かりやすいフォーマットだと思います。

上記疑似コードの最初の2行だけは、現状の証明ソフトウェアであるLean 4でそのまま入力できます。

theorem sample (k:Nat) : even (k^3 + k) := 
calc

Lean 4も運算的証明をサポートしていて、それはcalcキーワードで始まります*3。しかし、Lean 4は自然言語のコメントをまったく理解できないので、最初の2行以降はエラーになります。

何の制約もない自然言語では困りますが、統制された英語〈controlled english〉のコメントくらいなら、ソフトウェアが解釈できてもよさそうなもんだ、と思いますよね。

楽観的な予測

僕がこのブログを初めてすぐの頃の記事「HOLをWindowsで動かす（とりあえずダメだった）」は、証明ソフトウェアであるHOLをソースからビルドしようとして四苦八苦している様を綴っています。その頃思っていたことは「数年で状況は改善されるであろう」でした。

ビルドやインストールに関しては実際に改善されて、今は昔のような苦労はありません。しかし、「改善されるであろう」には別な期待 -- 証明記述そのものも改善されて、人間にとって自然なスタイルで書けるようになるだろうと予測していました。

前節の論文の著者達 -- グランディとセンタも、自然言語を含むサンプルが、いずれは機械可読形式にコンパイル出来るようになると期待していたでしょう。「いずれ」をどの程度と予測していたかはわかりませんが。

楽観的な予測は外れましたが、2023年時点において、予測と現実にはどの程度のギャップがあるのでしょう？ 古参のIsablle, Coqと肩を並べる（贔屓目で言うと凌駕する）能力を持つ新鋭Lean 4（「プログラミング言語Lean 4の現状」参照）に、グランディとセンタのサンプルを理解させることを考えると、だいたいの感触は得られるでしょう。Lean 4が理解できない部分を人間が助けてあげるときの労力を計る、ということです。

その労力はねー、えっらい大変ですよ。

ワンステップだけ

グランディ／センタのサンプルは上から下にスルスルと読めますが、実はバックワード・リーズニングになっています。なので、下から上に読んでいって、（シーケントで書けば）$`\top \to \mrm{even}(k^3 + k)`$ という証明になります。行と行のあいだはすべて双方向証明があるので、逆向きにできるのです。上から下だと $`\mrm{even}(k^3 + k) \to \top`$ ですが、真（$`\top`$）はどんな前提からでも証明できるので無意味です。

証明の全体の流れは下から上ですが、各証明ステップのコメントは上から下を前提に書いています。まずは上の行から下の行に見て、その後で下の行から上の行もOKだな、と確認することになります。

証明の方向に関して、かなりイレギュラーな書き方をしているにも関わらず、人間は違和感を抱かないのは（抱く人もいるかも知れませんが）、普段、バックワード・リーズニングとフォワード・リーズニングをごちゃ混ぜに使っているからです。

さて、証明の最初のワンステップだけを見てみましょう。

$`\mrm{even} ( k^3 + k)\\
\updownarrow //\text{ Extract the common factor.}\\
\mrm{even} (k\cdot (k^2 + 1) )`$

述語evenは前もって定義しておくことにしましょう。例えば：

def even (k : Nat) := ∃(j : Nat), 2*j = k

英文 "Extract the common factor." を解釈すると、因数分解していると分かります。直接的には次の等式的定理が必要です。

$`(k : \mrm{Nat}) \vdash k^3 + k = k \cdot (k ^2 + 1)`$

ここで、$`\vdash`$ は証明可能性を意味する記号で、全体として証明可能性判断〈provability judgement〉になっています。この特殊な等式がライブラリにあるとは思えません。もっと一般的な定理でしょう。

$`(k, i, j : \mrm{Nat}) \vdash k\cdot i + k \cdot j = k \cdot (i + j)`$

自然数に関する定理ではなくて、半環〈semiring〉の分配法則としてライブラリに存在するかも知れません。あるいは、適切なライブラリをインストールしてないと、自分で補助定理として証明する必要があるかも知れません。

いずれにしても、"Extract the common factor." に使える定理を探すのが先決です。この定理検索が大変。定理／関数／型などの名前の文字列検索しか手段がない。ありていに言って“grep検索”ですよ。

Lean 3では、OpenAIのAPIを利用したlean-gptfという知的検索ツールがありました。

Lean 4にはポーティングされてませんが、いずれAI利用検索ツールは登場するでしょう。当座は、そもそもインターネット上に情報がないので学習不足であまり使えないかも知れませんが、将来には期待してます。

今々使える道具は、library_searchコマンドとhttps://leanprover-community.github.io/mathlib4_docs//サイト、あとはホントにgrepだけです。

述語 $`\mrm{even}`$ の引数内を等式で変形〈リライト〉するので、次の定理も必要です。

$`X : \mrm{Type}, (P: X \to \mrm{Prop}), (x, y: X), p: P(x), e: x = y \vdash P(y)`$

述語の引数を等値なモノで置き換えてもいいよ、という内容です。この定理（と同等なもの）も探して使えるようにします。

探してきた既存定理、または自分で準備した定理から $`k^3 + k = k \cdot (k ^2 + 1)`$ を導くフォワードまたはバックワード・リーズニングを書き足して、「述語の引数を等値なモノで置き換えてもいいよ」と組み合わせて $`\mrm{even} ( k^3 + k)`$ に適用して、やっと $`\mrm{even} (k\cdot (k^2 + 1) )`$ が得られます。

これで、まだワンステップだけです。

直接証明（実体はラムダ式）を書くよりタクティクを使ったほうが楽でしょうが、「「プログラミング ＝ 証明」のはずだが」で述べたように、タクティク証明は人間が読めません。

近未来の証明ソフトウェア

グランディ／センタのサンプルのような半形式的証明は、僕も目にしたことがありました。HOLのビルド・インストールに消耗していた2005年時点では、十年後の2015年くらいには「半形式的じゃなくて形式的証明」になるような気がしていたわけですが、そう、大外れ*4。

もう楽観的な気分にはなりにくいのですが、自然言語で対話できるAIが評判になっているご時世だし、「2年後にはグランディ／センタのサンプルをそのまま理解する証明ソフトウェアが実現する」と予測しておきましょう。まー、予測っつうより“願い”ですけど。

*1:Grundy の発音 https://www.youtube.com/watch?v=FiQuaVd2kgk

*2:Centre の発音 https://www.youtube.com/watch?v=4VqnPmxiAn0

*3:https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html 参照

*4:追記： 予測が外れたのは、僕が「人間が文脈を考慮したり行間を読む行為を、コンピュータでシミュレートするのがどんだけ難しいか」実感がないというか、認識してなかったんですね。今でも実感はないけれど、どえらく難しいという事実は認識してます。