擬似ランダムとネクストビット予測不可能性の同値性の証明をLean4で形式化する過程で色々と困難もありました。それらについてClaude DesktopやGoogle AI Studioなどの生成AIと議論してきた結果、１つのライブラリ（定理集）とその使い方文書を作成し、それらもGithubで公開しました。
今回はそのライブラリと使い方文書の話をしたいと思います。ライブラリの名称はBVCryptGameLib.leanです。BitVecで鍵、平文、暗号文を表す共通鍵暗号のためのライブラリです。BitVecの上の一様分布やPMFのdo文による確率ゲーム（いくつかの確率試行から確率事象を定義してその確率を表す）が簡単に扱えます。またハイブリッド論法に特化して一様分布やそれを支えるBitVecの３分割やその結合を明示的な定理として提供しています。
ライブラリの構成
４つのレイヤーから構成されています。第１レイヤーはBitVecに関する諸定理で、特に分割や連結に関する同型についての定理を集めました。BitVecはビット列なのでその分割や連結は++, extractLsb'のような形で明示的に切ったり貼ったりができます。ただそれをやると前の記事で述べた通りビット演算の嵐になったり依存型のキャストの嵐になり、Lean4の中の既存の道具(simpのついた簡略化命題やomegaによる証明)との相性が悪くなります。本来自動証明できるような命題を手で証明したりと大変な思いをします。その部分を吸収するのがこの層です。
第２レイヤーはPMFによる確率計算の層です。ここではPMFの証明でtsumに落とさないとできないものを補助定理として提供します。
第３レイヤーは一様分布U nのレイヤーです。第１レイヤーのBitVecの定理を一様分布に持ち上げたものが提供されています。
第４レイヤーは確率ゲームの変形レイヤーです。以前にみたbind_unusedで不要な確率試行を削除したり、bindがPMF.bindに由来するために使えなくなる多くのbind関連補題の代わりの命題が提供されています。
ライブラリの活用
tsumにまで展開されていた多くの証明をこのライブを使って書き直すことで非常にシンプルにすることができています。確率計算も第２レイヤーと第４レイヤーを活用すると確率ゲームの変形の形で人間として分かりやすく証明を進めることができました。この方針による証明は生成AIからも評判は良かったです。以前の記事で紹介した以下のような証明はその一例です。
theorem Pr_comparison_uniform_bit (AnyDist : PMF Bool) :
Pr (do let a ← AnyDist
let b ← PMF.uniformOfFintype Bool
PMF.pure (a == b)) = 1/2 := by
calc
Pr (do let a ← AnyDist;
let x_bit ← PMF.uniformOfFintype Bool;
PMF.pure (a == x_bit))
_ = Pr (do let a ← AnyDist; PMF.uniformOfFintype Bool) := by
congr 1; congr 1; funext a
change (PMF.uniformOfFintype Bool).map (bool_beq_equiv a) = _
rw [U_map_equiv]
-- The sampled `a` is now unused, so it can be dropped.
_ = Pr (PMF.uniformOfFintype Bool) := by rw [bind_unused]
_ = 1 / 2 := by simp [Pr, PMF.uniformOfFintype_apply]
一方ライブラリや便利な補助定理を作ってファイルにまとめただけでは人間も使うのを忘れるし、生成AIもそれらを使うきっかけがないことがありました。特に生成AIはライブラリの中身を分かってくれていれば数行で済むかも、というような場面でも、目の前の式をどう展開して証明するか、に突き進んでしまうことが多かったです。一つの証明が完結するとよくAIと振り返りをするのですが、その際に聞いてみると「その方が証明終了に行きつける確実な道だと考えた」という返答が多かったです。実際にはビット演算の証明や依存型の計算で苦労する局面が確かに多々ありました。
使い方規範文書
そのような議論をしていて、「今の議論は重要だからまとめてみて」とお願いしたのが発端となり生まれたのがBVCryptGameLib.mdというライブラリ活用のための文書です。この文書ではなぜ４つのレイヤーのAPIが整備されているのか、どう使うのか、依存型やビット演算やtsumを避けるためにこのライブラリをどう活用できるか、が書かれています。また生成AI自身がうまく証明できなかったケースを分析してどうすれば証明できるかを書いてくれています。
その中でAI自身からの意見で加えた文を１つ紹介しましょう。
AI は目の前に提示された問題をそのまま解こうとする傾向が強く、「この問題設定自体を疑い、より抽象度の高い定式化に乗り換える」という判断は、放っておいて自然に出てくるものではない。
実際に `BitVec (n+m+k) ≃ BitVec n × BitVec m × BitVec k` を `++` ベースで定式化して証明を依頼したところ、AI は `right_inv` の場合分けで長時間行き詰まった。ここで「この命題はビットパターンの中身に一切触れていない、構造だけの主張のはずだから、同型の合成だけで示せないか考え直してほしい」と明示的に伝えたところ、`trans` を用いた5行の証明にたどり着いた。
この一押しは、AI モデルの性能が上がっても本質的には不要にはならないと考えられる。モデルが賢くなるほど「目の前の問題を力業で解き切る」持久力は上がるが、「そもそもの定式化を疑う」判断軸は、これとは独立に人間側が明示的に促す必要がある可能性が高い。したがって、本ドキュメントのような「どのレベルで考えるべきか」を言語化した指示書は、モデルの世代が変わっても、その都度形を変えて必要とされ続けると考えられる。
AIの能力が上がると方針変更能力や事前に多くの方針を検討するなどの振る舞いも出てくるかもしれません。それでも大きな方針変更やある方針を諦めるなどの高度な振る舞いは人間の方から示唆することでAI側の考慮事項になっていくこともあると思います。
最後に、このような使い方規範文書は、これからライブラリやフレームワーク、公開APIを作る場合の重要なドキュメントになっていくと思います。AIがコーディングする際にそれらを知らずに自分の知識だけで車輪の再発明もしながら作業することを防ぐためには、このような使い方規範文書が有効だろうと思います。
