[過去ﾛｸﾞ] ChatGPTについて、語ろうぜ (1002ﾚｽ)
上下前次1-新
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
862(1): 2023/03/12(日)13:12 ID:djoUlqhE0(1) AAS
ChatGPTが論理的推論に全く向いていないのは重々承知の上で、>>281が出来たならこれはどうだ？と実験
「1+1=2 をペアノの公理、ペアノ算術、等号公理に基づいて証明する」
まずChatGPTの認識を確認し、自然数をペアノの公理に基づいて構成してもらう
（0を自然数に含めるのはブルバキ流）
画像ﾘﾝｸ[png]:i.imgur.com
加法をペアノ算術の公理に基づいて定義してもらう
画像ﾘﾝｸ[png]:i.imgur.com
等号を等号公理に基づいて定義してもらう
画像ﾘﾝｸ[png]:i.imgur.com
もう一度確認して、証明開始
画像ﾘﾝｸ[png]:i.imgur.com
証明の流れを振り返る
また、これを記述するのに適したプログラミング言語は何か？
画像ﾘﾝｸ[png]:i.imgur.com
証明の記述には適さないがよく知られた言語として、Javascriptで実装した例
画像ﾘﾝｸ[png]:i.imgur.com
次に、Wolfram言語で実装した例
（ChatGPTは数学的証明に向いていると言っているが、後でChatGPT自身が言っているように、Wolfram言語も証明の正しさを検証できないので向いてはいない）
画像ﾘﾝｸ[png]:i.imgur.com
最後に、Coqで実装した例
画像ﾘﾝｸ[png]:i.imgur.com
最も適した言語はCoq
画像ﾘﾝｸ[png]:i.imgur.com
実際にCoq Web Editorでこの証明が正当であることを確認する
画像ﾘﾝｸ[png]:i.imgur.com
→「No more goals.」正しい証明であることが確認できた
上下前次1-新書関写板覧索設栞歴
あと 140 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.008s