なぜただ Lean を使わないのか

 (lawrencecpaulson.github.io)
1 ポイント 投稿者 GN⁺ 1 일 전 | 1件のコメント | WhatsAppで共有
  • 数学の形式化の歴史は Lean から始まったわけではなく、ほぼ60年前から複数の系統のシステムが中核的な手法と成果をすでに蓄積してきた
  • 1968年の AUTOMATH、LCF 系、HOL、Rocq、ACL2、Mizar といったツールは、実解析から素数定理、四色定理、ケプラー予想に至るまで幅広い形式化を実現してきた
  • Lean は大規模ライブラリと活発なコミュニティを土台に現代数学の定義を素早く積み上げてきたが、propositions as types や依存型が proof assistant の唯一の道というわけではない
  • Isabelle は 強力な自動化、高い可読性、依存型の回避を長所として掲げ、proof object なしでもカーネルの抽象化バリアによって証明検査を構成する LCF の伝統を受け継いでいる
  • AI が構造化された証明を整理し、別のシステムへ 翻訳する流れまで加わることで、ひとつのツールだけを絶対的な基準として見る負担は今後さらに小さくなりうる

初期システムと別系統

  • AUTOMATH

    • AUTOMATH は1968年の時点ですでに数学の形式化に必要な要素の大半を備えていた
    • 1977年、Jutting は AUTOMATH で Landau の Foundations of Analysis を形式化し、純粋論理から出発して 複素数の構成 まで扱った
    • 同値類 と有理数集合を用い、実数直線の デデキント完備性 も形式的に証明した
    • この成果は20年にわたり再現されず、1990年代半ばになってようやく John Harrison の HOL Light と Jacques Fleuriot の Isabelle/HOL で再び実数の形式化が行われた
    • 記法は非常に扱いにくく、自動化もまったくなかったため、証明は長く読みにくかった
    • それでも同値類の扱いでは Rocq より優れているとし、Rocq ユーザーが経験する setoid hell とは異なり、Jutting は同値類の形式化を落ち着いて進めた

  • Boyer と Moore

LCF 以後の流れ

  • Edinburgh LCF はプログラミング言語理論に集中していたが、証明支援系の メタ言語として関数型言語 を置くという発想は広く普及した
  • Cambridge、INRIA、Cornell など複数のグループが ML を用いて初期 HOL、Coq（現 Rocq）、Nuprl のようなツールを作った
  • HOL グループはハードウェア検証に注力していたが、浮動小数点ハードウェアの検証のために 実解析 が必要になった
  • John Harrison はコーシーの積分公式を通じて 素数定理 のような本格的な数学的結果を HOL 系で証明した
  • 100 theorems を可能な限り多く検証するという目標のもと、HOL Light はしばしば最上位に位置していた
  • 2014年までに、この系統のシステムは多くの高度な定理を形式化していた
  • これらの定理は概して証明が長く複雑で、形式化作業もきわめて大規模であり、定理に残っていた疑問を減らすうえで重要な役割を果たした

Lean コミュニティの台頭

  • 数学者たちは、先行する形式化の成果では Grothendieck schemes や perfectoid spaces のような主流の現代数学における精緻な構成までは扱えていないと見ていた
  • Tom Hales はこうした定義をライブラリとして積み上げる方向を選び、証明よりも 定義の蓄積 に重点を置いて Lean を選択した
  • 彼は Big Proof プログラムでこの方向性を発表し、類似の構想もあわせて議論された
  • Kevin Buzzard がこれを聞いて教育に Lean を使ってみることにし、その後の拡大が加速した
  • Lean コミュニティの重要な転換点として、Rocq を長く支配していた 構成的証明への執着 から離れたことが挙げられている
  • 直観主義 は Russell のパラドックス以後に現れ、実数概念にも特定の含意を持っていた
  • Martin-Löf type theory は明らかに直観主義的形式主義だが、Rocq はそれほど単純には捉えられないと述べている
  • それでも Rocq 関連の論文では、構成的証明が無関係または無意味な場面でも繰り返し現れ、この傾向が Rocq の数学への応用を妨げ、その立場を Lean に譲ることになったと見ている

