a4です。Ｐ２Ｐ人工知能「Ｔ」開発(2)

**デフォルトの名無しさん** · 2018/09/02(日) 01:57:35.12

前スレ
a4です。Ｐ２Ｐ人工知能「Ｔ」開発。
https://mevius.5ch.net/test/read.cgi/tech/1517470193/

a4 ◆L1L.Ef50zuAv · 2018/11/05(月) 18:45:30.42

>>929
もともと持ってたんですけど、UFOの実験してたら、壊れちゃったんですよ。
また、携帯会社の誰かに見張られているのでは？といった統合失調症の監視妄想が
強くなってしまうので、無理には購入してません。あと、お金があったら、
TOEFLを受験したいんですよ。１回の受験につき$235かかります。

**ゆりな** ◆Ky/cs3er/I · 2018/11/05(月) 22:52:53.48

私は昔５ちゃんねる（当時は２ちゃんねる）でP2Pソフトを開発していた者ですが
ちょっと来るのが遅かった感じですか？

ちなみに、開発していたのは↓です。
CREA（言語はC#）
https://ja.wikipedia.org/wiki/CREA_(%E3%82%BD%E3%83%95%E3%83%88%E3%82%A6%E3%82%A7%E3%82%A2)
https://github.com/pizyumi/CREA

今となっては懐かしいですね・・・。

**デフォルトの名無しさん** · 2018/11/05(月) 22:55:05.61

あっ、よく見たら上のソースコードはCREACOINのコードでした
CREAのソースコードはGitHubには上げてませんね・・・

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 06:21:53.65

>>931
来るのは遅くないですよ。まだまだこれからです。ただ、自分のやりたいことと、
いろんな人との人間関係があるので、今は英語の勉強をしています。

wikipedia見ました。P2Pニコ動は負荷のかかるものかもしれませんね。

このスレでは１文でもいいので、コードを書いてくれる人を募集しています。
たとえば、

c(i(ありがとう。),o(どういたしまして。))

みたいに。半分完成した「Ｔ」はこちらです。
http://www.01ken.com/art1.html

ただ、現在配っている半分完成した「Ｔ」は小さいバグもあるし、メモリも十分に
確保できていないため、治さないといけないです。その研究時間を作るためにも、
今３０歳ですが、海外の大学院へ留学しようと思っています。

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 06:23:34.22

そういえば、逆にP2P機能はまだ作ってないですね。人が集まらないんですよ。
この板だけだと。他の板へ行くとスレが閉鎖しちゃうし。

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 06:32:08.19

いろんな人からあれやってこれやって言われて混乱してる状態ですが、留学前に、
推薦状を書いてもらうために、教授くらいの人とこのソフトを８割くらい完成させる
というのはありです。そういう先生が３人も見つかるかはわかりませんけどね。
厳しいです。

**デフォルトの名無しさん** · 2018/11/06(火) 09:08:29.18

東京にいっぱい超高層マンションを建てたいのですが、具体的にどうすれば良いのでしょうか？

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 09:26:43.07

>>936
僕と一緒に非ユニタリ量子コンピュータを作って、スパコンの2^(10^10)倍の計算力で、
ビジネスしましょう。

**デフォルトの名無しさん** · 2018/11/06(火) 09:43:38.90

世界を牛耳っているのはユダヤ国際金融資本ですか？

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 09:53:24.88

>>938
僕はリアルで名古屋の宇宙人に会ったとき、世界を牛耳っているのは、
「イルミナティ」と「フリーメイソン」であると、教育を受けました。

**デフォルトの名無しさん** · 2018/11/06(火) 14:45:45.88

中二病乙

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 14:49:16.79

>>940
中二病という単語は、中二の頃に聞いたときは、おじさんたちが何やってるんだろう？
と思いましたが、今となっては、そういう定義かもしれませんが、早めに挫けさせて
負け組にさせる搾取構造なのではないかと思っています。

**ゆりな** ◆Ky/cs3er/I · 2018/11/06(火) 16:10:49.49

>>933
人工知能のコードは書けませんが、興味深いのでスレに参加させていただきたいと思います。

