証明補助装置

RocqIDE での対話型証明セッション。左側に証明スクリプト、右側に証明状態が表示されます。

コンピュータサイエンスと数理論理学において、証明支援装置（Proof Assistant）または対話型定理証明器（Interactive Theorem Prover）は、人間と機械の協働による形式的な証明の開発を支援するソフトウェアツールです。これは、何らかの対話型証明エディタやその他のインターフェースを備えており、人間はこれを用いて証明の探索を誘導することができます。証明の詳細はコンピュータに保存され、いくつかの手順はコンピュータによって提供されます。

この分野における最近の取り組みとしては、これらのツールに人工知能を利用して通常の数学の形式化を自動化することである。[1]

システム比較

名前最新バージョン開発者実装言語特徴
高階論理依存型スモールカーネル証明の自動化
反射による証明		コード生成
ACL28.3マット・カウフマン、J・ストロザー・ムーアコモンリスプいいえ未入力いいえはいはい[2]すでに実行可能
アグダ2.6.4.3 [3]ウルフ・ノレル、ニルス・アンダース・ダニエルソン、アンドレアス・アベル（チャルマーズとヨーテボリ）[3]ハスケル[3]はい
[引用が必要]		はい
[4]		はい
[引用が必要]		いいえ
[引用が必要]		部分的
[要出典]		すでに実行可能
[要引用]
アルバトロス0.4ヘルムート・ブランドルOCamlはいいいえはいはい未知まだ実装されていません
クソ*リポジトリマイクロソフトリサーチとINRIAクソ*はいはいいいえはいはい[5]はい
HOLライトリポジトリジョン・ハリソンOCamlはいいいえはいはいいいえいいえ
HOL4カナナスキス-13（またはレポ）マイケル・ノリッシュ、コンラッド・スリンド他標準MLはいいいえはいはいいいえはい
イドリス2 0.6.0エドウィン・ブレイディイドリスはいはいはい未知部分的はい
イザベルIsabelle2025（2025年3月）ラリー・ポールソン(ケンブリッジ)、トビアス・ニプコウ(ミュンヘン)、マカリウス・ウェンゼル標準ML、Scalaはいいいえはいはいはいはい
傾くv4.23.0 [6]レオナルド・デ・モウラ( Microsoft Research )C++、リーンはいはいはいはいはいはい
レゴ1.3.1ランディ・ポラック（エディンバラ）標準MLはいはいはいいいえいいえいいえ
メタマスv0.198 [7]ノーマン・メギルANSI C
ミザール8.1.11ビャウィストク大学フリーパスカル部分的はいいいえいいえいいえいいえ
ンクム
ニューPRL5コーネル大学コモンリスプはいはいはいはい未知はい
PVS6.0SRIインターナショナルコモンリスプはいはいいいえはいいいえ未知
ロク9.0インリアOCamlはいはいはいはいはいはい
121.7.1フランク・フェニング、カールステン・シュールマン標準MLはいはい未知いいえいいえ未知
  • ACL2 – Boyer-Moore の伝統に基づくプログラミング言語、一階論理理論、および定理証明器 (対話型モードと自動モードの両方を備えています)。
  • Rocq (旧名: Coq ) – 数学的な主張の表現を可能にし、これらの主張の証明を機械的にチェックし、形式的な証明を見つけるのに役立ち、形式仕様の構成的証明から認定されたプログラムを抽出します。
  • HOL定理証明器– LCF定理証明器から派生したツール群。これらのシステムでは、論理的な中核はプログラミング言語のライブラリです。定理は言語の新しい要素を表し、論理的な正しさを保証する「戦略」を通じてのみ導入できます。戦略合成により、ユーザーはシステムとのやり取りを比較的少なくして、意味のある証明を作成できます。このファミリーのメンバーには以下が含まれます。
  • IMPS、対話型数学証明システム。[8]
  • Isabelleは HOL の後継となる対話型定理証明器です。メインのコードベースは BSD ライセンスですが、Isabelle のディストリビューションには、異なるライセンスの多くのアドオンツールがバンドルされています。
  • Jape – Java ベース。
  • 傾く
  • レゴ
  • Matita – 帰納的構成の計算に基づいた軽量システム。
  • MINLOG – 一次最小論理に基づく証明支援ツール。
  • Mizar –自然演繹スタイルの第一階論理とタルスキ-グロタンディーク集合論に基づいた証明支援ツール。
  • PhoX – 拡張可能な高階論理に基づく証明支援システム。
  • プロトタイプ検証システム(PVS) – 高階論理に基づく証明言語とシステム。
  • 定理証明システム(TPS) と ETPS – 単純型ラムダ計算に基づいていますが、論理理論の独立した定式化と独立した実装に基づいた対話型定理証明器です。