propositions as types と LCF の違い

  • Propositions as types は論理記号 ∀, ∃, →, ∧, ∨ と型構成子 Π, Σ, →, ×, + を結びつける双対性である
  • この枠組みは美しく理論的にも生産的だが、唯一の道ではない
  • proof assistant を propositions as types の原理で証明を検査するソフトウェアに限定してしまうと、この半世紀の研究の大半が定義の外へ追いやられてしまう
  • そうなると Rocq、Lean、Agda だけが残る
  • AUTOMATH でさえ propositions as types の実例ではなく、Π や → に似た要素はあっても、論理は一般的な論理教科書のように 公理として設定 している
  • de Bruijn は50年前の時点ですでに 型と命題の分離 が必要だと見ていた
  • 代表例として除算は3つの引数を取る必要があり、(x/y) の値は (y \ne 0) の証明に依存するため、proof irrelevance が必要になると述べている
  • LCF のアプローチが propositions as types と同じだという認識 も事実とは異なると明言している
  • Rocq と Lean には命題の sort である Prop があり、ここでは同じ命題のすべての proof object が同じ値として評価されることで proof irrelevance が与えられる
  • だからといって巨大な proof object が消えるわけではなく、実際のシステムには依然として残っている
  • Robin Milner の中核的発見 は、LCF では proof object そのものが不要 だという点だった
  • ML の 抽象データ型 の中に証明カーネルを入れ、推論規則をコンストラクタとして置くことで、動的に証明を検査できる
  • ML の abstraction barrier によって不正は不可能だと見ている
  • 巨大な項が何も指し示していないのに数十MBを占めるようなことは、RAMmageddon の時代にはとりわけ不合理に映る
  • そうした不要な項をさらに優雅にする研究へ進んでいる点も批判している

Isabelle を選ぶ理由

  • 同僚が Lean を使っており、チームの専門性も Lean にあり、必要な前提ライブラリも Lean にあるなら、Lean を使うのが自然である
  • ただし自由に選べるなら、Isabelle を検討する理由は十分にある

  • 自動化

    • 長所として 最も強力な自動化 を挙げ、日常的な “hammer” たちと比べても sledgehammer に匹敵するものはないと評価している
    • 計算機代数の分野も別途扱う必要があると述べている

  • 可読性

    • 可読性の面で最良の選択肢 とし、Isar 関連の例 を根拠に挙げている

  • 依存型の回避

    • 依存型がないため、universe level や初学者を困らせるさまざまな癖を避けられる
    • Lean の mathlib や Rocq の SSReflect、Mathematical Components でも依存型の使用は推奨されていないと述べている
    • 依存型の核心的な難点は、まともに実装すると 型検査そのものが決定不能 になることだ
    • これは等価性判定が決定不能だからであり、初期にはこの点が当然のものとして受け入れられていたと述べている
    • 1990年ごろからは型検査を決定可能にするため、等価性を definitional/intensional equality へと弱める方向に合意が移っていった
    • その結果、(T(N+1)) と (T(1+N)) は互いに異なる型になる
    • この制約は実際の証明にも影響し、definitional equality の検査自体も依然として 計算負荷 が大きい

依存型なしでも可能な現代数学

  • 2017年時点では、Isabelle がどこまでの数学を扱えるかについて、はるかに慎重に見ていたと述べている
  • 当時は、次のようなテーマを扱うには依存型がどうしても必要に見えがちだった
  • しかし Alexandria 関連研究 を通じて多くを学び、核心は あらゆるものを型へ押し込まないこと だとまとめている

今後の方向性と AI

  • Lean は多くの点を正しく捉えており、入れ子の証明ブロック までサポートしているので、潜在的には十分に読みやすい証明言語になりうる
  • いま必要なのは Lean コミュニティがそうした機能を実際に活用することであり、Isabelle ユーザーはすでに概ねそうしていると述べている
  • コンピュータが検査できる proof object よりも、人間が実際に読める 証明テキストの透明性 のほうが重要である
  • AI の台頭はこの違いをさらに際立たせる
  • AI が作った証明は散らかっていることが多いが、sledgehammer で整理しやすく、構造がしっかりしていれば細部が過剰でも読める
  • そうすれば進行の流れを把握しやすくなり、より単純な形へ縮約することも容易になる
  • 最近では言語モデルが直接 sledgehammer を呼び出す 研究 も現れている
  • AI は読みやすい構造化証明を、ある proof assistant から別の proof assistant へ 翻訳 することも容易にこなせる
  • そうなれば、どのシステムを選ぶかという負担そのものが小さくなる

Mizar の欠落を補う

  • 数学の形式化の歴史は Mizar とその膨大な 数学ライブラリ なしには完結しない
  • Isabelle の Isar 言語 も Mizar から多くの影響を受けている
  • Mizar を落としていた点を別途訂正し、次の記事で Mizar を扱う予定だと述べている

関連記事

