数学の証明に大規模言語モデル（LLM）は使えるのか
正直無理だと思ってんですけど。ワンチャン狙いで。
大規模言語モデル（LLM）とは
大規模言語モデル（LLM）とは、膨大な量のテキストデータを使ってトレーニングされた自然言語処理のモデルのことです。
LLMは、人間のような自然な言語生成や理解を実現することができます。
LLMは、従来の自然言語処理モデルと比べて、以下の3つの点で大きく異なります。
データ量：LLMは、従来の自然言語処理モデルの100倍以上のテキストデータを使ってトレーニングされます。これにより、より高度な言語の理解と生成が可能になります。
計算量：LLMは、大量の計算量を必要とします。これにより、高性能なハードウェアやクラウドコンピューティングが必要です。
モデルサイズ：LLMは、従来の自然言語処理モデルよりもはるかに大きなモデルサイズを持ちます。これにより、より複雑な言語モデルを構築することができます。
LLMは、さまざまな分野で活用されています。
例えば、以下のようなものが挙げられます。
自然言語処理：質問応答、機械翻訳、文章要約、テキスト生成など
教育：学習支援、個別指導など
ビジネス：顧客対応、マーケティング、広告など
LLMは、今後もさらなる進化が期待されており、さまざまな分野で活躍していくでしょう。
LLMの具体的な例としては、以下のようなものが挙げられます。
GPT-3：OpenAIが開発したLLM
LaMDA：Google AIが開発したLLM
Megatron-Turing NLG：Google AIとNVIDIAが共同で開発したLLM
LLMは、まだ発展途上にある技術ですが、その可能性は非常に大きく、今後の社会に大きな影響を与えることが期待されています。
LLMは、今後もさらなる進化が期待されています。
知らんけど。
LLMの仕組み
LLMの仕組みは、大きく分けて3つのステップで構成されています。
データの収集と前処理
モデルの構築と学習
推論と評価
データの収集と前処理
LLMは、膨大な量のテキストデータを使ってトレーニングされます。
このデータは、Webサイト、書籍、論文、コードなど、さまざまなソースから収集されます。
収集されたデータは、テキストのクリーニングやノイズの除去などの前処理が行われます。
モデルの構築と学習
LLMは、ニューラルネットワークと呼ばれる機械学習モデルによって構成されています。
ニューラルネットワークは、人間の脳の神経回路を模倣したモデルであり、膨大な量のデータから学習することができます。
LLMの学習では、入力テキストと出力テキストのペアを使って、ニューラルネットワークの重みを調整します。
この学習プロセスは、反復的に行われ、ニューラルネットワークはより正確な言語モデルへと進化していきます。
推論と評価
学習が完了したLLMは、新しいテキストを入力して、推論を行うことができます。
推論結果は、人間による評価や、別のLLMによる評価などによって評価されます。
LLMは、まだ発展途上にある技術であり、さまざまな課題が存在します。その一つは、偏見の問題です。
LLMは、トレーニングデータに含まれる偏見を学習してしまうため、偏った推論結果を生成してしまう可能性があります。
もう一つの課題は、誤った情報の生成です。
LLMは、トレーニングデータに含まれる誤った情報も学習してしまうため、誤った情報を生成してしまう可能性があります。
問題点
「推論と評価フェーズ」では、単語や文の組み合わせの確率に基づいて、テキストを生成します。
つまりは結局のところ確率論なので、どんなに簡単な問題でも低確率で間違う可能性があるということです。
とはいえ、あんまりないっゃないですが。
数学の基礎
数学の基礎というと難しそうなイメージあるかもですが、「公理と推論規則」がベースにあります。
「公理」とは
「公理」とは雑に説明すると、「めっちゃ簡単なこと」のことです。
例えば、何も証明されていない公理系だけで考えると、「1の次の数は？」の答えは「2」ではありません。「1の次の数（後続数）」が正解となります。
「2」が定義されていないからです。
ちなみにすでに証明できているものは「定理」と呼ばれ、証明の前提として使うことができます。
数学界におけるセーブデータみたいなもんです。
「推論規則」とは
数学における推論規則とは、論理式から他の論理式を導く推論の規則ですが実はこれまた当たり前のことを言っています。
推論規則は、数学における証明において重要な役割を果たします。
証明とは、ある命題が真であることを示すことです。
推論規則を用いることで、既知の命題から未知の命題を導き出すことができるため、証明を行うことができます。
数学における推論規則には、以下のようなものが挙げられます。
前件肯定：Pが真であるならば、P→Qも真である。
後件否定：Qが偽であるならば、P→Qも偽である。
否定除去：Pと￢Pは同時に真ではない。
否定導入：P→⊥は￢Pを導く。
普遍例化：∀xψ(x)はψ(a)を導く。
存在汎化：ψ(a)は∃xψ(x)を導く。
二重否定の除去：￢￢PはPを導く。
二重否定の導入：Pは￢￢Pを導く。
選言三段論法：P∨Qと￢PはQを導く。
これらの推論規則は、数学において広く用いられています。
推論規則は、論理学の基本的な概念です。数学を学ぶ際には、推論規則の理解が重要です。
Bardにやらせたんでなんかミスってる気がするけど。
LLMではなぜ厳しいのか
冒頭で言った、「正直無理だと思ってんですけど。」はLLMの性質上の問題です。
LLMの言っている推論は「人間の知っているデータから推測して正答率の高そうな答えを生成する」ことなので、人間の知らないことを導き出せるのか結構微妙です。
数学界の推論は「もうすでに知られていること（公理や定理）から推論規則を使用して新たな定理を導く」ことなのでニュアンスというかそもそもが違います。
ワンチャンあるかも
でもワンチャン狙える可能性はあります。人類が証明しきれていないものをAIが証明する可能性が。
LLMもかなりカスタマイズできるようになりました。
そこでLLMを魔改造して数学の推論規則を教え込めばもしかしたらという希望もあります。
人類サイドで解きたい方は申し訳ございません。
オチがつけられない。。。
メンバーシップあるぽよ
リーダー募集中です。
#数学がすき
基本的にふざけてます。たまに真面目になります。ギャップ萌えです。