トップページ⇒math
652コメント203KB

コンピューターによる定理の自動証明

■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん2005/09/06(火) 23:35:12
これが可能になったら数学者という仕事が無くなっちゃうの？
0002１３２人目の素数さん2005/09/06(火) 23:36:59
2
0003１３２人目の素数さん2005/09/07(水) 00:22:52
定理の自動証明が実用レベルに達してるなら他の大抵の仕事も実用レベルに達する。
その時にコンピュータには出来ないような新しい仕事を見つけられなければ
数学者だけでなく殆どの人間の仕事が無くなる。
0004１３２人目の素数さん2005/09/07(水) 00:34:23
で、
コンピュータによる定理の自動証明ってどうやるのさ？
0005１３２人目の素数さん2005/09/07(水) 10:58:40
趣旨とは違うが、「A=B」のような方向はもう少し発展すべきだと思う。
0006１３２人目の素数さん2005/09/07(水) 12:43:47
ゲーデルの考えが正しいとすると、機械には数学者と同じレベルの証明は、
永久に出来ないだろう。
0007１３２人目の素数さん2005/09/07(水) 12:53:17
>コンピュータには出来ないような新しい仕事
何が「美しい」か見極める事(新しくないけど)。
コンピュータの万能性の可能性を否定するにはそれだけで十分。
0008１３２人目の素数さん2005/09/07(水) 13:35:03
主観がない、ということか。
0009１３２人目の素数さん2005/09/07(水) 18:10:37
数学の概念を全て「記号」であらわすというのはライプニッツの目指したもの。
それを2進であらわせれば、コンピュータに数学をやらせる土台ができるかもな〜。
0010１３２人目の素数さん2005/09/07(水) 18:13:06
可能にはなると思うが、
「美しい証明」になるかどうかは別問題。
0011１３２人目の素数さん2005/09/07(水) 18:13:47
既にある証明のデータベース化は進んでないの？自動証明による証明の再現という意味なのだけど。
0012１３２人目の素数さん2005/09/07(水) 18:23:54
意味が概念として理解できなければ組合せの爆発により証明が終了しない。
0013１３２人目の素数さん2005/09/07(水) 20:16:39
数学にも哲学にも通じてる情報科学のあったまぃー人が解決してくれるんでしょ
0014１３２人目の素数さん2005/09/08(木) 00:23:02
以下マジレス
コンピュータによる定理の自動証明は今のところ「少し可能」という状態です。
事実、コンピュータで自動証明された定理も存在します。ただ、その証明はおせじにも美しい証明とはいえないが…
証明の内容は忘れたが、こんなことを前期の授業でやった。
0015１３２人目の素数さん2005/09/08(木) 00:48:41
四色問題か
0016１３２人目の素数さん2005/09/08(木) 01:31:06
>>15
たしか、二等辺三角形がどうたらってやつだった
四色問題は異論があるから微妙じゃない?
0017１３２人目の素数さん2005/09/08(木) 03:48:11
４色問題は、地図を幾つかのパートに分割して、
その全てのパートに対して定理が成り立つことを確認する所を
コンピュータにやらせたんだったっけ？
この場合、コンピュータは人間の作ったアルゴリズム通りに動作しているだけなので、
「自動」証明とは言い難いなぁ。
てか、自動証明って何？コンピュータが1から全部証明やってくれることでしょ？
0018１３２人目の素数さん2005/09/08(木) 07:33:41
四食問題は単に機械的にチェックできる部分をやらせただけなのでは。
微分方程式の数値解を計算機で出すか手計算でやるかの違いみたいな感じがする。

普通の自動証明というと、推論規則と命題を与えてその証明を作らせることかな？
0019１３２人目の素数さん2005/09/08(木) 08:47:53
定理の自動証明は公理から出発して定理が導けるまで動作を続けるか、
定理から証明に必要な公理を導き出す。
0020１３２人目の素数さん2005/09/08(木) 11:02:02
>>19
基本的には¬（公理⇒定理）から自動的に矛盾を導く。
証明が存在するなら、矛盾が導ける。
しかし、存在しない場合にはプロセスが終了しない可能性がある。
0021１３２人目の素数さん2005/09/08(木) 16:06:50
>>20

それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
例えば宇宙の原子の数なんて10^50程度のオーダーしかない。
ちょっと難しい定理の機械証明の探索論理ステップ数なんて
そんなオーダーの組合わせ数じゃ済まないんじゃないの？
0022１３２人目の素数さん2005/09/08(木) 16:45:14
「こういうときにはこの定理を用いる場合が多い」っつー傾向というのがありまして、
そういうメタ知識を用いると、かなりよくなります。
0023１３２人目の素数さん2005/09/08(木) 18:01:02
>>22

それは人間が発見した定理を利用するということ？
それはちょっとズルイというか、やっぱ人間が必要なんじゃないかと
0024１３２人目の素数さん2005/09/08(木) 18:03:40
>>23
なんじゃそりゃ、
もしや0から全てコンピュータに行わせようとしてるのか？
過去の資産を生かさずしてどうする。
0025１３２人目の素数さん2005/09/08(木) 18:08:21
いつまでも人間が面倒みなけりゃならないなら、こっちこそなんじゃそりゃ
と言いたくなるな
0026１３２人目の素数さん2005/09/08(木) 18:25:38
コンピュータは所詮道具なんだよ。
人間がやる定理証明に役立ってくれればいいの。
なんでもかんでもコンピュータにやらせる必要は無いの。
0027１３２人目の素数さん2005/09/08(木) 18:25:42
とりあえず定理のデータベースを作ってくれ。
0028１３２人目の素数さん2005/09/08(木) 18:31:02
>>5
A=B？
0029１３２人目の素数さん2005/09/08(木) 18:35:36
>>26
それで役立つんかい？
人間が証明出来ない定理をコンピュータが証明してくれるとか？
0030１３２人目の素数さん2005/09/08(木) 19:41:41
>>1
正しい定理を見つける仕事は残るだろう。
0031１３２人目の素数さん2005/09/08(木) 20:02:07
ときたまジョブをチェックする仕事は必須
0032１３２人目の素数さん2005/09/08(木) 20:08:24
人間に証明出来ない問題がコンピュータに証明出来るわけないわな。
コンピュータなんてただ計算が速いだけだし。難しい予想なんて解こうものなら既存の数学では無理な場合もあるし、
コンピュータがその道具を作っていくなんてまず不可能じゃね？
0033１３２人目の素数さん2005/09/08(木) 23:08:57
人間だろうがコンピュータだろうが鼠を取るのが良い猫だ。
0034１３２人目の素数さん2005/09/08(木) 23:14:10
コンピュータに快楽と苦痛を与えればなんでも出来る。
0035１３２人目の素数さん2005/09/08(木) 23:57:12
オダインに頼め。
エルオーネの能力に比べれば、証明なんて
0036１３２人目の素数さん2005/09/09(金) 01:31:54
>>34
強化学習も結局はx^nオーダーの計算量となるわけで
0037１３２人目の素数さん2005/09/09(金) 01:36:53
追試・データベース化、翻訳などに役立つであろう。
0038１３２人目の素数さん2005/09/09(金) 05:54:41
合流性とか停止性とかいう話があったよね＞証明系
0039１３２人目の素数さん2005/09/09(金) 13:21:38
おまえらPrologは知ってるよな？
0040１３２人目の素数さん2005/09/09(金) 13:32:45
ああ、あの失敗したプロジェクトで使われた言語ね
第五世代コンピュータ開発計画とかいう税金のムダ使いで
0041１３２人目の素数さん2005/09/09(金) 13:55:07
プログラミング言語で一種のファッションだろ？
0042１３２人目の素数さん2005/09/09(金) 14:14:59
プログラミング言語は流行廃りが激しいから、数学者が勉強すべきものではないだろう。
0043１３２人目の素数さん2005/09/09(金) 14:37:44
自動証明⊆人工知能
と言える？
人間並みの人工知能ができれば、自動証明もできるはず。
0044GiantLeaves ◆6fN.Sojv5w 2005/09/09(金) 17:03:36
証明作成のアルゴリズムとして、どんな方法がありうるのか？
検索の枝きりが難しいと思う。
0045１３２人目の素数さん2005/09/09(金) 17:40:48
あ、今アリゴリズム体操おわっちゃった。
0046１３２人目の素数さん2005/09/09(金) 19:04:07
こっち向いて二人で前ならえ
あっち向いて二人で前ならえ
0047１３２人目の素数さん2005/09/09(金) 22:58:51
>>28
> >>5
> A=B？
ググれ。
0048１３２人目の素数さん2005/09/09(金) 23:15:49
>>47
http://www.google.com/search?num=50&hl=ja&q=A%3DB&lr=lang_ja
http://www.google.com/search?num=50&hl=ja&q=A%3DB%E3%80%80%E8%87%AA%E5%8B%95%E8%A8%BC%E6%98%8E&lr=lang_ja
http://www.google.com/search?num=50&hl=ja&q=A%3DB%E3%80%80%E3%82%B3%E3%83%B3%E3%83%94%E3%83%A5%E3%83%BC%E3%82%BF&lr=lang_ja