>>934
今はライブラリも豊富だろうし、P2P機能は昔よりも楽に作れるのでしょうね。
ちなみに、CREAは表向きP2P型動画共有を目標にしつつも
仮想空間構築のためのグリッドコンピューティングという個人的な目的がありました。
言ってしまえば、動画共有機能は人集めのためだったのですが、、、
実際は動画共有とかファイル共有でも人が集まらなくて
プロジェクト中断になってしまったので
P2Pで人集めるのは難しいですね。

**ゆりな** ◆Ky/cs3er/I · 2018/11/06(火) 16:12:54.00

私は今はもうP2P関連やるのは辞めちゃって
数学寄りのところにいます。
>>201 >>203 でCoqの名前が挙がってますが、
まあその辺です。
定理証明の分野は広く浅く勉強したことがあるので
ある程度はお教えできることもあるかもしれません。
実はこのスレにはリーマン予想を解決しようとしているという噂を聞いてやってきました。
私は今数理論理学から公理的集合論までの数学の基礎を
コンピュータ上で構築する試みを行っています。
Coqやその他定理証明支援系の二番煎じと言えばそうなのですが、
私は専門家向けじゃなく一般人にも分かりやすいシステムを作れないか
というところを主眼に置いています。

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 16:28:12.03

>>942
P2Pのライブラリ？あるかもですけど、僕は１から作りたい派です。

僕も格子の仮想空間を作ろうと思ったのですが、複雑なシムシティみたいなのを
作ってみたいと思っても、格子上の点を手動で動かしても知能のあることがあまり
できないな、といったところで一旦止まりました。時間をかければ、面白いもの
ができる、ということは信じていますが、玩具的な用途にしかならず、普及しない
と見積もって、それでの人工知能開発を一旦ストップしています。

>>943
考えてることがほぼ同じですね。数理論理学の本とか読んでた頃もありましたけど、
なんか、纏まってなくて好きになれないんですよ。しかも、コンピュータに
入れようと思うと、a=b=cと入力するだけで、a=b, b=c, a=cと理解させないと
いけないなどで、問題が起こると思っています。個人的な意見としては、人間の
扱っている数学は結構曖昧で、神経科学と量子計算で自動定理証明できるように
なったら、その後は、時計の芸術などが発展すると見越してます。僕も一般人に
わかりやすい書籍を売れないか、とか考えてます。

**デフォルトの名無しさん** · 2018/11/06(火) 16:50:08.74

【浜、マⅰトレーヤ】　ナマポ、ニート、ヒキコモリ　＜対＞　ユニクロ、自民党　【分ち合い抵抗勢力】
http://rosie.5ch.net/test/read.cgi/liveplus/1541471001/l50

被災地にはボランティアや義援金が殺到するのに、何で貧困層には無関心なの？　自分達が加害者だから？

a4 ◆L1L.Ef50zuAv · 2018/11/06(火) 17:09:04.06

>>945
ユニクロが敵なんですね。僕の服は意外と原宿で集めましたが。貧困層に無関心なのは、
石油が足らなくなるとか、そういう問題を議論しないといけないと思ってます。

◆QZaw55cn4c · 2018/11/06(火) 20:48:32.85

>>943
＞私は今数理論理学から公理的集合論までの数学の基礎をコンピュータ上で構築する試みを行っています。
論理というのは人間の外にある「客観的」なものではなく、人間の遺伝子に組み込まれた「主観的」あるいは「人間的」なものだという感覚を持っています

**デフォルトの名無しさん** · 2018/11/06(火) 21:26:07.78

本当に絶対に無になってもう二度と有になりたくない。

a4 ◆L1L.Ef50zuAv · 2018/11/07(水) 00:27:32.14

>>948
その手法を一緒に量子計算しませんか？

**ゆりな** ◆Ky/cs3er/I · 2018/11/07(水) 11:00:20.76

>>944
P2P、1から作るのですか・・・大変だと思いますよ？

＞考えてることがほぼ同じですね。数理論理学の本とか読んでた頃もありましたけど、
＞なんか、纏まってなくて好きになれないんですよ。
数理論理学は多分にメタ的ですから。
https://togetter.com/li/988472
たとえば、1階述語論理の上で実際の「普通の」数学を展開する場合、
数理論理学の文献に書いてあるような1階述語論理に対するメタ的な議論は
ほとんど無視して構わないかと。
ただ単に1階述語論理の定義だけ基盤として採用すれば良いです。

