AIのLean証明は意味不明か 型理論を巡り海外で論争
姉妹サイトの新着
海外の数学系掲示板4chan「/sci/」で、AIが自動生成するLean(定理証明支援系)の証明は、構文的には正しくても意味的には支離滅裂なのではないか、という疑問が投げかけられた。これに対し「型には人間が作った数学概念の形式化が反映されているので、そうはならない」という反論が出た一方、「型チェックが通ることと意味が正しく伝わることは別問題だ」とする立場も根強く、群論の具体例まで引っ張り出した議論に発展した。最終的な結論は出ず、終盤は互いを罵り合う展開も見せた。
AIによるLeanの証明が、構文的には正しくても意味的には支離滅裂だったらどうする？数学は現象を説明するための言語であり、「7という色は激しい思想の近くで溶ける」と言っても文法的には正しいが、まともな情報は伝わらない。AIのクズ出力は、借金の穴から這い出るためのマーケティングに過ぎないように見える。
>>1
「AIによるLeanの証明が、構文的には正しくても意味的には支離滅裂だったらどうする？」
それらの大半は人間が書いた数学概念の形式化の上に構築されているから、そうはならない。
「『7という色は激しい思想の近くで溶ける』と言っても正しい」
いや、正しくない。
「AIによるLeanの証明が、構文的には正しくても意味的には支離滅裂だったらどうする？」
それらの大半は人間が書いた数学概念の形式化の上に構築されているから、そうはならない。
「『7という色は激しい思想の近くで溶ける』と言っても正しい」
いや、正しくない。
>>2
「いや、正しくない。」
文法的には正しいだろ。
「いや、正しくない。」
文法的には正しいだろ。
>>1
「AIによるLeanの証明が、構文的には正しくても意味的には支離滅裂だったらどうする？」
「どうする」も何も、もうそうなってるだろ。
「俺のコードはコンパイルが通る」
でも何をするコードなんだ？
「コンパイルが通るんだ！」
それがAI証明の世界だよ。
「AIによるLeanの証明が、構文的には正しくても意味的には支離滅裂だったらどうする？」
「どうする」も何も、もうそうなってるだろ。
「俺のコードはコンパイルが通る」
でも何をするコードなんだ？
「コンパイルが通るんだ！」
それがAI証明の世界だよ。
>>6
「文法的には正しい」
ああ、でもそれは一連の圏エラー(category error)だ。静的型があれば避けられる最も基本的なミスの一つだよ。
「文法的には正しい」
ああ、でもそれは一連の圏エラー(category error)だ。静的型があれば避けられる最も基本的なミスの一つだよ。
>>7
それをLeanの中で示すことはできないんじゃないか？
それをLeanの中で示すことはできないんじゃないか？
>>16
「型を意味的な性質として見ることには色々問題がある」
一つ挙げてみろよ。
「型を意味的な性質として見ることには色々問題がある」
一つ挙げてみろよ。
>>19
任意の有限表示群が自明群かどうかを、型チェックだけで判定するプログラムを書いてみろよ。
型は分類のための枠組みであって、解釈のための仕組みじゃない。後者を変えても前者には何の影響もない、完全に別物なんだ。
任意の有限表示群が自明群かどうかを、型チェックだけで判定するプログラムを書いてみろよ。
型は分類のための枠組みであって、解釈のための仕組みじゃない。後者を変えても前者には何の影響もない、完全に別物なんだ。
>>21
「任意の有限表示群が自明群かどうかを型チェックだけで判定するプログラムを書いてみろよ」
なんでそんなことする必要があるんだ？血圧が上がってきてるのが分かるぞ、ちゃんとした答えが出せないって自覚してるんだろ。
「任意の有限表示群が自明群かどうかを型チェックだけで判定するプログラムを書いてみろよ」
なんでそんなことする必要があるんだ？血圧が上がってきてるのが分かるぞ、ちゃんとした答えが出せないって自覚してるんだろ。
>>19
どう見てもそいつは答えられないよ。
どう見てもそいつは答えられないよ。
>>23
「AIがLeanのバグを見つけたらどうなる」って、それこの話と何の関係があるんだ？
「AIがLeanのバグを見つけたらどうなる」って、それこの話と何の関係があるんだ？
>>1
「数学は言語だ」
違う、数学はたくさんの異なる言語の集まりで、どの言語で書いているかによって同じ記号でも全然違う意味を持つんだ。
「数学は言語だ」
違う、数学はたくさんの異なる言語の集まりで、どの言語で書いているかによって同じ記号でも全然違う意味を持つんだ。
>>22
お前の頭の上を通り過ぎた論点は、お前にはそれができないってことだ。単にお前がその言葉の意味を理解してないからだけじゃなく、論理的に不可能だからできないんだ。
お前の頭の上を通り過ぎた論点は、お前にはそれができないってことだ。単にお前がその言葉の意味を理解してないからだけじゃなく、論理的に不可能だからできないんだ。
型が意味的性質と同じ(isomorphic)だという考えを否定する。使える中で最も表現力の高いマルティン・レーフ型を使っても、この意味的性質はエンコードできないからだ。
他サイトの新着
Leanはどうやって不完全性定理を回避してるんだ？
>>36
回避してないよ。でもそれが何の関係があるんだ？
回避してないよ。でもそれが何の関係があるんだ？
>>37
じゃあ、数学全体をある種の型理論の公理に還元できないなら、どうやって正確な意味論を伝えられるんだ？
じゃあ、数学全体をある種の型理論の公理に還元できないなら、どうやって正確な意味論を伝えられるんだ？
この話題の背景と論点
Lean(リーン)は数学の証明を計算機上で検証する証明支援系で、近年はAIによる定理証明の自動生成にも使われている。スレで問題になったのは、AIが生成した証明が「コンパイル(型チェック)が通る」ことと、その証明が人間にとって意味のある数学的主張になっているかは別問題だという点だ。擁護派は、Leanの型は人間が書いた数学概念の形式化に基づいているため意味不明にはなりにくいと主張したが、反対派は「型はあくまで分類の仕組みであり、意味を保証する機構ではない」として、有限表示群の自明性判定のような具体例を挙げて反論した。終盤ではゲーデルの不完全性定理への言及も出たが、議論を深める方向には進まず、合意は形成されなかった。
※本記事は海外掲示板 4chan /sci/ (Science & Math) のスレッド「What if the AI lean proofs are syntactically correct but semantically gibberish?」から抜粋し、編集部で日本語に意訳したものです。訳文の責任は当サイトにあります。
この記事のリアクション
まだコメントはありません。