ユーザーインターフェース

証明支援システムの人気のあるフロントエンドは、エディンバラ大学で開発されたEmacsベースの Proof Generalです。

Rocqには、OCaml/ GtkをベースにしたRocqIDEが含まれています。Isabelleには、jEditとドキュメント指向証明処理のためのIsabelle/ ScalaインフラストラクチャをベースにしたIsabelle/jEditが含まれています。最近では、 Rocq用のVisual Studio Code拡張機能が開発され、[9] Makarius WenzelによるIsabelle、[10] Lean 4用の拡張機能がleanprover開発者によって開発されました。[11]

形式化の範囲

Freek Wiedijkは、よく知られている100個の定理のリストの中から、定理が形式化されたものの数に基づいて証明支援システムのランキングを作成しています。2025年9月現在、定理の70%以上を形式化した証明を提供しているシステムは、Isabelle、HOL Light、Lean、Rocq、Metamath、Mizarの6つのみです。[12] [13]

注目すべき形式化された証明

以下は、証明支援システム内で形式化された注目すべき証明のリストです。

定理証明補助装置年
四色定理[14]ロク2005
フェイト・トンプソン定理[15]ロク2012
円の基本群[16]ロク2013
エルデシュ・グラハム問題[17] [18]傾く2022
多項式フライマン・ルザ予想​​[19]傾く2023
BB(5) = 47,176,870 [20]ロク2024

参照