ﾊｧ?
0049１３２人目の素数さん2005/09/09(金) 23:30:32
ほらAIってあれだろっ！ドラクエ４に搭載の…
0050１３２人目の素数さん2005/09/10(土) 06:22:49
ボスに向かってザラキを唱えるやつか。
0051１３２人目の素数さん2005/09/10(土) 10:43:48
>>48
キミはgoogle の使い方を知らない。
0052１３２人目の素数さん2005/09/10(土) 11:07:15
この分野は日本では信州大が一番進んでいる
ようだよ。
お前らが大好きな数研の教科書書いてる方が
精力的に進めている
0053１３２人目の素数さん2005/09/10(土) 11:46:30
>>52
mizarは"theorem prover"ではなく"proof checker"ですよ。
checkerでさえ現状ではライブラリ不足で実際に数学では使えないでしょう。
0054482005/09/10(土) 13:48:10
>>51
ではどのようにすればA=BでGoogleで検索できるか教えていただけますか？

(´-`).｡ｏO(二重引用符でくくれとかそういうｵﾁかな？)
0055名無しさん＠そうだ選挙に行こう2005/09/10(土) 23:49:29
挑発したら教えてもらえなくなるよ
0056482005/09/10(土) 23:53:25
はいはいヽ(´ー`)ﾉ
0057名無しさん＠そうだ選挙に行こう2005/09/11(日) 19:18:21
>>53
ライブラリ不足かどうかは知らんが、そもそも現実の数学研究で使えるような
表現力を持つ言語を処理させるのはきついんじゃなかろうかと思う。

>>54
俺も気になる。
「A=B」みたいなのをキーワードにしてGoogleで有意義な情報を引き出せるのか？
まあ元々の発言(>>5)の言わんとするところはわからなくもないが。
0058名無しさん＠そうだ選挙に行こう2005/09/11(日) 22:54:00
コンピュータにPeano算術での自動証明プロセスを与えて、
しらみつぶしで¬(0=0)の証明を探索させたら、
もしかしたら有限時間内に「証明あり」って出力が返る可能性がある?
もしそうなったらどうなるの?
0059名無しさん＠そうだ選挙に行こう2005/09/11(日) 23:03:14
>>58
PA が矛盾してるならあるかもね
0060名無しさん＠そうだ選挙に行こう2005/09/11(日) 23:31:38
>>59
こえー。そしたら帰納法使った証明が全ておじゃんだしZFとかも壊滅だし。
>>58の自動証明を延々走らせてる不信心な暇人っていないのかな。
0061１３２人目の素数さん2005/09/12(月) 08:30:11
A=B 等式証明とコンピュータ, 1997 トッパン
トッパンが2000年に出版事業から撤退したため、あまり知られてない。
幸い原本がpdfで公開されている。クヌースによる序言だけでも読むことを勧める。

http://www.cis.upenn.edu/~wilf/AeqB.html
0062１３２人目の素数さん2005/09/12(月) 17:01:24
>>21
＞それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
人間もバカチョンでしらみつぶしに探してる。意識してないだけ。