＞人間の扱っている数学は結構曖昧で
長大な証明になってくると、数学者でも100%正しいと言える人はいなくなってきます。
たとえば、有限単純群の分類定理の証明は1万5000ページ以上の規模ですが、
この証明は99.99%くらいは正しいと言われていますが、
100%正しいと言える数学者は誰もいないとも言われています。
実際、2004年に証明の完成が宣言された後にギャップが見付かっています。
https://ja.wikipedia.org/wiki/%E6%9C%89%E9%99%90%E5%8D%98%E7%B4%94%E7%BE%A4%E3%81%AE%E5%88%86%E9%A1%9E

＞神経科学と量子計算で自動定理証明できるように
私は量子計算についてはあまり詳しくないのですが、
自動定理証明という問題は計算量的にかなり難しいので
量子計算で自動定理証明が発展するかはちょっと疑問ですね。
っていうのはほとんどの数学って決定不可能（undecidable）なんですよ。
逆に、決定可能だと証明されている数学には簡単な幾何学(Tarski[1948])があるのですが、
「円の面積」のような重要な概念が記述できないという欠陥があります。
それで、もうちょっとまともな幾何学の体系を作ろうとすると今度は決定不可能になってしまうことが証明されています。
しかも、Tarski[1948]による簡単な幾何学の体系をコンピュータ上に実装して
自動定理証明しようとすると非常に非効率なことが分かっています（使い物にならないレベル）。
じゃあ、逆に効率良く自動定理証明できる幾何学の体系ってどんなものなの？という疑問に対してはWu[1977]があります。

**ゆりな** ◆Ky/cs3er/I · 2018/11/07(水) 11:05:21.50

>>947
仰る通りだと思います。
実際のところ、人間が「普通」だと思っている論理って体系的にはかなり複雑怪奇です。
何故人間はこれを自然に感じるのか不思議に感じるほどです。
たとえば、有名なBourbakiにおける自然数「1」は依存する全ての定義を展開していくと
長さ4523659424929の記号列となることが分かっています。
A term of length 4,523,659,424,929（PDF）
https://www.dpmms.cam.ac.uk/~ardm/inefff.pdf
別の例としては、命題論理体系としてHilbert流の最も単純な3つの公理群と1つの推論規則を
採用すると証明がとんでもなく難しくなるというのもありますね。
逆に簡単に証明できるようにしようと思ったら、より複雑な公理や推論規則を採用しなければならなくなります
（あるいは、演繹定理というメタ的なアプローチもあります）。

a4 ◆L1L.Ef50zuAv · 2018/11/07(水) 11:40:21.48

>>950

>P2P、1から作るのですか・・・大変だと思いますよ？
確かに既存のものを使わないと安定しないかもですね。考えておきます。

>ただ単に1階述語論理の定義だけ基盤として採用すれば良いです。
リーマン予想とかだとどうなんでしょうね？Wikipediaで２階述語論理について検索
すると、「空でなく上に有界な実数の集合があるとき常にその集合には上限が存在
するという命題を表すには、二階述語論理が必要となる。」と出てきました。だと
すると、解析学の基礎と関係するリーマン予想には、高階述語論理が必要かもしれ
ません。僕は専攻は数学になれなかったので、今はきちんと理解してませんが。
でも、「Ｔ」は一応、独自の手法で近いことをやっていると考えています。

>たとえば、有限単純群の分類定理の証明は1万5000ページ以上の規模ですが、
これは面白い情報ですね。覚えます。

a4 ◆L1L.Ef50zuAv · 2018/11/07(水) 11:40:58.76

>>950

