証明付きバイブコーディングで証明支援系を作った

この記事は株式会社proof ninjaの助成を受けて書いています．

TL;DR

• Codexバイブコーディングで証明支援系を作った．

• その際，論理のコアの部分はRocq(旧Coq)で実装させ，「この自作証明支援系で証明可能な命題はRocqでも証明可能」をRocqで示し，OCamlにextractした．

はじめに

Codexに証明支援系 ZFCert を作らせてみました．Web上のチュートリアルもちょっとだけ作りました．
VS Code や Emacs でも動かせます．コードはこちら．

(なお，この文章は人の手で書いています．)

どんな証明支援系か？

一階述語論理の自然演繹ベースで，ZFC公理系が最初から公理として認められています．
証明はRocq風のタクティクで記述できます．

LLMが作った証明支援系，信用できるの？

LLMに作らせたとは言ってももちろん自分でコードをチェックしながら開発しました．
とくに，前述の通り論理のコアの部分はRocqで実装させ，

「ZFCert で証明可能 → Rocq でも証明可能」(健全性)

をRocqの定理として証明させました．(詳細は後で)

UIの部分などはRocqの証明は付けていないので，表示がおかしいなどのバグはあるかもしれません．

なんで作ったの？

「ただの趣味」は一つの答えですが，はじまりは「論理や集合の教育に使える証明支援系がほしいな」と思ったことです．
RocqやLeanは型理論ベースであり，「いわゆる普通の」一階述語論理，自然演繹，集合論からは異なる基礎付けとなっているので，教育上はその差がちょっとややこしいのです．
IsabelleやMizarでいいのかもしれないけど，私自身が詳しくないという問題がありました．それに加え，自分で1から設計してみたかったという思いもありました．
「既存の証明支援系を超える」のような意図は今のところありません．

中身について

Rocq 部分

Rocqの中で形式化した，論理のコア部分は以下のような設計になっています．

(1) FOL.v で論理のコア部分の定義・証明をしています．具体的には以下のようなことをしています．

• 論理式の型 formula の定義(de Bruijn indexを採用)
• formula から Prop への変換として意味論を定義
• 自然演繹による証明可能性を帰納的データ型 derives として定義
• derivesの健全性「derives の意味で A : formula が証明可能なら，変換後の Prop 型の命題がRocq の命題として真」を証明

健全性に関して，ある程度わかる人向けの詳細：
公理系の型 theory を theory := formula -> Prop とし，証明可能性を
derives : theory -> list formula -> formula -> Prop
として定義します．ここで，第二引数の list formula は仮定のリスト，第三引数の formula は結論です．
さらに，型パラメータ D に対して変数の付値の型を valuation D とし，関係記号の解釈の型を interp D とするとき，
inp : interp D, rho : valuation D の下で，任意の A : formula を Rocq の論理式として解釈できます．つまり，
satisfies : interp D -> valuation D -> formula -> Prop
が定義できます．
この上で公理系 T : theory が inp : interp D の下で valid であることを theory_valid T := forall A rho, T A -> satisfies inp rho A と定義されます．
このとき，以下の意味での derives の健全性

forall (T : theory)(A : formula),
    theory_valid T ->
    derives T [] A ->
    forall rho, satisfies inp rho A

が証明されています．

(2) 証明支援系を作る上では「タクティクを入力すると証明状態が更新される機構」がほしいです．
ProofState.vでは以下を実装しています．

• 証明状態の型 proof_state，タクティクの型 tactic．
• 証明状態の更新 step : tactic -> proof_state -> outcome proof_state (outcome はエラーハンドリングのためのResult型のようなもの)
• stepの健全性「step tac st = Success st' かつ st' が derives の意味で証明可能な証明状態ならば st も同様」であることの証明．

また，ここでの tactic は自然演繹の各規則を含んでいます．
「タクティク列によって A は証明可能 ↔ derives の意味で A は証明可能」であることを，TacticCompleteness.v で証明しています．

(2.5) 実際に証明支援系を使うとき，de Bruijn index表記では読みたくないので，変数名を使った論理式への変換(と健全性証明)を NamedProofState.v で行っています．