人間が証明を見つけるまでの間にもそれこそ長い年月を必要としている。
今のコンピュータよりも人間のほうが優れているかもしれんが
それこそ非常に長い時間をかけた進化の結果である。
0063１３２人目の素数さん2005/09/12(月) 17:05:14
>人間もバカチョンでしらみつぶしに探してる。意識してないだけ。

嘘だろ
0064１３２人目の素数さん2005/09/12(月) 17:12:09
>>63
残念だが本当だ。
ところで、誰かTarskiの量化記号消去について簡単に説明してくれ。
0065１３２人目の素数さん2005/09/12(月) 17:21:28
>>64

話をそらすなよ。しらみつぶしなわけないだろ
しらみつぶしだったら時間がかかりすぎ。
0066１３２人目の素数さん2005/09/12(月) 17:34:00
>>65
いや、そのくらい時間がかかるのが当然なんだ。
それより、質問したことについて知らないなら黙っててくれ。
無知な奴と遊んでる暇はないんだ。
0067１３２人目の素数さん2005/09/12(月) 17:41:41
>>66

時間がかかりすぎというのは１００年とか２００年のオーダー
じゃないんだよ。現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。
0068１３２人目の素数さん2005/09/12(月) 17:43:51
>>67
＞現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。

君以前の人がそうしている。
君がその知識を利用しているときに
そのことを意識できないだけ。
0069１３２人目の素数さん2005/09/12(月) 17:58:40
>>68

過去の知識といっても膨大。
その膨大な知識をしらみつぶしに調べてるわけじゃない。
0070１３２人目の素数さん2005/09/12(月) 18:02:23
彼の「しらみつぶし」って単語の定義が俺様独自定義なんだろ
0071１３２人目の素数さん2005/09/12(月) 18:26:37
昔の人がすでにしらみつぶしに調べてきたから今の人はそうする必要がないという理屈だな
0072１３２人目の素数さん2005/09/12(月) 18:51:19
例えば将棋で次の一手をしらみつぶしで探せるはずがない。
それと同じで証明もこうすればよさそうだ、とある程度見切りをつけて行っているはず。
直観力+構成力+知識・経験が物を言う。
0073１３２人目の素数さん2005/09/12(月) 18:54:43
>>71

その昔のひとが得た結果の組み合わせの数だって膨大。
それを、しらみつぶしに調べてるわけない。
0074712005/09/12(月) 19:28:09
>>72
我々がそういう力を持ってるのは昔の人がしらみつぶしにやって得た知識を
受け継いでるからだと考えることもまったく不可能なわけではないんじゃない？

>>73
まあそうかもしれないとは思うけど、自信を持って言い切れる理由があるの？

一応言っとくと、>>62 を積極的に支持するわけじゃないよ。
けど、間違いだという根拠も持ってないし、
部分的には正しいように思えるからあえてこういうレスをしてみた。
0075１３２人目の素数さん2005/09/12(月) 20:19:54
コンピュータで証明するときに、あらかじめ「知識」のデータベースを入れて
それ使って証明しても「しらみつぶしで証明しました」って言うわけか？
0076１３２人目の素数さん2005/09/12(月) 20:31:51
しらみつぶしって言うのは、たとえて言うなら、10回戦のトーナメント方式の1回戦から全ての対戦を行うことに例えれば。
知識があるっていうのは、経験則でこの対戦は無いってシードの部分がいくつかあって考慮する必要のない部分があるってことでしょ。
0077１３２人目の素数さん2005/09/12(月) 20:39:10
今使ってるパソコンでも、π=3.14・・・とかはいちいち計算しないで使われてるんだろ？
0078１３２人目の素数さん2005/09/12(月) 20:39:15
意味を理解しているならばしらみつぶしに探索しなくてよい。
0079１３２人目の素数さん2005/09/12(月) 21:35:02
おまえら、せめてヒューリスティックスって言葉使えよ・・・
0080１３２人目の素数さん2005/09/12(月) 21:37:47
うむ、そういえばそんな言葉があったな。
最近使ってなかったせいか忘れていた。
0081１３２人目の素数さん2005/09/12(月) 21:39:37
>>77
ヒューリスティックスなしらみつぶしで、「知識」のデータベースを
元に計算してまつ
0082１３２人目の素数さん2005/09/12(月) 21:43:39
>>81
ﾜﾛｽw
0083１３２人目の素数さん2005/09/13(火) 13:45:06
とにかくこのスレは不毛。人間の知能の仕組みなんて誰もなーんも
わかっちゃいない。それをコンピュータでシミュレート出来るわけがない。
映画とかＳＦでは人間なみのロボットが出てくるけど、そんなのまさに
夢物語。人口知能の研究者ってのは鉄腕アトムの読みすぎ。
定理の証明というのは人間の知的能力の一部だけど、まるで解明
0084１３２人目の素数さん2005/09/13(火) 13:49:55
書き込んでる最中に暗殺された>>83のご冥福をお祈り致します。
0085１３２人目の素数さん2005/09/13(火) 16:01:37
>>72
＞証明もこうすればよさそうだ、ある程度見切りをつけて行っているはず