>私は量子計算についてはあまり詳しくないのですが、
僕は大学生の頃、実際に量子コンピュータを開発している研究室に在籍し、
自動定理証明などに関する論文のようなものを書きました。結果としては、
既存の有名な理論を使うだけでは、シュレディンガーの猫の実験をしたとき、
生きた猫のいる世界から、死んだ猫のいる世界の映像などを見ることはできず、
確かに使い方によっては高速なんですが、使い勝手が悪く、自動定理証明には
あまり使えないというものでした。ところが、その後も独自に研究を進めると、
ナマズが地震予知できるので、その神経についている特異点上の量子の複製という
物理法則を使って、その生きた猫と死んだ猫の世界をくっつけて並列計算して
しまおうと、考えるようになりました。成功するかはよくわかりませんが、僕の
妄想です。

>しかも、Tarski[1948]による簡単な幾何学の体系をコンピュータ上に実装して
>自動定理証明しようとすると非常に非効率なことが分かっています（使い物にならないレベル）。
初等幾何学とか僕、高校時代くらいは苦手だったんですよ。でも、あれの解法の
一般化は面白そうなので、「Ｔ」とかでやってみたいですが、やはり古くから研究
されてるんですね。

a4 ◆L1L.Ef50zuAv · 2018/11/07(水) 12:02:06.25

950を超えたので、次スレ建てました。

a4です。Ｐ２Ｐ人工知能「Ｔ」開発(3)
https://mevius.5ch.net/test/read.cgi/tech/1541559631/

**ゆりな** ◆Ky/cs3er/I · 2018/11/08(木) 10:00:10.95

>>952
ちなみに、P2Pの開発で一番難しいのはテストだと思います。
テストしようと思ってもノードを用意しないとテストにならないので・・・。
もちろんローカルでもテストするのですが、
1台のPCだと処理能力にも限界があって多ノードのテストは難しいです。
しかも、ローカルのテストでは発現しない不具合も出てきたりするので・・・。
私が開発してた時は頭がおかしくなりそうになりました・・・。

＞リーマン予想とかだとどうなんでしょうね
ほぼ間違いなく2階は必要でしょうね。
現代数学はほとんど2階述語論理までは必要としています。
あと、今の数学は基本的にはZFCの上で行われていますので
高階述語論理は必ずしも必要ではないかと。

**ゆりな** ◆Ky/cs3er/I · 2018/11/08(木) 10:00:56.45

>>953
やはり現在の量子コンピュータは特定のアルゴリズムの計算は高速にできても
汎用的なコンピュータとしてはまだまだですよね。
今後もっと使える量子的なコンピューティング方法が見付かる可能性はあるかもしれませんが。

＞初等幾何学
初等幾何学は人工知能に学習させる題材としては面白そうですね。

a4 ◆L1L.Ef50zuAv · 2018/11/09(金) 02:06:47.26

>>955
なるほど。僕も格子の人工生命をP2Pで作ってた頃は同期の問題で訳がわからなく
なってしまいました。しかも、せっかくできたのに、実験してくれる人数が集まらない
というところで止まってしまいました。

数理論理学とか詳しそうですね。僕も昔はそっちの専門家になりたかったのですが、
今は、無職に近い状態で、ここで人工知能を売りながら、３０歳ながらも特異点技術
などを追って、海外への大学院進学を目指してます。

>>956
僕は高度な技術はタイムマシンによる歴史改変と関わってると信じてる人なんですよ。
だから、公に出てくる技術はそこで制限されるのではないかと。5chというのは、
「うそはうそであると見抜ける人でないと(掲示板を使うのは)難しい」ということで
こういう情報も書くんですけどね。

**ゆりな** ◆Ky/cs3er/I · 2018/11/09(金) 19:17:11.86

>>957
＞同期の問題で訳がわからなくなってしまいました
同期は難しいですよね。

＞数理論理学とか詳しそうですね
数理論理学の周辺は広く浅く勉強したことがあります。
深いことはあまり知りません。
＞今は、無職に近い状態で
私も最近仕事を辞めて28歳で無職なので似たようなものですよ。
しかも、オカマになってしまいました（笑）。

a4 ◆L1L.Ef50zuAv · 2018/11/09(金) 21:13:54.74

>>958
なるほど。専攻が近いみたいなので、仲良くなりたいです。「Ｔ」のP2P実験とか
一緒にしませんか？

**デフォルトの名無しさん** · 2018/11/10(土) 01:10:42.37

専攻ってどこですか

