英DeepMindと数学者ら、AI利用で新たな数学の定理を発見へ 29
ストーリー by nagazou
研究アルゴリズム 部門より
研究アルゴリズム 部門より
AIを活用することで新たな数学の定理の発見や、未証明の予想の解決に役立つという研究結果が発表された。この研究は囲碁AIなどの開発で知られる英DeepMindによるもので、同社はシドニー大学とオックスフォード大学の数学者とともに、数学研究を支援する機械学習フレームワークを構築した。新たに作られたアルゴリズムでは、研究対象を調べる新たなパターンを検索したりできるという。この技術の活用により、順列に関する新しい定理を発見した他、「結び目理論」についても異なる数学の分野をつなぐ新しい関係性を見つけたとしている（DeepMindリリース、ITmedia）。
エレファントな証明 (スコア:1)
コンピュータだけがわかる世界 (スコア:0)
発見された新たな定理って、人間にも理解できるんだろうか。
現有人類の誰にも理解できない定理は定理と呼べるのだろうか。
Re: (スコア:0)
理解できずにAI任せにしていると、いつか「AIの定理は今まで合っていたと思えたけど、それは結果が偶然一致しただった」ということも出てくるよね。
AIが定理にたどり着くために本当に必要なデータを集めたのか、それすら人間に分からないから実はAIにゴミデータを学習させていただけ、なんてこともあり得る。
Re:コンピュータだけがわかる世界 (スコア:1)
そんなの人間がやってる研究でだってしょっちゅう起こってるから
大した問題じゃないよ
Re: (スコア:0)
問題は定理の用途だけでなく、一般のAI利用にも言えるので。
いわゆる「AIのブラックボックス問題」ですね。
Re: (スコア:0)
理屈は判らんけど(たまたま)正解が出る
クラークの第3法則：十分に発達した科学技術は、魔法と見分けがつかない。
ってやつですね。
Re: (スコア:0)
科学は「理屈は今は判らなくても再現性さえ安定してるなら利用する」ものだし
「十分に発達した～」については「専門科には判ってるけどシロウトには判らない」って話だから
とにかくピントずれてるな…
Re: (スコア:0)
ブラックボックス問題を抱えたままAIに依存した社会になると専門科＝すべてAIとなる。
それでもクラークの第3法則発動する。
よって元タイトル「コンピュータだけがわかる世界」が現実になる。
未来人「うちら定理も知らないし、科学技術と魔法の見分けもつかないけど…便利だからOK!」
Re: (スコア:0)
今回のは、機械学習技術で予想を出すとか既存の予想を改善するとかして、数学者がピックアップして証明する話なので
Re: (スコア:0)
4色定理って、最終的にコンピュータの力技で全ての場合を数え上げたと聞くけど、あれは理解できたことになるのかな…？なんで4色？って聞かれても、やってみたらそうだったからとしか答えられないような？
Re: (スコア:0)
多いか少ないかの違いだけで数学の証明って本質的に全パターンに対して真かどうかを調べているだけという実態はあるので、程度の問題になっちゃってる印象。
全てはやってみたらそうだったとしか言えない
Re:コンピュータだけがわかる世界 (スコア:1)
Re: (スコア:0)
確認できなかったら証明できているとは言えないので、そもそも証明成功と発表できないでしょう。
出来たから4色定理が証明されたとされたのです。
コンピュータによる証明は人による自然言語も交えた怪しい証明とは違って異論の余地がなくなりますし、昨今は人の手で証明されてもコンピュータで論理飛躍が無いか確認しますから。
昨今の超厳密な数学の証明はまるでアセンブラーでプログラムを書くかのような状態になっていて、バグ混入の確認が困難なのでコンピュータ支援はよく使われているようです。
写真機が発明された当時 (スコア:0)
レゾンデートルを失ってとち狂った絵描き達は、カンバスに四角だの三角だの塗りたくり始めたが、
「証明なんてAIにやらしとけ」と言う時代が来たら、数学者はどういう道を見出すだろうか。
Re: (スコア:0)
レゾンデートルを失ってとち狂った絵描き達は、カンバスに四角だの三角だの塗りたくり始めたが、
「証明なんてAIにやらしとけ」と言う時代が来たら、数学者はどういう道を見出すだろうか。
大丈夫現代でもEXCELに入力したデータを
電卓で検算しているところはまだある
# 本当にあった怖い話
Re: (スコア:0)
経理あるあるですね。
印刷した伝票持ってきたので、元データくれって言っても、いつまでも送ってこない。
その日のうちに処理しないといけないので、しかたなく電卓で検算
そういうやつに限って
SUMの範囲間違えてる・数式狂ってる・小数点以下の処理間違ってる・もとより入力数値間違ってる
入力前のテンプレから数式間違ってるので毎回繰り返す。
指摘しても直してくれない。
Re:写真機が発明された当時 (スコア:1)
印刷した伝票持ってきたので
いい加減これもなんとかならんもんですかね
印刷した伝票の時点で元はデータなわけで
実データか参照先入りのバーコードなりQRコードなりを入れておけば
再入力せずに済むというのに
レジで出てくるレシート｜領収証なんかも
今のままじゃ紙と労力の無駄使いだよなぁ
# 全盛期から同じことの二度書きが億劫でしょうがない
Re: (スコア:0)
電子帳簿保存法では紙に統一するか、全て電子化してタイムスタンプのシステム使わせるか選ばせるから、これからも紙だよ
Re: (スコア:0)
そうやって必要も無いのに特別対応するからつけあがるんだよ。
印字伝票原則受付禁止を明文化して受付不能で突っ返しとけ。
Re: (スコア:0)
スマホで写真撮ってそれ見ながらスマホの電卓で計算する奴に比べたらマシかと。
本人曰く「これが一番早い」とは言ってましたけどね。
#数字間違いまくり
prologは元々 (スコア:0)
数学の定理の証明のために作られたんですよね
この分野は興味があるので数学の基礎体力を身につけたらチャレンジしたいとおもっています
Re: (スコア:0)
数学の定理の証明のために作られたんですよね
この分野は興味があるので数学の基礎体力を身につけたらチャレンジしたいとおもっています
いやそこは
prologがちゃんと証明できているかを証明するためのシステム
がちゃんと証明できているかを証明するためのシステム
が(ry
・・・・
のためのシステムを作ることにチャレンジしてみてはいかがだろうか
Re: (スコア:0)
このAIに定理を証明するための言語を作らせよう
Re: (スコア:0)
その言語が正しいかどうかのテストにAIをだ・・・
Re: (スコア:0)
定理証明においてディープラーニング使った
証明コード生成行われてる
順列じゃなくて置換だよね (スコア:0)
ちょっと自信が無いけど、日本語だと置換の事を順列と呼ぶことは無いよね
Re: (スコア:0)
機械翻訳なんかで (partial) permutation →順列 になっちゃったんだろうね
arXivの論文のアブストラクトに
> Our approach suggests a solution to the combinatorial invariance conjecture for symmetric groups
我々のアプローチは「対称群」に対する組合せ論的不変量予想の解法を提示する
って書いてることからしても「置換」だと思われる
論文自体のタイトルは「カジュダン・ルスティック多項式の組合せ論的不変量に向けて」だからもっと広い群の話みたいだけど、そのような群の典型例が対称群で、対称群は具体的な置換の話として実感させやすいから広報的な話題として出したって感じなのかな
Re: (スコア:0)
任意の有限群は対称群の部分群として表現できるので、対称群というのは具体例というより寧ろ本丸。
Re: (スコア:0)
でもコクセター群は有限群とは限らないですよね