目次
＊＊＊＊＊＊＊＊
各種AIシミュレーション紹介・販売ページはこちら。
Product Shop
売上予測や需要変化、収支確認など、事業判断に役立つAIシミュレーションをわかりやすくまとめています。
数字をもとに検討したい方や、企画・業務改善の参考資料を探している方は、ぜひ一度ご覧ください。
AIシミュレーションについてのお問い合わせも下記で受付中
↓↓↓
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
おつかれさんです。
いやー アンソロピックさんのFable5の突然BAN。
フロンティアモデルが一発でBANされるなんて。
もっと使っとけばなあ。
実力はすごかったですよね。
早く復活して欲しいですわな。
そんなこんなで今回は
アート系でも、ビジネス系でもなく、
AI for サイエンス（あえてカタカナで）
これ系でいってみます。
さて、下記の記事に興味があったので、簡易版のAlphaProofを実装してみました。
https://ledge.ai/articles/deepmind_alphaproof_nexus_erdos_problems
本家 Deepmindのブログ （英文)
https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/
以下の記事は数式がちょこちょこ出てきます。
数式はちょっとなあという方は読み飛ばしてください。
簡易版AlphaProofで数学証明に挑戦
今回は、ローカルPC上に作った簡易版AlphaProofを使って、アインシュタイン型の三平方の定理証明をLeanで実装してみました。
といっても、ここで使ったのは本家のAlphaProofそのものではありません。
Leanの証明コードを自動修正するための簡易的な証明エージェントです。
Leanでは、数学の証明をコードとして書くことができます。
そして、そのコードが本当に正しいかどうかを、Leanが厳密にチェックしてくれます。
つまり、ただ「それっぽい説明」を書くのではなく、
コンピューターに検査される形で数学の証明を書くということです。
今回はその題材として、誰でも一度は聞いたことがある「三平方の定理」を選びました。
しかも、普通の三平方の定理ではなく、
「アインシュタインが若いころに考えた」と言われるタイプの証明をテーマにしています。
AlphaProofとは
AlphaProofは、Google DeepMindが発表した数学証明AIの仕組みです。自然言語で書かれた数学問題を、Leanのような形式言語で扱える形に変換し、コンピューター上で正しい証明を探索します。
2024年には、AlphaProofとAlphaGeometry 2を組み合わせたシステムが、国際数学オリンピックの問題で銀メダル相当の成績を出したことでも注目されました。
さらにその後、関連する研究としてAlphaProof Nexusという枠組みも報告されています。
これは大規模言語モデルによる証明案の生成と、Leanによる機械的な検証を組み合わせるもので、エルデシュ問題と呼ばれる未解決数学問題のうち、353件に挑戦して9件を解決したとされています。
ここで重要なのは、AIがただ文章で「それっぽい証明」を作るのではなく、Leanによって証明が本当に正しいか検査される点です。
今回使ったものは本家AlphaProofではなく、その考え方に着想を得てローカルで作った簡易版です。
アインシュタインの三平方の定理証明とは
三平方の定理は、直角三角形について成り立つ有名な定理です。
直角をはさむ2つの辺を a と b、斜めの一番長い辺を c とすると、
a² + b² = c²
になります。
学校では、正方形を描いて面積で説明する証明を見た人も多いと思います。
一方、アインシュタイン型の証明は少し雰囲気が違います。
直角三角形の中に、もう一本線を引きます。
直角のところから、斜辺に向かって垂直に線を下ろすのです。
すると、もとの大きな直角三角形が、2つの小さな直角三角形に分かれます。
ここで面白いのは、
大きな三角形と、分かれた2つの小さな三角形が、全部同じ形になる
という点です。
大きさは違います。
でも形は同じです。
数学では、こういう関係を相似と呼びます。
この「相似」という考え方を使うことで、三平方の定理をとてもすっきり導くことができます。
今回Leanで証明する範囲：幾何全体ではなく読み物としての核心へ
ただし、今回いきなり全部をLeanで証明したわけではありません。
ここはかなり大事です。
本当に厳密にやるなら、Leanの中で、
点A、点B、点Cを定義する
直角三角形であることを定義する
Cから斜辺に垂線を下ろす
3つの三角形が相似であることを証明する
相似なら面積比が辺の2乗比になることを証明する
というところまで全部やる必要があります。
これはかなり大きな作業になります。
そこで今回は、まず一番おいしい部分だけを切り出しました。
それが、
相似三角形の面積比から、三平方の式を導く部分
です。
アインシュタイン型の証明では、3つの三角形が相似になります。
相似な図形では、長さが2倍になれば面積は4倍になります。
長さが3倍になれば、面積は9倍になります。
つまり、面積は長さの2乗に比例します。
この考え方から、
大きい三角形の面積は c² に比例
小さい三角形の一方の面積は a² に比例
もう一方の面積は b² に比例
と考えられます。
そして、大きい三角形は、小さい三角形2つを合わせたものです。
だから、
c² に比例する面積
=
a² に比例する面積
+
b² に比例する面積
となります。
ここから、
c² = a² + b²
が出てくるわけです。
今回Leanで証明したのは、まさにこの部分です。
言い換えると、
図形そのものを完全に証明したのではなく、アインシュタイン型証明の代数コアを形式検証した
という位置づけです。
証明ターゲットを作成する
次に、簡易版AlphaProofに渡すためのLeanファイルを作りました。
Leanでは、まだ証明が完成していない部分に sorry と書くことができます。
これは、ざっくり言えば、
ここはあとで証明する
という印です。
今回の流れでは、まずsorry 入りの証明ターゲットを作りました。
そして、その未完成のLeanファイルを、簡易版AlphaProofに渡して、自動修正できるかを試しました。
最初に狙ったのは、次のような証明です。
c² × k = a² × k + b² × k
k は 0 ではない
だから
c² = a² + b²
ここで k は、面積が辺の2乗に比例するときの共通の係数です。
三角形の形が同じなら、面積は「斜辺の長さの2乗 × 共通係数」の形で表せます。
この共通係数 k が両辺にかかっているので、
k が0でなければ消すことができます。
人間が見れば当たり前に思える操作ですが、Leanではそれをきちんと証明として書く必要があります。
簡易版AlphaProofで証明を自動修正する
準備したLeanファイルを、ローカルの簡易版AlphaProofに渡して実行しました。
実行後、成功ファイルが出力されました。
その中では、未完成だった証明が、Leanで通る形に修正されています。
証明の流れを日本語で書くと、こうです。
まず、
c² × k = a² × k + b² × k
という前提があります。
右側の
a² × k + b² × k
は、まとめると、
(a² + b²) × k
になります。
だから、
c² × k = (a² + b²) × k
です。
そして、k ≠ 0 なので、両辺の k を消せます。
その結果、
c² = a² + b²
が得られます。
Leanのコードでは、この「共通因子を消す」操作がきちんと書かれていました。
これにより、アインシュタイン型三平方証明の中核である、
面積比から三平方の式を導く部分をLeanで証明できたとなります。
間違った証明コードとの比較と今回分かったこと
今回はさらに、比較実験も行いました。
ただ正しい証明が通っただけでは、記事として少し物足りません。
そこで、あえて間違った証明コードも用意しました。
最初に試したのは、命題自体は正しいけれど、証明コードだけが間違っているパターンです。
具体的には、証明部分に ring だけを書きました。
ring は代数式を整理するためのLeanの機能です。
しかし今回の証明では、単に式を整理するだけでは足りません。
前提として与えられた式を使い、さらに k ≠ 0 という条件を使って、共通因子 k を消す必要があります。
そのため、ring だけでは証明として不十分です。
ところが、簡易版AlphaProofを実行すると、この間違った証明コードは修正されました。
最終的には、ちゃんと前提を使い、k ≠ 0 によって共通因子を消す形に直されました。
つまり、
正しい命題に対して、証明コードが不十分だった場合は、簡易版AlphaProofで修正できた
ということです。
偽の命題も試してみる
次に、もっと重要な実験として、数学的に偽の命題も試しました。
本来の証明では、k ≠ 0 が必要です。
そこで、あえてこの条件を外してみました。
するとどうなるか。
もし k = 0 なら、
c² × 0 = a² × 0 + b² × 0
はいつでも成り立ちます。
左も右も0になるからです。
でも、そこから
c² = a² + b²
が成り立つとは限りません。
つまり、k ≠ 0 を外した命題は、数学的には正しくありません。
この偽の命題は、簡易版AlphaProofでも証明できませんでした。
これはかなり大事な結果です。
AIが何でもかんでも「それっぽい証明」を作って通してしまうわけではありません。
最終的にはLeanが、
その証明が本当に正しいかどうか
を厳密にチェックしているということです。
今回の実験で見えたこと
今回の実験で分かったことは、大きく3つあります。
1つ目は、簡易版AlphaProofでも、正しい命題に対してはLean証明を自動修正できる場合があることです。
2つ目は、証明コードが多少間違っていても、適切な形に直せる可能性があることです。
3つ目は、数学的に偽の命題は、最終的にはLeanで通らないということです。
今回実装できたのは、三平方の定理の完全な幾何証明ではありません。
しかし、アインシュタイン型証明の中核である、
相似三角形の面積比
↓
c²k = a²k + b²k
↓
c² = a² + b²
という流れは、Leanで形式証明できました。
読み物として見れば、これはかなり面白い結果です。
数学の証明をAIに任せるのではなく、
AIが証明案を作り、Leanがそれを厳密に検査する。
この役割分担が見える実験になりました。
今後は、さらに一歩進めて、垂線や相似そのものをLeanで扱う方向に進めると、より本格的な幾何証明に近づいていけそうです。
今回使ったleanコードの一例
あくまでもほんの一例です。
そのうちに、本体をGitにアップしようかと。
下記は表示バグで、インデントいまいちです。
お気に入りのAIに修正してもらってください。
import Mathlib
theorem pythagoras_from_area_ratio
{a b c k : ℝ}
(hk : k ≠ 0)
(h : c^2 * k = a^2 * k + b^2 * k) :
c^2 = a^2 + b^2 := by
apply mul_right_cancel₀ hk
calc
c^2 * k = a^2 * k + b^2 * k := h
_ = (a^2 + b^2) * k := by ring
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
最近のデジタルアート作品を掲載！
X 旧ツイッターもやってます。
https://x.com/ison1232
インスタグラムはこちら
https://www.instagram.com/nanahati555/
＊＊＊＊＊＊＊＊＊＊＊＊＊＊
Follow me!