a4 ◆L1L.Ef50zuAv · 2018/11/10(土) 04:21:02.25

>>960
僕は大学にいた頃は、量子コンピュータによる自動定理証明と、格子の人工生命を
用いた人工知能で、論文を書いて提出しました。

**ゆりな** ◆Ky/cs3er/I · 2018/11/10(土) 10:21:34.39

>>959
コードは書けませんが、P2Pのテストくらいならできるかもです。
あと、a4さんの目標の1つは、人工知能による数学の重要定理の証明、ですよね？
私は人工知能にはあまり興味がありませんが、
数学の定理をPC上で手動で証明するためのシステムを作っています（Coqに似たようなものとお考えください）。
人工知能を使うか、手動で行うかという違いはあれど
コンピュータ上で数学の定理を証明したいという点は共通しているので
情報、技術などある程度共有できることはあるかもしれません。

a4 ◆L1L.Ef50zuAv · 2018/11/10(土) 10:49:09.72

>>962
ありがとうございます。そうですね。Coqは名前しか聞いたことなくて、逆に使った
ことないんですよ。暗号通信は需要があるみたいなので、実験しておきたかったん
ですけど、まだ先になるかもしれません。ご縁があれば実験しましょう。

**ゆりな** ◆Ky/cs3er/I · 2018/11/10(土) 20:18:03.78

>>963
Coqは難しいです。私は挫折しました。
私はもう少し分かりやすいシステムを開発していて、自然演繹ベースです。
多分よく知られている論理体系の中では自然演繹が最も初学者でも分かりやすいです。
たとえば、命題論理で有名なPeirceの法則は私のシステムで証明すると↓の画像のようになります。
https://i.imgur.com/WMRbwRt.png
上の方にある図のようなものが証明の内容を図的に表したもの（証明図）で
下の方にあるコマンドがこの証明を行うのに必要なコマンド列です。
今のところ私のシステムでは論理式の作成から証明まで全部コマンドを実行することで行います。
これは人間が手動で証明する場合には面倒なのですが（なので今後改善が必要）
人工知能に証明させる場合はコマンドを覚えさせるだけなので楽かもしれませんね。

＞まだ先になるかもしれません
はい、私は私で自分のシステムの開発を続けます。
お互い開発頑張りましょうね！a4さんは大学院進学も。

**デフォルトの名無しさん** · 2018/11/10(土) 20:27:06.42

論文のタイトルを教えてください

a4 ◆L1L.Ef50zuAv · 2018/11/11(日) 10:07:56.16

>>964
自然演繹とかはまだ勉強したことがないですね。本を買わないといけないかもですね。

はい。頑張りましょう。

>>965
僕の書いたことのある論文のようなものは３つあって、

量子アルゴリズムの提案
http://www.01ken.com/report.pdf
人工生命的手法を用いた豊かな個性と曖昧な感情を兼ね備えた論理的に行動する人工知能の開発
http://www.01ken.com/dissertation2.pdf
Contradiction on science and Introduction to philanthrophy
http://www.01ken.com/cosaitp.pdf

です。

**ゆりな** ◆Ky/cs3er/I · 2018/11/11(日) 16:32:51.99

>>966
自然演繹のためだけに本を買うのは勿体ない気がします。
上の論文が書けるレベルなら私より知能レベルは上だと思うので
ネットの情報で十分理解可能かと。
個人的にオススメなテキストは↓です（PDF）。
http://web.sfc.keio.ac.jp/~mukai/modular/gentzen-NK.pdf
証明図についてきちんと定義していますので理解が深まりやすいかと思います。

a4 ◆L1L.Ef50zuAv · 2018/11/11(日) 18:15:58.83

>>967
pdfをdownloadしました。僕はリーマン予想などを解こうと思っていることもあり、
どこかで見たような内容ですね。僕が覚えているのは、完全性定理とか、集合論的
な観点からしても、この演繹があってるとかって。

そういえば、P2Pのテストを一緒にしていただけるのであれば、メールかskype
あたりでやり取りしませんか？今、考えているのは、オープンソースの簡易な
暗号化通信によるチャットとファイル送受信システムです。これで「Ｔ」の
コードを共有します。需要はあるみたいですが、人数がそこまでは集まらない、
というあたりで止まるかもしれませんけどね。

