大規模言語モデルに基づく人工知能技術では、誤った主張を避けるために証明の検証機能が重要です。しかし、機械が誤った主張を行う幻覚は避けられません。AIの展望では、マシンの誤った主張は許されません。Coqを使用した証明の話に戻ります。Coqの証明は人間との対話によって進行し、証明の状態を把握することが重要です。証明の状態には、証明に集中すべき命題と、前提として利用できる命題の情報が含まれています。Coqは問題を分解し、すべてのサブゴールを解決することを目指します。証明の最終目標は、未解決のサブゴールがゼロになることです。
Bing AIの説明
Coqは、定理証明支援系の一つで、数学的な定理をコンピュータで証明するためのプログラムです。Coqは、論理式の形で定理を述べることができ、コンピュータとの対話で証明を作ることもできます。Coqは、OCamlとよく似た形でプログラムが書けるため、そのプログラムを対象とした性質や証明もできます。最終的に作ったプログラムをOCamlなどに自動的に翻訳する機能も付いているため、証明付きのプログラムが作れます。
Coqは、フランスのInria（国立情報学自動制御研究所）で開発された定理証明支援系の一つです。Coqは、1984年にThierry CoquandとGérard Huetによって開発されました。Coqは、論理式の形で定理を述べることができ、コンピュータとの対話で証明を作ることもできます。Coqは、OCamlとよく似た形でプログラムが書けるため、そのプログラムを対象とした性質や証明もできます。最終的に作ったプログラムをOCamlなどに自動的に翻訳する機能も付いているため、証明付きのプログラムが作れます。
https://maruyama097.blogspot.com/2023/06/coq_14.html
 | Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化 新品価格 |