注記

  1. ^ Ornes, Stephen (2020年8月27日). 「Quanta Magazine – コンピューターは数学的推論の自動化にどれだけ近づいているか？」
  2. ^ Hunt, Warren; Kaufmann, Matt ; Krug, Robert Bellarmine; Moore, J.; Smith, Eric W. (2005). 「ACL2におけるメタ推論」(PDF) .高階論理における定理証明. コンピュータサイエンス講義ノート. 第3603巻. pp.  163– 178. doi :10.1007/11541868_11. ISBN 978-3-540-28372-0。
  3. ^ abc 「agda/agda: Agdaは依存型プログラミング言語/対話型定理証明器です」GitHub 。 2024年7月31日閲覧。
  4. ^ “アグダ Wiki” . 2024 年7 月 31 日に取得。
  5. ^ 「反射による証明」を検索: arXiv : 1803.06547
  6. ^ 「Lean 4 Releases Page」GitHub . 2025年9月22日閲覧。
  7. ^ 「リリース v0.198 metamath/Metamath-exe」。GitHub。
  8. ^ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). 「IMPS: 対話型数学証明システム」 . Journal of Automated Reasoning . 11 (2): 213– 248. doi :10.1007/BF00881906. S2CID  3084322. 2020年1月22日閲覧。
  9. ^ "coq-community/vscoq". 2024年7月29日 – GitHub経由.
  10. ^ Wenzel, Makarius. 「イザベル」 . 2019年11月2日閲覧。
  11. ^ 「VS Code Lean 4」。GitHub 。2023年10月15日閲覧。
  12. ^ Wiedijk、フリーク (2025 年 9 月 22 日)。 「100の定理を定式化する」。
  13. ^ Geuvers, Herman (2009年2月). 「証明支援システム：歴史、思想、そして未来」. Sādhanā . 34 (1): 3– 25. doi : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 . S2CID  14827467.
  14. ^ Gonthier, Georges (2008)、「形式的証明—4色定理」(PDF)、アメリカ数学会誌、55 (11): 1382– 1393、MR  2463991、2011年8月5日時点のオリジナルよりアーカイブ(PDF)
  15. ^ “Feit Thomson proved in coq - Microsoft Research Inria Joint Centre”. 2016年11月19日. オリジナルより2016年11月19日時点のアーカイブ。 2023年12月7日閲覧。
  16. ^ Licata, Daniel R.; Shulman, Michael (2013). 「ホモトピー型理論における円周の基本群の計算」. 2013 第28回ACM/IEEEコンピュータサイエンス論理シンポジウム. pp.  223– 232. arXiv : 1301.3443 . doi :10.1109/lics.2013.28. ISBN 978-1-4799-0413-6. S2CID  5661377。
  17. ^ 「3500年かけて解明された数学の問題がついに解明」IFLScience . 2022年3月11日. 2024年2月9日閲覧。
  18. ^ Avigad, Jeremy (2023). 「数学と形式的転回」. arXiv : 2311.00007 [math.HO].
  19. ^ Sloman, Leila (2023年12月6日). 「数学の『Aチーム』が加算と集合の重要なつながりを証明」Quanta Magazine . 2023年12月7日閲覧。
  20. ^ 「BB(5) = 47,176,870」を証明しました。The Busy Beaver Challenge . 2024年7月2日. 2024年7月9日閲覧。

参考文献

  • Barendregt, Henk ; Geuvers, Herman (2001). 「18. 依存型システムを用いた証明支援システム」(PDF) . Robinson, Alan JA; Voronkov, Andrei (編).自動推論ハンドブック. 第2巻. Elsevier. pp. 1149–. ISBN 978-0-444-50812-6. 2007年7月27日時点のオリジナル（PDF）からアーカイブ。
  • Pfenning, Fr​​ank . 「17. 論理的枠組み」（PDF） .ハンドブック第2巻 2001年. pp.  1065– 1148.
  • Pfenning, Fr​​ank (1996). 「論理フレームワークの実践」. Kirchner, H. (編). Trees in Algebra and Programming – CAAP '96 . Lecture Notes in Computer Science. Vol. 1059. Springer. pp.  119– 134. doi :10.1007/3-540-61064-2_33. ISBN 3-540-61064-2。
  • コンスタブル, ロバート L. (1998). 「X. コンピュータ科学、哲学、論理学における型」. バス, SR (編).証明理論ハンドブック. 論理学研究. 第137巻. エルゼビア. pp.  683– 786. ISBN 978-0-08-053318-6。
  • ヴィーダイク、フリーク (2005)。 「世界の17の証明者」(PDF)。ラドボウド大学ナイメーヘン校。
  • 定理証明器博物館
  • 依存型を使用した認定プログラミングの「概要」。
  • Coq Proof Assistant の紹介（対話型定理証明の一般的な紹介を含む）
  • Agdaユーザーのためのインタラクティブな定理証明
  • 定理証明ツールのリスト
カタログ
  • カテゴリー別デジタル数学：戦術証明者
  • 自動控除システムとグループ
  • 定理証明と自動推論システム
  • 既存の機械化推論システムのデータベース
  • NuPRL: その他のシステム
  • 「特定の論理フレームワークと実装」。2022年4月10日時点のオリジナルよりアーカイブ。2024年2月15日閲覧。（フランク・フェニング著）。
  • DMOZ : 科学: 数学: 論理と基礎: 計算論理: 論理的枠組み
Retrieved from "https://en.wikipedia.org/w/index.php?title=Proof_assistant&oldid=1319565958"