Leanというプログラミング言語を初めて知った。調べてみたら、LLMとも相性が良さそうで面白い!
生成AIが数学的な問題に取り組むときに、単なる数式処理の問題なら、Maximaのような数式処理ソフトを使えばある程度正しい答えを導いたり、検算したりすることはできる(ハルシネーションのリスクはあるが)
一方、証明問題では論理が正しいかどうかを検証することは非常に難しい。が、Lean 4を使えばその検証が実現できるらしい
どうもbuildが通れば厳密に式変形が正しいことが保証されるようで、つまり「ソースコードのデバッグをする」ことが「数学的な証明問題を解く」ことに対応していると言えそうだ
そして、「ソースコードのデバッグをする」ことは昨今のコーディングエージェントが得意とすることである。そして、アナロジーとして考えると「数学的な証明問題を解く」こともLLMの得意分野になる可能があるのでは?と思っている
私はLeanというプログラミング言語がとても好きです。
RustやTypeScriptなどの一般的な言語では「計算」をするのに対して、Leanでは「証明」を行います。
Leanだからこそできることの単純なものの一つとして、数学的式変形が合っていることを自分自身で機械的に厳密に検証可能になることが挙げられます。
計算が大量にある数学の問題で、式変形が合っているか不安になった経験は誰しもあるはずです。
このような簡単な例を考えてみましょう。
(a+b)(b+c)(c+a) + abc
= … {式変形}
= (a+b+c)(ab+bc+ca)
Rustでこれが正しいことを確認しようとしたとしても、基本的にRustには式変形という概念は存在しません。
左辺と右辺をそれぞれ実装し、a,b,cに具体的な値を代入してみて確認することで証明を実現することはできるように感じます。
しかしたとえa=1, b=2, c=3で成り立っても、全てのあらゆる実数で成り立つことは保証できません。
つまりそれは式変形を証明したとは言えません。
一方、Lean言語を使うとそれが実現可能となります。
これが具体的なLeanの実装です。
このように実装して lake build というコマンドの成功を確認すれば、(1億でも5兆でも)任意の実数でこの式変形が正しいことを証明できます。
そこまでして式変形を証明する必要がある?という疑問は当然あると思います。
例えばあなたがノーベル賞を狙う科学者で、論文内に数百行の式変形があったとします。
この時、それが本当に正しいか自分でも不安になることは当然あると思います。
どれだけすごい方に査読してもらったとしても、特定の1行だけに存在するちょっとしたミスを見つけられない可能性はあり
そのようなケースでは活躍するかもしれません。
加えて更に嬉しいことに、自分の式変形だけでなく他人の式変形の正しさも検証可能にしてくれるので、客観的に正当性を示したい際は非常に有用です。
記法に慣れるまでが大変なので、みんなが使うようになる未来はまだまだ先かもしれません。
しかし、曖昧な情報が増え続けてるこの世の中ではもっと注目されるべき技術だと思います。