それはしらみつぶしとは矛盾しない。
単に深さ優先探索ではないというだけ。
0086１３２人目の素数さん2005/09/13(火) 16:04:24
>>83-84
ﾜﾛｽw
0087１３２人目の素数さん2005/09/13(火) 16:04:25
＞人間の知能の仕組みなんて誰もなーんもわかっちゃいない。
＞それをコンピュータでシミュレート出来るわけがない。

･･･というより、シミュレートしていたとしても
それに気づくことができないというべきか。

ところで数学の定理の証明がすばらしいものだ
という考えは数学をやっている人間の個人的感情
に過ぎない。
0088１３２人目の素数さん2005/09/13(火) 16:30:30
>>87

定理の証明が出来るということは不思議な能力だという考えは？
0089１３２人目の素数さん2005/09/13(火) 16:38:48
>>88
不思議とは無理解のことである。
0090１３２人目の素数さん2005/09/13(火) 17:06:41
この場合は無理解というより不可解
0091１３２人目の素数さん2005/09/13(火) 17:51:05
地球の原子すべてをシミュレーション出来るコンピュータが出来たら生物はもちろん文明さえもシミュレーション
出来るのではないか。
0092１３２人目の素数さん2005/09/13(火) 18:10:57
>>91

データをどうやって入れるんだよ
0093１３２人目の素数さん2005/09/13(火) 18:15:55
>>91
そのコンピュータは自分自身をシミュレートするのか？
0094１３２人目の素数さん2005/09/13(火) 18:53:47
哲学的な問いでなかなか面白いでつね。
0095１３２人目の素数さん2005/09/14(水) 00:02:45
>>94　
チューリングマシン
とか
停止問題
でぐぐってみ。否定的な結論が出るから。
0096１３２人目の素数さん2005/09/14(水) 06:20:52
証明すべき命題をどう符号化するか、という問題がまずある。
もし、すべての数学定理が計算機で証明できるならば、
たったひとつのアルゴリズムから、次々に定理を自動生成できるんじゃなかろうか？
そんなアルゴリズムが果たして存在するのか？
0097１３２人目の素数さん2005/09/14(水) 07:14:49
>>96
ZFC を計算機で書けばいいわけだから原理的には余裕でできる
けどなんか工夫しないと時間かかりすぎて意味のある定理はほとんど出ないと思う
0098１３２人目の素数さん2005/09/14(水) 07:39:17
>>96
くそ定理は山程合成出来る。
0099１３２人目の素数さん2005/09/14(水) 09:30:09
人間機械論を否定したゲーデルの論文があると聞いた。
彼の不完全性定理を基にしている。
人工知能を研究している人なら知ってるよね？
0100１３２人目の素数さん2005/09/14(水) 10:21:30
>>93
コンピュータをシミュレーションするコンピュータはターゲットのコンピュータより
メモリは大きくスピードも速くなければならない。
0101１３２人目の素数さん2005/09/14(水) 10:31:37
そんなことより地球シミュレータのデータのほうが問題だろ。
全ての原子のデータなんてわかるわけがない。
可能性があるとしたらBig Bangのシミュレータ。
仮に出来たとしても地球が出来るまで相当時間がかかるｗ
■ このスレッドは過去ログ倉庫に格納されています