**ゆりな** ◆Ky/cs3er/I · 2018/11/12(月) 15:24:08.85

>>968
＞完全性定理とか、集合論的な観点からしても、この演繹があってるとか
その辺は数理論理学者が保証してくれますので、
普通の数学者は数理論理学者が構築した論理体系の上で数学を行うだけです。
まあ、多少は知っておいても良いかとは思いますが。

＞メールかskypeあたりでやり取りしませんか？
とりあえずメール送りました。

a4 ◆L1L.Ef50zuAv · 2018/11/12(月) 15:33:06.31

>とりあえずメール送りました。
ありがとうございます。メール返信しました。これからもよろしくおねがいします。

**デフォルトの名無しさん** · 2018/11/12(月) 17:00:47.31

自演して楽しい？

a4 ◆L1L.Ef50zuAv · 2018/11/12(月) 17:02:48.05

>>971
自演はしてませんよ。名古屋の宇宙人からのテレパシーは裏技術です。表向きには
統合失調症ということになっています。

**デフォルトの名無しさん** · 2018/12/08(土) 21:25:06.05

ﾎﾓ相手するのはやめたほうがいいぞ
それともｵﾏｴ、ﾎﾓなの

**デフォルトの名無しさん** · 2018/12/09(日) 17:04:16.75

オネエだったりして(笑)

a4 ◆L1L.Ef50zuAv · 2018/12/12(水) 20:44:34.25

>>973->>974
僕は誰とも話す人なのですが。同性との性的な交わりについては、僕はイスラム教と
絡んでいるので厳しいです。

**leicaq** · 2019/01/12(土) 21:54:45.85

>>13
インペリアルの院じゃダメでつか？

**デフォルトの名無しさん** · 2019/01/17(木) 13:40:30.03

埋め

**デフォルトの名無しさん** · 2019/01/17(木) 13:41:05.10

埋め

**デフォルトの名無しさん** · 2019/01/17(木) 20:55:07.89

-🍓-

**デフォルトの名無しさん** · 2019/01/18(金) 01:17:07.92

埋め

**デフォルトの名無しさん** · 2019/01/18(金) 01:18:01.78

埋め

**デフォルトの名無しさん** · 2019/01/18(金) 19:27:03.17

埋め

**デフォルトの名無しさん** · 2019/01/18(金) 19:27:21.26

ume

**デフォルトの名無しさん** · 2019/01/19(土) 01:05:37.36

うめ

**デフォルトの名無しさん** · 2019/01/19(土) 01:05:52.49

梅

**デフォルトの名無しさん** · 2019/01/19(土) 09:24:50.36

うめ

**デフォルトの名無しさん** · 2019/01/19(土) 09:25:11.97

うむ

**デフォルトの名無しさん** · 2019/01/19(土) 20:13:56.30

うお

**デフォルトの名無しさん** · 2019/01/20(日) 00:38:30.72

埋め

**デフォルトの名無しさん** · 2019/01/20(日) 00:38:47.49

**デフォルトの名無しさん** · 2019/01/20(日) 10:47:18.08

う

**デフォルトの名無しさん** · 2019/01/20(日) 10:47:32.93

め

**デフォルトの名無しさん** · 2019/01/20(日) 23:59:11.91

うめー

**デフォルトの名無しさん** · 2019/01/24(木) 01:17:18.41

埋める

**デフォルトの名無しさん** · 2019/01/24(木) 23:36:47.09

埋め

**デフォルトの名無しさん** · 2019/01/24(木) 23:37:12.22

あとちょっと

**さまよえる蟻人間** ◆T6xkBnTXz7B0 · 2019/01/24(木) 23:56:33.93

埋め立てふせ

a4 ◆L1L.Ef50zuAv · 2019/01/25(金) 03:47:40.54

埋めます。

**デフォルトの名無しさん** · 2019/01/25(金) 08:58:42.25

埋め

**デフォルトの名無しさん** · 2019/01/25(金) 08:58:57.82

1000

**1001** · Over 1000

このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 145日 7時間 1分 22秒