アカウント名:
パスワード:
数学の自動定理証明はNP問題だからできないだの、形式証明では不十分で数学者の直感的な理解が重要だので、結局人間がやらないといけないとか言われてたね。大規模言語モデルがあればその辺解決すると期待できる。なにより普通のLLMなら話していてかなり人間的な思考をしてるように見えるから、数学でもやってくれそう。学習元データはあるし仮にも数学者が「論文を学習させんな」とは言わないだろう。出力は大抵ゴミだろうけど、定理検証アルゴリズムにまで通せるくらいなら数うちゃ当たる。24時間大量に廻せばその内すごいのを証明してくれる。頑張れ！数学者を首にしてしまえ！
。o 〇（証明は人間に代わってAIがやってくれるようになるかもしれないけど、新しい問題を創る方もお任せできそうなのかしら）
横だがAI自体が新たな問題で（色々な意味で）
個数を数えたり計算が苦手なイメージがあるけど実用になるんだろうか？
この前スラドで話題になった女性宅の暗証番号ボタンに透明塗料、特殊な光あて4桁を特定 [security.srad.jp]の話で、4桁の数字の組み合わせがどれだけあるか議論になって4桁それぞれ数字が違う場合はすぐに解けるのだけど、2つ3つ同じ数字がある場合はすこしもめてた。 ChatGPT3.5に解かせたらさんざんな結果 [srad.jp]だったので、同じくChatGPT3.5使った
NPで済むなら不完全性定理なんて成り立たなかったね
P=NP? 問題は対角線論法で解けないから不完全性定理は関係ないだろ。NPで済むはずないのは正しいが(「決定不可能」クラス)
証明可能な定理に関しては、証明文の長さをnとしてNP問題だね。証明不可能なものは最悪永遠に分からない。
そもそもNPって決定問題のクラスだから出力はYes/Noなわけで、自動証明ってのを証明の文字列を出力することと解釈するとまるで別物だったり
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
アレゲはアレゲ以上のなにものでもなさげ -- アレゲ研究家
こういうの (スコア:0)
数学の自動定理証明はNP問題だからできないだの、形式証明では不十分で数学者の直感的な理解が重要だので、結局人間がやらないといけないとか言われてたね。
大規模言語モデルがあればその辺解決すると期待できる。
なにより普通のLLMなら話していてかなり人間的な思考をしてるように見えるから、数学でもやってくれそう。
学習元データはあるし仮にも数学者が「論文を学習させんな」とは言わないだろう。
出力は大抵ゴミだろうけど、定理検証アルゴリズムにまで通せるくらいなら数うちゃ当たる。
24時間大量に廻せばその内すごいのを証明してくれる。
頑張れ！数学者を首にしてしまえ！
Re:こういうの (スコア:2)
。o 〇（証明は人間に代わってAIがやってくれるようになるかもしれないけど、新しい問題を創る方もお任せできそうなのかしら）
Re: (スコア:0)
横だがAI自体が新たな問題で（色々な意味で）
Re: (スコア:0)
個数を数えたり計算が苦手なイメージがあるけど実用になるんだろうか？
Re: (スコア:0)
この前スラドで話題になった女性宅の暗証番号ボタンに透明塗料、特殊な光あて4桁を特定 [security.srad.jp]の話で、4桁の数字の組み合わせがどれだけあるか議論になって
4桁それぞれ数字が違う場合はすぐに解けるのだけど、2つ3つ同じ数字がある場合はすこしもめてた。
ChatGPT3.5に解かせたらさんざんな結果 [srad.jp]だったので、同じくChatGPT3.5使った
Re: (スコア:0)
NPで済むなら不完全性定理なんて成り立たなかったね
Re: (スコア:0)
P=NP? 問題は対角線論法で解けないから不完全性定理は関係ないだろ。NPで済むはずないのは正しいが(「決定不可能」クラス)
Re: (スコア:0)
証明可能な定理に関しては、証明文の長さをnとしてNP問題だね。
証明不可能なものは最悪永遠に分からない。
Re: (スコア:0)
そもそもNPって決定問題のクラスだから出力はYes/Noなわけで、自動証明ってのを証明の文字列を出力することと解釈するとまるで別物だったり