1件のコメント

 
GN⁺ 1 일 전
Hacker Newsの意見

  • HN読者の大半は数学者よりプログラマに近いので、数学的証明よりプログラミングの観点からLeanを見るほうが実用的だと思う
    関数型プログラミングの視点でLeanを扱う本として https://leanprover.github.io/functional_programming_in_lean/ はかなり良い
    私もLeanを学んでいる最中なので、初心者のバラ色の見方が少し入っているかもしれないが、最近のlean-zipの例のように、実際の圧縮・展開アルゴリズムのような普通のプログラマのコードを書いて証明することを目標にしている
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • この本を読みながら、Leanで基本的なコンピュータ代数簡約器を実際に触ってみた
      https://github.com/dharmatech/symbolism.lean
      C#コードを移植したもので、Leanの表現力は驚くほど高い
    • そういう用途ならDafnyも似た選択肢ではないかと思う
      以前に少し話題になっていたのを見たが、この分野は最近は詳しく追っていない
    • 1990年代にソフトウェア正当性証明を試した事例を覚えているが、最終的な証明注釈のほうで実際のソフトウェアより多くのバグが出ていた記憶がある
      そして障害がさらに二つあるように見える。第一に、ソフトウェアが何をすべきかを知ること自体が難しく、ユーザーがやりたいことと顧客が金を払うことが必ずしも同じではない
      第二に、多くの開発者の仕事の質があまりに低く、Javaのような言語より真理の言語をうまく扱えると期待しにくい
      ただし二つ目は、必要な注意を払うAIシステムに置き換えられることで消えるかもしれず、そうなれば状況は変わるかもしれない
    • 非関数型プログラミングはどうなのかと思う
      関数型プログラミングも、すでに見捨てられた数学と同じくらい、ほとんどのプログラマにとって大きな関係はないと思う

  • 筆者はLeanをかなり誤解しているようで、この分野をよく知る人に見えるだけに余計に意外だった
    Leanが証明オブジェクトをそのまま保持し、最終的にはすべての定義が展開された巨大な証明オブジェクト一つを検査すると見ているようだが、実際とはかなり違う
    Leanは、著者がLCFの利点として持ち上げていた最適化を、実質的にまったく同じ形で実装している。たとえるなら黒板を消しながら証明を進める方式に近い
    Lean4で def ではなく theorem として書くと、その証明オブジェクトはそれ以上使われず、これは単なる最適化ではなく言語の中核的性質だ。theoremはopaqueである
    証明項が残っていたとしても対話モードでユーザーに見せるためでしかなく、カーネルはその証明オブジェクトが何だったかを気にすることすらできない

    • これは実装というより概念的な違いに近い
      LCFでは証明と項は別物で、私としては本来そうあるべきだと思う。こうしたCurry-Howard的な混同は不要なのに、多くの人がそれがコンピュータで数学をする唯一の方法だと思っている
      望むならLCFでも証明を保存して活用できるし、Leanでも望むなら最適化で消せるだけだ
    • 依存型理論では証明オブジェクトは単にある型を満たす項そのものだが、だとするとLeanの実装は、そうした項を作らずに証明を構成できるという意味なのか気になる
    • その通りだと思う
      抽象型アプローチは多少メモリを節約するだろうが定数倍の差にすぎず、漸近的な改善ではない
      Leanが数十MBを無駄にしているという不満は1980〜90年代なら重要だっただろうが、今日ではそこまで決定的な利点ではないかもしれない

  • Leanが関数型プログラミングに向いているという話はよく聞くが、Agdaから来るとかなり無骨なダウングレードのように感じる
    tacticも良いとは言われるが、私の経験ではCoqのtacticのほうが強力で使いやすかった
    これも第一印象バイアスかもしれないが、今のところLeanの強みは何か一つを最高にこなすことではなく、全体的に無難でコミュニティが大きいことにあるように見える
    なぜ魅力的なのかは分かるが、その代償として美しさと力が少し失われている感じがして惜しくもある

    • 結局はネットワーク効果という話でもある
      ただ、こうした効果はその瞬間には永続的に見えても、実際には思ったほど長続きしない。本当にそれだけが重要ならPerlは今でもなお大物であるはずだ
      Leanでは特に大きなライブラリを先に確保した点が大きい。PerlにとってのCPANのようなものだ
      しかしスケーリング則を見ると、大半のユーザーにとって大きなライブラリの価値はサイズの対数程度にしか増えない可能性が高い
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      初期にはこの差は越えられないように見えるが、必ずしも規模を追い抜かなくても、ある時点からは使いやすさのほうが重要になる
      しかも数学ライブラリの移植はLLMに向いた作業でもある。ソースは検証済みで、ターゲットも検証可能で、推論経路もだいたい移せる
      逆に言えば、LLMのおかげで少数派プラットフォームで作業するハードルも予想より低くなる。向こうのライブラリを自分のプラットフォームに移せるなら、自分の証明も向こうへ移せる可能性が高い
    • むしろそれは、コミュニティがついに成熟して実際の仕事を始めたという意味に見える
      完璧な道具が重要なのではなく、十分に良い道具で仕事をやり遂げることのほうが大切だ
    • Agdaは証明チェッカーとしてはより良いが、ソフトウェアを作る実用的な選択肢ではないと思う
      Leanは本当にHaskellの後継になり得るほど、ソフトウェア開発向けの関数型言語として成長する余地があるように見える
    • Agdaは少し、Leanはそれより多く使ったが、数学の証明より一般的な関数型プログラムを書くのはLeanのほうがずっと簡単だった
      差は主にツール支援にあった気がする。Agdaの文書は乏しく、システムにインストールして動かすのも面倒で、事実上Emacsを使うことを強く要求してくる
      一方Leanは公式ドキュメントに cat ユーティリティの書き方まであり、全体としてずっとモダンなtooling体験を与えてくれる
    • Agdaの関数型プログラミングで具体的に何が良いのか気になる
      たいてい称賛されるのはdependent pattern matchingのあたりだが、その点ではLeanはかなり弱いと感じる
      それでも一般的なFPでもAgdaのほうが親しみやすいと感じるなら、どの点でそうなのか聞いてみたい

  • Isabelle/HOLは言語自体は悪くないが、ツーリングにはデスクトップ中心アプローチを離れても深い欠陥がある
    言語はLeanと違うが、必ずしも優れているわけではなく、依存型へのいくつかの批判には同意する
    結局のところ両言語は異なるトレードオフを選び、その選択がそれぞれの領域でかなり効率的な道具になることを可能にしたのだと思う。証明という領域自体が広く、パラダイムごとに強みと弱みが異なり、Leanはそのうち別の部分に特化しているだけだ
    Sledgehammerは良いが、Leanにも似たものが出てくるのは時間の問題のように思う
    探索段階では有用かもしれないがリソースを多く食い、証明を短くはするものの、公開されたコードでは半ば魔法のような by sledgehammer よりも証明の全ステップが直接見えるほうを好む
    一方でIsabelle自体を開発するのはLeanよりはるかに苦痛で、特に開発者たちとのやり取りがそうだ
    メーリングリストでバグはなく、予想外の挙動があるだけだというような態度は幼稚で非専門的に見えた
    そしてLeanのようなシステムのRAM使用量を皮肉るのも、Isabelle側のメモリ食いを見ればかなり滑稽な話だ

    • ここでの問題は、UNSAT証明書を高速に検査できる形にすることがまったく自明ではない点にある
      事実上それ自体が形式証明を書くのに近い難しさだ
    • 最後に確認したとき、Isabelle/HOLはカスタムEmacsモードをインターフェースとして使っていた記憶がある
      別のHOLと混同しているのかもしれない
    • Sledgehammerが何かは知らないが、説明だけを見るとMathlibの grind とほぼ同じ道具に聞こえる
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Leanで興味深いのは、Leanは言語なのに、人々が主に語っているのは実際にはMathlibというライブラリだという点だ
    Mathlibの制作者たちはかなり実用主義的に見え、そのためLeanの型の中に古典論理を入れ、直観主義論理は一部しか使っていないようだ

    • 排中律を説明するときに出した例は間違っている
      「あるものが同時に真であり偽であることはない」というのは排中律ではなく矛盾律だ
      排中律は p が真であるか、not p が真であることを意味する
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • コンピュータサイエンス側はすでに独自のCSLibを作り始めている
      https://www.cslib.io https://www.github.com/leanprover/cslib
      直観主義論理は本質的に計算可能な構成物へ数学的議論を変換しようとするところに意味があるので、この問題をどう扱うのか興味深い
      実際、Leanでアルゴリズムを書く時点ですでに何らかの形で構成的制約の中に入っており、その目的にはその程度の論理で十分なのかもしれない
    • 構成主義数学を受け入れる5段階というジョークを思い出す
      否認、怒り、取引、抑うつ、受容
      Andrej Bauerの関連講演や文章も参考になる
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • ここで言うべきなのは intuitive logic ではなく intuitionistic logic だ
    • そうした制約や行き詰まりが多いのに、いつ、なぜ直観主義論理を好むようになるのか気になる

  • こういう記事はもっと必要だと思う
    みんなが当然のようにとにかくXを使えと押しつける集団思考に対しても、少なくとも代替案を検討するだけの説得力ある理由はいつだってある
    結局代替案を捨てて主流を選ぶとしても、地形を知ったうえで選ぶほうがいいと思う

    • 完全には同意しない
      今でもフレームワークと代替案を作りすぎていて、おそらく面白いからなおさらそうなっている
      既存ツールを改善したり、ただ実際の仕事を進めたりする代わりに、言語やライブラリやビルドツールを延々と増やす方向に行くことが多い
      言語もライブラリもビルドツールも、今の半分しかなかったほうがむしろ良かったと思う
    • 結局はケースバイケース
      主流から外れるほど文書は減り、探索されていない隅のせいでバグは増え、助けてくれる人も少なくなる
      選択肢が20個以上積み上がったら、平均的には標準の選択肢を選んで先に進むのが正しい。注意力には限りがあり、依存関係ごとに調査報告を書いていたら肝心の問題が解けなくなる
      例外は二つで、標準ツールが自分のユースケースに本当に合っていない場合か、標準ツール自体が自分の解こうとしている中核問題と大きく重なる場合だ

  • こうした議論はPythonの科学技術計算の限界を指摘する記事に似ていると感じる
    ある程度まともなツールの周囲にコミュニティが臨界質量を超えて集まると、それが他のほとんどの要素を圧倒する
    モメンタムがつき、チュートリアルや解説記事やより良い文書が積み上がって、事実上脱出速度に達する
    LeanはTerrance Taoのような強力な支持者までいて、今まさにそういう位置にあるように見える
    だから「言語Xのほうが優れている」という話が完全に間違いではないとしても、本当に重要な問いを見落としやすい
    みんなが知っていてすぐ使え、より多くの時間が改善に投入されるそのツールより実際に優れているのかが核心だ
    結局はworse is better、あるいは良くて人気があるならそれで十分、という状況に見える

    • LLMが異なる形式体系の翻訳をかなり効果的に可能にしてくれるという点は良い指摘だと思う
      特にこの分野では翻訳結果をかなりの部分自動検証できるので、選択そのものはそれほど大きな問題ではないかもしれない
    • ただしAI時代には臨界質量の重要性ははるかに小さい
      AIは巨大なコミュニティライブラリがなくても自力でコードを書けるし、インターネットにチュートリアルが百万本転がっていなくても文書や仕様を直接読める
      求人市場がない言語を避ける必要もない。AIはキャリアを積むのではなく、いま与えられた仕事をこなせばいいからだ
      だから昔なら機会がなかった小規模言語やDSLにも採用の余地が広がる
      プログラミングで長く続いた言語の単一文化もAIが終わらせるかもしれない

  • 「今日ある形式化されたほぼすべてのものはAUTOMATHでも形式化できただろう」という言い方は、現代の言語で書いているものは50年前のアセンブリでも全部書けたと言うのに似ている
    技術的には正しくても、経済的にはまったく違う

    • アセンブリ言語はたいていチューリング完全だが、証明エンジン側でそれに対応する比較が正確には何なのかはよく分からない

  • 15年ほど前にCoq/Rocqや他のいくつかのツールを触ってみようとしたが、概念以前にソフトウェア自体がまるで理解しにくかった
    証明支援系／対話型定理証明系で奇妙なのは、interactiveという性格のせいで言語とIDEが結びついた形になり、実際にも両者が強く絡み合うことだ
    だから言語だけを切り離して語るのが難しく、どんな環境で使うかも一緒に見なければならない
    私もVS Codeの熱烈なファンではないが、非常に多くの人が使い、大きな資金が投じられて磨かれてきた拡張可能IDEが、代替案の環境よりはるかに先を行っているのは明らかだ
    Natural Numbers Gameのような優れた入門経路も、VS Codeのハックしやすさとエコシステムのおかげで可能になっているように見える
    ただ、Leanを学びながら気になるのは構文拡張性が諸刃の剣だという点だ
    言語を覚えたらその言語で書かれたコードを読みたくなるが、プロジェクトごとに独自DSLを大量に作り始めると収拾がつかなくなるかもしれない
    結局これはコミュニティとエコシステムがどれだけ節度を保てるかにかかっていて、その意味で少し期待しつつ少し不安でもある

  • Leanは数学者に最も愛されている証明支援系でもなければ、ソフトウェアの形式検証に最も適した道具でもない
    ただし両方をそこそここなせて、その代わり最も得がたいモメンタムをつかんだ
    しかもAI時代には、公開された人間が書いたコードの量がエージェントの新しいコード生成能力に直接影響するため、そのモメンタムはさらに強くなる