大学の数学が期待したほど面白くなかったんだが
■ このスレッドは過去ログ倉庫に格納されています
>>49 これ、20歳で数学諦めてAIに逃げた敗北者の経歴でしょ AIなんて誰でも出来るじゃん
プログラミングすら出来なくてもいい >>55
あれは学者のサラブレッドだし英語圏出身だからあまり庶民には参考にならんな
>>57
いやLLMが何なのか何もわかってないんだけど
生成文法の時代から言語の数学はまだまだって言われてきたけど今も変わらない
人間の言語とAIの言語を比較する数学を解明したらフィールズ賞は無理かもだが
チューリング賞は貰えるんじゃないか LeanがLLMと融合したら9割の数学者はヤバいと、お前ら思わないのか?
小山信也はAIじゃ本当に創造的な数学はできないと言ってるが時間の問題かもしれん >>59
>LeanがLLMと融合したら9割の数学者はヤバいと、お前ら思わないのか?
全く思わないよ? >>61
むしろなぜそれでダメになるかの論拠を示してよ ていうか
コンピュータの人って
自動証明っていう単語に
期待抱きすぎだと思うよ >>62
既に自然言語では質問するとなかなか良い人間レベルの解答を出せる
&GPT5では探索アルゴリズムとQ学習により算数の問題が解けると示唆されている
&AlphaGoでは既に囲碁で人類を打ち負かしている
&Leanでは研究レベルの数学の形式化が蓄積している
これでも可能性が低いと思う? 自然言語で問題を書くところは本質ではないと思うのだが… >>64
解けるって何を?
数学の研究における探索って?
囲碁もオセロも有限だし
研究レベルの数学の形式化って誇大広告じゃない? 一度でいいから
まともな数学書を読破してみてよ
たとえば岩波の起訴数学でもいい 算数制覇しましたぞエッヘンって言ってるみたいに聞こえるんでね >>66
最初二行はふ~んという感じで無視するがw、三つ目の有限はなるほどあんたはそう
考えるのねって感じだな
四つ目はショルツのCondensed理論が典型的じゃん
ちなみに小山信也は、8割9割の論文はそんなに創造的ではなく再利用的なもので、
AIに代替されうると殆ど認めてるからね >>70
>最初二行はふ~んという感じで無視するがw
そこが一番のネックなのね
たぶんダメだよ
>四つ目はショルツのCondensed理論が典型的じゃん
それだけ?
>ちなみに小山信也
誰?
そんなに創造的でなくても別にいいよ
新しい知見が出たらイイだけ
そしてAIが新しい知見を出したのは見たこと無いけど
出したとしてもああ出したんだなってだけじゃないかな 数学者の仕事が1つ増えるだけかも
AIが既に出した結果かどうかチェックするってのがw
まあともかく
面白い結果を早く出してね >>64
>これでも可能性が低いと思う?
途轍もなく低いし
まずは何か出されてから心配したら? 数学は集合論で全部できる
数学は論理学で全部できる
数学は圏論で全部できる
あと何でもイイヤ
全部展開できたからって
それで何が出てくるのかって話
使い古された言葉だけど
abstract nonsenseにならない方が
キモチイイと思うけどね >>71
そこはネックじゃなくて論外ってこと
ちなみにAIコミュニティは算数の問題が解けると数学はすぐ到達できると
見ているらしい。自動推論という意味では本質が変わらないという考えだろう >>74
それは良い反論かもしれないね、本当に成り立つかは別として
集合論、圏論、述語論理をただ形式的に走らせても数学的に価値のある内容は
必ずしも出てこない。それはその通りだろう 数学者を楽にしてくれるツールになってくれるといいかも
これ成り立ちそうだけど証明お願い☆とか
あとは組合せで論文になるw >>76
ダメダメ
丸でダメだよ
>>77
ていうか君が考える「数学」の底の浅さがそう書いたことで露呈してるよ
もしかしたら自動証明やってる人皆かもね >>79
なるほど底が浅いと。具体的にどういう話? >>70
>ショルツのCondensed理論が典型的じゃん
横だが、その辺どういう意味なのか
もうちょっと具体的に知りたい >>81
テクニカルな話は
https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/
を読んだほうが早いよ
要は関数解析における位相線形空間をcondensed集合の線形空間に
置き換えると、アーベル圏のホモロジー代数を展開できることをLeanで検証した >>82
読んでないけど、これって自動証明の要素あるんけ? 軽く読んだけど、これが上でやってた話とどう関係してるのかわからん
Coqで四色定理とかodd order theoremとかと何か違うようには見えないんだが >>80
具体的には基礎数学読んでからにしてねってこと Condenced mathの話は証明が恐らくできていると思われたが非常に複雑なので計算機でチェックしてもらったという内容だったかと 無限にある数学的に真な命題のうち数学的に意味のあるものはほんの一部だからね
AIにその判断をさせるのは厳しいよ
というのも人間だってその数学的意味とはなんなのかハッキリ定義できないんだから chatgpt3.5の場合だが、解が1つもない方程式
(解がないことは高校数学で簡単に示せる)を出題してみると、
chatgpt3.5は「これが解です」とデタラメな解を捏造してくる。
人間側が「間違ってるよ」とだけ指摘すると、chatgpt3.5は
「すみません。これが本当の解です」と別のデタラメな解を捏造してくる。
この作業、何度繰り返しても同じで、
解が1つもないことにchatgpt3.5が気づくことはなく、
延々とデタラメな解を捏造してくる。 従って、chatpgt3.5の回答が正しいかどうかをchatpgt3.5自身が
検証するようにプログラムした場合、chatpgt3.5は
「これが解だ」→「いや違ったわ」→「これが解だ」→「いや違ったわ」→・・・
という無限ループに陥るはず。
適当な回数で打ち切れば無限ループは回避できるが、そのかわり、
最終的に出力された回答は依然としてデタラメな回答ということになる。
こういう問題、AI側はどうやって対処したらいいのか?
言うまでもなく、完璧な対処法は存在しない。
なぜなら、それができたら停止性問題が決定不能であることに矛盾するからだ。 直観的に言えば、与えられた数学の問題の「複雑性」が
決定不能問題の複雑性に肉薄すればするほど、
AIは無限ループに陥りがちになるはず。
しかも、数学ではそのような事象が起こりやすい。
問題文の一部を変えただけで難易度が激変するからだ。
尤も、AIが数学の問題を解けなくなっていくことは
人間にとっても同様であり、難しい数学の問題ほど、人間だって歯が立たない。
そんな状況下で、AIは人間よりもマシな回答(しかし結局はデタラメな回答)を
出力できるようになるのだろうか? ここで言う
>人間よりもマシな回答(しかし結局はデタラメな回答)
とは、
「数学的には間違った解答だが、そのアイデアには新規性があり、
新しい数学が創出できそうだ」
という意味。このレベルに妥協するなら、そのうち可能になるかもしれない。
ただし、それは数学者が仕事を失うことを意味しない。 もしかしたらラマヌジャンみたいなのが生まれるかもね これが自動証明できる?
∃N,s,p,m,P,g(φ∈N
∧s∈N×N
∧∀a∈N∃b∈N([a,b]∈s)
∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
∧∀a∈N(¬[a,φ]∈s)
∧∀M⊂N(φ∈M
∧∀a∈M∃b∈M([a,b]∈s)
→M=N)
∧p∈N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈p)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
∧∀a∈N([a,φ,a]∈p)
∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
∧ ([a,b,c]∈p→[a,d,e]∈p))
∧m∈N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈m)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
∧∀a∈N([a,φ,φ]∈m)
∧∀a,b,c∈N∃d,e∈N([b,d]∈s
∧[a,c,e]∈p
∧([a,b,c]∈m→[a,d,e]∈m))
∧P⊂N
∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
∧g∈N×N
∧∀a∈N([a,a]∈g)
∧∀a,b∈N∃c∈N([b,c]∈s
∧([a,b]∈g→[a,c]∈g∧¬[c,a]∈g))
∧∀n∈N(n≠φ∧¬[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
∧n≠q
∧m≠q
∧[n,q]∈g
∧[q,m]∈g))) 全ての暗号は有限だから必ず解ける
リソース的に無理ってだけ
つまるところ ID:cs8MUWrU は
「1+1が計算できたぞ
これでどんな暗号も解ける」
って言ってるようなもんだと思うよ ちょっと違うか
「どんな暗号も解けるんだぞ怖いか?」
かな >>97
>これが自動証明できる?
随分間違えてた
これで
↓
N,s,p,m,P,g(φ∈N
∧s⊂N×N
∧∀a∈N∃b∈N([a,b]∈s)
∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
∧∀a∈N(¬[a,φ]∈s)
∧∀M⊂N(φ∈M
∧∀a∈M∃b∈M([a,b]∈s)
→M=N)
∧p⊂N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈p)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
∧∀a∈N([a,φ,a]∈p)
∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
∧([a,b,c]∈p→[a,d,e]∈p))
∧m⊂N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈m)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
∧∀a∈N([a,φ,φ]∈m)
∧∀a,b,c∈N∃d,e∈N([b,d]∈s
∧[a,c,e]∈p
∧([a,b,c]∈m→[a,d,e]∈m))
∧P⊂N
∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
∧g⊂N×N
∧∀a∈N([a,a]∈g)
∧∀a,b∈N∃c∈N([a,c]∈s
∧([a,b]∈g→[c,b]∈g∧¬[b,c]∈g))
∧∀n∈N(n≠φ∧¬[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
∧¬[n,q]∈g
∧¬[q,m]∈g))) 頭が消えてた
これで
↓
∃N,s,p,m,P,g(φ∈N
∧s⊂N×N
∧∀a∈N∃b∈N([a,b]∈s)
∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
∧∀a∈N(¬[a,φ]∈s)
∧∀M⊂N(φ∈M
∧∀a∈M∃b∈M([a,b]∈s)
→M=N)
∧p⊂N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈p)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
∧∀a∈N([a,φ,a]∈p)
∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
∧([a,b,c]∈p→[a,d,e]∈p))
∧m⊂N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈m)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
∧∀a∈N([a,φ,φ]∈m)
∧∀a,b,c∈N∃d,e∈N([b,d]∈s
∧[a,c,e]∈p
∧([a,b,c]∈m→[a,d,e]∈m))
∧P⊂N
∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
∧g⊂N×N
∧∀a∈N([a,a]∈g)
∧∀a,b∈N∃c∈N([a,c]∈s
∧([a,b]∈g→[c,b]∈g∧¬[b,c]∈g))
∧∀n∈N(n≠φ∧¬[φ,n]∈s→∃q∈P∃m∈N([n,n,m]∈p
∧¬[n,q]∈g
∧¬[q,m]∈g))) ごめん重複があった
これで
↓
∃N,s,p,m,P,g(φ∈N
∧s⊂N×N
∧∀a∈N∃b∈N([a,b]∈s)
∧∀a,b,c∈N([a,b],[a,c]∈s→b=c)
∧∀a∈N(¬[a,φ]∈s)
∧∀M⊂N(φ∈M
∧∀a∈M∃b∈M([a,b]∈s)
→M=N)
∧p⊂N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈p)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈p→c=d)
∧∀a∈N([a,φ,a]∈p)
∧∀a,b,c∈N∃d,e∈N([b,d],[c,e]∈s
∧([a,b,c]∈p→[a,d,e]∈p))
∧m⊂N×N×N
∧∀a,b∈N∃c∈N([a,b,c]∈m)
∧∀a,b,c,d∈N([a,b,c],[a,b,d]∈m→c=d)
∧∀a∈N([a,φ,φ]∈m)
∧∀a,b,c∈N∃d,e∈N([b,d]∈s
∧[a,c,e]∈p
∧([a,b,c]∈m→[a,d,e]∈m))
∧P⊂N
∧∀q∈P∀b,c∈N([b,c,q]∈m→[φ,b]∈s∨[φ,c]∈s)
∧g⊂N×N
∧∀a∈N([a,a]∈g)
∧∀a,b∈N∃c∈N([a,c]∈s
∧([a,b]∈g→[c,b]∈g∧¬[b,c]∈g))
∧∀n∈N(n≠φ∧¬[φ,n]∈s→∃q∈P∃k∈N([n,n,k]∈p
∧¬[n,q]∈g
∧¬[q,k]∈g))) >>94
それはちょっと面白い話だけど、多分AIはまず形式化されたデータ学習で生産的な
数学から攻略していくようにチューニングされるんじゃないかな
これは>>91と合わせて決定的な山だとは思う
数学的な意味や価値を自律的にかぎ分けるようになってくると一気に革命となるん
じゃないか
例えば関数体で出来たことは代数体で簡単に一般化できないという知識を出せるなら
、更にそれを入力にして探索を進めるような振る舞いはできるだろうし 代数幾何なんかやってると思うけど、これだけ定義に手間暇かかるのにこれくらいのことしか言えんのか。。
ってなる >>97 >>100−102 φが束縛されてないが・・・ >>111
うむ確かに
∃φ∀a(¬a∈φ)
追加で
あとPに1入っちゃうけど関係ないからこのままで そうか別に空集合で無くてもいいから
∃φ
追加だけでもいいか >>98
基本的に暗号の問題は計算量
AIの今の問題は意味理解
根本的に問題が違う。形式化が意味するのは、数学の情報処理自体は可能ってこと >>114
情報処理自体は可能
暗号は解くことが可能
可能であっても無意味ってことを喩えたのよ まあええから
これくらいは解いて見せてほしいものだね
>>102 >>64
「探索アルゴリズム」があると思ってるのがまず噴飯モノ
それを>>70
>最初二行はふ~んという感じで無視するがw
そこがネックでしょ
さらに
譬えとして有限の「囲碁」を出してきてるのが次のコケどころ >>117
>「探索アルゴリズム」があると思ってるのがまず噴飯モノ
普通の数学の問題を解けるくらいに有効な
は入れておくべきか
暗号だって探索アルゴリズムはあるはある >>117
>>118
それらは俺は本質的な批判にならないと思ってるけど、その前に>>89は答えに
なってないと思う。集合論や圏論の一般論だけでは具体的な数学は出てこないって話
だよねと言ったら「底が浅い」と言うからその意味を聞いてるんだけど
改めて聞こう。一般論は具体的な理論と合わせなければ機能しないと言う話だ
それがどう底が浅い、基礎数学選書を読めという話になるのかを説明してくれ >>119
>本質的な批判にならないと思ってる
まあ
やって見せてから大言壮語するべきかと >>119
>底が浅い
深い人は>>102は何かは分かってるのだろうか >>120
根本的にずれてるね
「基礎数学を読むとこういうことがわかる、だから君は底が浅い」という具体的な
説明が必要だと言ってるんだけど
それができないのにただ読め、じゃ何の説得力も中身もない
74 132人目の素数さん 2023/11/30(木) 19:28:21.37 ID:afIXefRn
数学は集合論で全部できる
数学は論理学で全部できる
数学は圏論で全部できる
あと何でもイイヤ
全部展開できたからって
それで何が出てくるのかって話
使い古された言葉だけど
abstract nonsenseにならない方が
キモチイイと思うけどね
これをこっちは反復したわけで、それに底が浅いって言ってるのはブーメランでは? そもそも>>59
>LeanがLLMと融合したら9割の数学者はヤバいと、お前ら思わないのか?
これね
全然そんな感覚誰も持ってないと思うよってのを分かって貰えるかなと
起訴数学ぐらいは読んで欲しいと言ったわけ >>125
「誰も思ってない」という言い回しを使うのが逆に自信無さげに見えてしまう
8割の研究までは代替できそうと言ってる小山信也の例もあるわけだし、T.Taoは
GPTをもうすぐ研究パートナーくらいにはできそうだと言ってる
そしてAIの研究者はAGIを目指してるから、当然やるつもりでいる
GPTの五年前にも、誰もこれだけの成功を予想してなかった
とにかく客観的にはそういう状況だ プログラミングは既にある程度できているわけだから、数学も普通に
考えたら危ないよ。証明はプログラムと同質なんだから ハイハイソノトオリデスワ
ガンバッテネー
>>102ヨロシクー >>127
>小山信也
誰よそれw
まあいいから
8割代替してから誇ってイイヨ
君は何も分かってないってよく分かった もうちょっと言うと
キチンと理解して無いまま虎の威を借りようとしてるだけじゃないかなあ >>128
>証明はプログラムと同質
カリーハワード同型対応持ち出すから
あーこの人は1+1で暗号解いちゃう人だなって思われるのよ たぶん
プログラムで云々は
仕様を与えてそれをプログラムしてくれるってやつでしょ
何処まで出来てるか知らないけど
「Mathematica作ってちょ」でマイMathematica作ってくれるんなら嬉しいね
今のところこれに関しても懐疑的ていうか眉唾
実際にやれてるところを見てみたいね >>132
そっくりそのまま返すよ
可能性を否定してるだけで、数学わかってる奴特有の反論を全く見いだせない
数学者ならちゃんと論理的な理由を添えるけど、あんたのレスにはそれがない まあ、どの辺を根拠に否定したがってるのかは大体わかりはするんだけどさ
でも数学をわかってる人間として反論するなら、もうちょい具体的にやってくれ
ないと、今んとこただの否定してる人だよね >>134は良い反論ではあるのよ
確かにCH同型からだけでは、ただちにAIは数学者になるとは言えない
ただ、それが何を意味するのかを失礼ながらあんたは言語化できないらしい
もしAI研究者がそれを適切に言語化するならば、それが解ける可能性はあるね
誰だっけ?グロタンディークかキレンだったかが、適切な言語が見つかれば
問題は自然に解けると言った。AI研究も同じだろうね なんか人の名前ばかりで語るだけで内容が全く感じられないんだが、こういうの詐欺師と見分けつかないし中身のある話をしろよ
なんかこの人の名前あげときゃいいだろみたいな態度が哲学みたいで気に入らない 実際にLEANやCoqやらで手を動かして苦労した経験とかがまるで感じられないんだよね
とりあえず数万行くらい証明を形式化した経験がないからこんな絵空事が言えるんだと思うよ >>139
できそうな兆候はとっくに挙げてるけど
あんたが読めてないだけ
とりわけ、もしQ*アルゴリズムがGPTベースの自動推論で算数の問題を解けるなら、
数学でできない理由は何もない >>141
それ全く反論になってなくない?
お前の体験談がないから無理に決まってると言ってるの? >>143
他人が研究してることをお前が偉そうに語るなって言ってんだよ
実際LEAN触ったことないんだろ? 「形式化は大変だ→これは絵空事だ」が全く繋がらないんだよね
形式化のデータが蓄積していて、膨大なデータから学習するのがLLMなんだが、
それが算数の問題を考えて解けるようになれば数学もできるのでは、というだけの話
それについて何をどう反論してるわけ?
むしろ躍起になって否定してるほうが今んとこ中身がないよ。あんたも含めて >>145
だからそれ反論になってないじゃん
「具体的に」何が絵空事なのか言ってみ?あと偉そうなのは今んとこあんただよ
なら、お前もAIの研究者じゃないんだから俺らの話に気軽に口挟むなって返せるわ >>142
算数ができて数学ができない理由は?自動推論は自動推論だろ
まともな反論もできないのに何偉そうにしてんの? >>146
形式化の作業やったことないから蓄積してると考えちゃうんだよね
既存の形式化のメンテナンスやら、なんかミスったから最初から証明作り直さないとって世界なんたぞ 俺は予め「LLMの仕組みはまだよくわかってないがかなり上手くいってる」と
言ってるの理解してないな
つまり、展望はまだ不透明なわけよ
ところが自演かなんか知らねえが、アホが延々否定したがってる上に
お前Leanやってねえだろとか言い出したw
自演臭いけど、はっきり言って「できるかどうかわからないね」って素直に認めろよ
まともに否定する根拠を出せないならさ >>149
論外だわ
とっくに機械学習の実験的適用始まってるの知らねえのかよ
そんなグチャグチャならやるわけないだろ
何のためにライブラリがあると思ってんだよ。オープンな再利用のためだぞ こいつAIの研究してる人間だったのか
なんか算数できるAIを作った経験があって話してたのかな >>149
要はコードの整合性取るの難しいって言いたいの?
そういうことをちゃんと言わないと何も伝わらんぞ 大体Leanのトップを仕切ってる奴が、色んな形式化が蓄積してるし学部レベルなら
自動化できるようになるぜって言ってんだからそれはできるんだよ
あと「他人の発言使うな」とか言うのはマジで負けを認めてるようなもんだぞ
そんなこと言い出したらお前自力で証明してない数学の結果を一切使うなって話だ ■ このスレッドは過去ログ倉庫に格納されています