(3) ZFC公理は基本的には一つ一つ formula として定義していますが，分出公理と置換公理は公理図式(一つの公理ではなく，公理の族)であるため，formula 型の値としては定義できません．
そのためにそれらはタクティク separation, replacement として実装します．NamedCommands.v にこれらの定義と，健全性を証明があります．

(4) CertifiedSession.vでは，証明の履歴(certificate)を管理しています．
タクティク列により証明が完了した後，qed. コマンドで証明を終わらせるのですが，この際，証明の履歴をチェックし，履歴上の証明が本当に正しい証明になっていることをダブルチェックします．
これは本来は必要ないステップです．しかし，

• もしOCamlプログラムで途中の証明状態が改竄されたとしても qed. 時に弾けること
• certificateが，ユーザーにもチェック可能な witness としての役割を果たすこと(Rocqなどでいうproof termの代わり)
  などの利点があります．

(5) GlobalEnvironment.v で，グローバル定数記号の追加，管理を行います．
これは素朴な自然演繹を超える枠組みなのですが，次のような利点があります．
たとえば，空集合を扱いたいとき，本来は空集合の公理 exists e, forall x, not (x in e) から∃-除去で e を取ってくるのですが，空集合を扱う度にこれを行うのは少し面倒です．
そのため，代わりに empty という定数記号と forall x, not (x in empty) という定理をグローバルに追加すれば，空集合は empty という名前で参照できるようにします．
この仕組みにも健全性の証明があったほうがよいのですが，まだやっていません．

以上がRocqでコーディングした部分です．

OCaml 部分

Rocq で定義したタクティクや証明状態の更新を OCaml に extract し，それを用いて実際に動く証明支援系を OCaml で実装しています．

Codex に実装させる上で，「証明状態の更新はextractされたコードのみが行え，外側からは証明状態が変更できないようにすること」を徹底しました．
せっかくRocqで証明したプログラムも，extractした後に間違った使い方をしたら意味がありません．
そのため，証明状態の型 state やタクティクによる state の更新関数は mli ファイルで

type state

...

val rule_step :
  axioms:axiom list ->
  rule ->
  state ->
  (state, error) result

のように秘匿し，外部から state が変更できないようにしました．

また，Rocqで定義したのはプリミティブなタクティク(自然演繹の導出規則)のみなのですが，OCamlではより強力なタクティクを実装しました．
強力なタクティクはプリミティブなタクティク列に変換されるように実装されており，そのおかげでRocqで証明した健全性が壊れないようにしています．

UI

今のところ，Web, VS Code, Emacs で動きます．UI に関してはまだかなり色々改善の余地ありです．
WebインターフェースはOCamlプログラムをWasm/JavaScriptに変換して動かしています．
WebサイトのデザインもCodexに1から作らせたのですが，独特のLLM臭さ気持ち悪かったので多少自分で直しました．(まだ直し切れてませんが…)

自動証明タクティク

形式証明はとにかく手間がかかるので，自動化が欠かせません．
ZFCert では今のところ，導出原理に基いた自動証明タクティク resolution があります．Rocq の auto に似ていますが，ZFCert が排中律を仮定していることなどのおかげで Rocq の auto より ZFCert の resolution のほうが理論的には強いはずです．が，効率はまだよくありません．
また，resolution はスコーレム化を扱っていないため，量化子がネストした場合などにもまだ対応できていません．(それは Rocq の auto もそうですが．)

おわりに

ということで，バイブコーディングでできた証明支援系 ZFCert の紹介でした．
これまでバイブコーディングをあまりしてこなかった自分としては
「思ったより全然コーディング&証明してくれる！」
という感想もある反面，
「適切に指示を出せないと健全性とかを保証するのが大変だっただろうなぁ」
という気持ちもあります．
Codexが吐いた初期のバージョンではextractされたコードを適切に使ってるか分かりづらいプログラムだったため，そういった点は何度も指示を出したりしました．

あとは，思ったよりバイブコーディングは楽しかったです．
自分は，プログラムを勉強し始めたときは自分の手でのコーディングを楽しめていたのですが，残念ながら今やそういう感覚はなくコーディングは手段になってしまいました．
コードを書く(coding)こととは設計すること(programming)の一部なので，自分にとって手段である部分をLLMに任せられて，かつ設計は自分で考えられ，ちょうどいいところだけが残った感覚でした．

おわり．