証明の複雑さ

論理学と理論計算機科学、特に証明理論と計算複雑性理論において、証明複雑性とは、命題を証明または反証するために必要な計算リソースを理解し、分析することを目的とした分野である。証明複雑性の研究では、主にさまざまな命題証明システムにおける証明の長さの下限と上限を証明することに取り組んでいる。たとえば、証明複雑性の主な課題の 1 つは、通常の命題計算であるフレーゲ システムでは、すべてのトートロジーの多項式サイズの証明が認められないことを示すことである。ここで、証明のサイズは単にその中の記号の数であり、証明するトートロジーのサイズに対して多項式である証明は、多項式サイズであると言われる。

証明の複雑さに関する体系的な研究は、計算の複雑さの観点から命題証明システムの基本定義を提供したスティーブン・クックとロバート・レックハウ (1979)の研究から始まりました。特にクックとレックハウは、証明サイズの下限をますます強力な命題証明システムで証明することは、 NPをcoNP (したがってPを NP から)を分離するステップと見なすことができると観察しました。これは、すべてのトートロジーに対して多項式サイズの証明を認める命題証明システムの存在が NP=coNP と同等であるためです。

現代の証明複雑性の研究は、計算複雑性、アルゴリズム、数学の多くの分野からアイデアや手法を引き出します。多くの重要なアルゴリズムとアルゴリズム手法は、特定の証明システムの証明検索アルゴリズムとして使用できることから、これらのシステムで証明サイズの下限を証明することは、対応するアルゴリズムの実行時の下限を意味します。これにより、証明複雑性がSAT 解決などのより応用的な分野に結び付けられます。

数理論理学は命題証明のサイズを研究するための枠組みとしても役立ちます。第一階理論、特にペアノ算術の弱い断片は有界算術と呼ばれ、命題証明システムの統一バージョンとして機能し、さまざまなレベルの実行可能な推論の観点から短い命題証明を解釈するためのさらなる背景を提供します。

命題証明システムは、2 つの入力を持つ証明検証アルゴリズムP ( A、x ) として与えられます。 P がペア ( A、x ) を受け入れる場合、 x はAのP証明であると言います。Pは多項式時間で実行される必要があり、さらに、Aがトートロジーである場合に限り、 A が P 証明を持つことが条件となります。

命題証明システムの例としては、シーケント計算、解像度、切断平面、フレーゲシステムなどがあります。ZFC などの強力な数学理論も命題証明システムを誘導します。ZFCの命題解釈におけるトートロジーの証明は、「はトートロジーである」という形式化されたステートメントの ZFC 証明です。 ${\displaystyle \tau}$${\displaystyle \tau}$

証明の複雑さは、通常、与えられたトートロジーに対してシステムで可能な証明の最小サイズの観点から証明システムの効率性を測定する。証明（または式）のサイズは、証明（または式）を表すために必要な記号の数である。命題証明システムPが多項式的に有界であるとは、サイズ のすべてのトートロジーがサイズ のP証明を持つような定数が存在する場合である。証明の複雑さの中心的な問題は、トートロジーが多項式サイズの証明を許容するかどうかを理解することである。正式には、 ${\displaystyle c}$${\displaystyle n}$${\displaystyle (n+c)^{c}}$

問題(NP 対 coNP)

多項式的に制限された命題証明システムは存在するのでしょうか?

CookとReckhow（1979）は、NP=coNPの場合にのみ、多項式的に制限された証明システムが存在することを観察しました。したがって、特定の証明システムが多項式サイズの証明を認めないことを証明することは、NPとcoNP（したがってPとNP）を分離するための部分的な進歩と見なすことができます。^[1]

証明の複雑性は、 シミュレーションの概念を使用して証明システムの強さを比較します。トートロジーの Q 証明が与えられたときに同じトートロジーの P 証明を出力する多項式時間関数がある場合、証明システムPは証明システムQを p-シミュレートします。 P が Q を p-シミュレートし、 Q が P を p-シミュレートする場合、証明システムPとQはp-同等です。シミュレーションのより弱い概念もあります。証明システムP が 証明システムQをシミュレートするのは、トートロジーAのすべてのQ証明xに対して、 yの長さ、| y | が最大でp (| x |) であるようなAのP証明yが存在するような多項式pが存在する場合です。

例えば、シーケント計算は（あらゆる）フレーゲ系とp-同値である。^[2]

証明システムは、他のすべての証明システムをpシミュレートする場合にp 最適であり、他のすべての証明システムをシミュレートする場合に最適である。そのような証明システムが存在するかどうかは未解決の問題である。

問題（最適性）

p 最適または最適な命題証明システムは存在しますか?

あらゆる命題証明システムP は、 Pの健全性を仮定する公理で拡張された拡張フレーゲによってシミュレートできます。^{[3]最適な（またはp最適な）証明システムの存在は、 NE=coNE （または}E = NE ）という仮定から導かれることが知られています。^[4]

多くの弱い証明システムでは、特定のより強いシステムをシミュレートしないことが知られています（下記参照）。しかし、シミュレーションの概念が緩和された場合、問題は未解決のままです。たとえば、Resolution が拡張 Frege を効果的に多項式的にシミュレートするかどうかは未解決です。^[5]

証明の複雑さに関する重要な問題は、証明システムにおける証明の検索の複雑さを理解することです。

問題（自動化可能性）

Resolution や Frege システムなどの標準的な証明システムで証明を検索する効率的なアルゴリズムはありますか?

この問いは自動化可能性（自動化可能性とも呼ばれる）の概念によって形式化することができる。^[6]

証明システムPが自動化可能であるのは、トートロジーが与えられたときに、のサイズの多項式時間でのP証明を出力し、 の最短のP証明の長さになるアルゴリズムがある場合です。証明システムが多項式的に制限されていない場合でも、自動化可能であることに注意してください。証明システムPが弱自動化可能であるのは、証明システムRがあり、トートロジーが与えられたときに、のサイズの多項式時間で のR証明を出力し、 の最短のP証明の長さになるアルゴリズムがある場合です。 ${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$${\displaystyle \tau}$

興味深い証明システムの多くは自動化できないと考えられています。ただし、現在のところ、条件付きの否定的な結果のみが知られています。

• KrajíčekとPudlák（1998）は、RSAがP/polyに対して安全でない限り、拡張フレーゲ暗号は弱自動化可能ではないことを証明した。^[7]
• Bonet、Pitassi、Raz (2000)は、 Diffie-Hellman 方式が P/poly に対して安全でない限り、-Frege システムは弱自動化可能ではないことを証明しました。 ^[8]これは Bonet、Domingo、Gavaldá、Maciel、Pitassi (2004) によって拡張され、Diffie-Hellman 方式が指数関数的時間で動作する非一様攻撃者に対して安全でない限り、深さが少なくとも 2 の定数深さの Frege システムは弱自動化可能ではないことを証明しました。^[9]${\displaystyle TC^{0}}$
• AlekhnovichとRazborov (2008)は、ツリー状のResolutionとResolutionは、FPT=W[P]でない限り自動化できないことを証明しました。^[10]これは、GalesiとLauria (2010)によって拡張され、NullstellensatzとPolynomial Calculusは、固定パラメータ階層が崩壊しない限り自動化できないことを証明しました。^{[11] Mertz、Pitassi、Wei (2019)は、}指数時間仮説を仮定すると、ツリー状のResolutionとResolutionは、特定の準多項式時間でも自動化できないことを証明しました。^[12]
• AtseriasとMüller (2019)は、P=NPでない限り、Resolutionは自動化できないことを証明した。^[13]これは、de Rezende、Göös、Nordström、Pitassi、Robere、Sokolov (2020)によって、NullstellensatzとPolynomial Calculusの自動化のNP困難性に拡張され、^[14] Göös、Koroth、Mertz、Pitassi (2020)によって、Cutting Planesの自動化のNP困難性に拡張され、^{[15] Garlík (2020)によって、} k - DNF Resolutionの自動化のNP困難性に拡張された。 ^[16]

Resolution の弱い自動化可能性が、標準的な複雑性理論の困難性の仮定を破るかどうかは不明です。

良い面としては、

• BeameとPitassi（1996）は、木のようなResolutionは準多項式時間で自動化可能であり、Resolutionは小さな幅の式では弱指数関数的時間で自動化可能であることを示した。^{[17] [18]}

命題証明システムは、高次の理論の非一様等価物として解釈できます。等価性は、有界算術の理論の文脈で最も頻繁に研究されます。たとえば、拡張フレーゲシステムは、多項式時間推論を形式化するクックの理論に対応し、フレーゲシステムは推論を形式化する理論に対応します。 ${\displaystyle \mathrm {PV} _{1}}$${\displaystyle \mathrm {VNC} ^{1}}$${\displaystyle {\mathsf {NC}}^{1}}$

この対応はスティーブン・クック（1975）によって導入され、彼は理論のcoNP定理（形式的には公式）が拡張フレーゲにおける多項式サイズの証明を伴うトートロジーの列に変換されることを示した。さらに、拡張フレーゲはそのようなシステムの中で最も弱いシステムである。別の証明システムPがこの特性を持つ場合、Pは拡張フレーゲをシミュレートする。^[19]${\displaystyle \Pi _{1}^{b}}$${\displaystyle \mathrm {PV} _{1}}$

ジェフ・パリスとアレックス・ウィルキー（1985）によって提案された、 2階述語と命題論理式の間の代替変換は、フレーゲや定数深度フレーゲなどの拡張フレーゲのサブシステムを捉えるのに、より実用的であった。^{[20] [21]}

前述の対応は、理論の証明が対応する証明システムにおける短い証明のシーケンスに変換されることを示していますが、逆の含意の形も成り立ちます。証明システムP に対応する理論T の適切なモデルを構築することで、証明システムPの証明のサイズの下限を導くことができます。これにより、モデル理論的構成を介して複雑さの下限を証明することができ、これはAjtaiの方法として知られるアプローチです。 ^[22]

命題証明システムは、トートロジーを認識するための非決定性アルゴリズムとして解釈できます。したがって、証明システムPの超多項式下限を証明すると、 Pに基づく SAT の多項式時間アルゴリズムの存在が排除されます。たとえば、不満足なインスタンスに対するDPLL アルゴリズムの実行は、ツリー状の Resolution 反駁に対応します。したがって、ツリー状の Resolution の指数的下限 (以下を参照) により、SAT の効率的な DPLL アルゴリズムの存在が排除されます。同様に、指数的 Resolution 下限は、CDCLアルゴリズムなどの Resolution に基づく SAT ソルバーが (最悪の場合) SAT を効率的に解決できないことを意味します。

命題証明の長さの下限を証明することは、一般的に非常に困難です。しかし、弱い証明システムの下限を証明する方法はいくつか発見されています。

• Haken（1985）は、解像度と鳩の巣原理の指数下限を証明した。^[23]
• Ajtai (1988) は、一定深さの Frege システムと鳩の巣原理の超多項式下限を証明しました。^{[24]これは Krajíček、Pudlák、Woods [25]}と Pitassi、Beame、Impagliazzo ^[26]によって指数下限に強化されました。Ajtai の下限はランダム制約法を使用しており、これは回路の複雑さにおけるAC ⁰下限を導くためにも使用されました。
• Krajíček (1994) ^[27]は実行可能な補間法を定式化し、後にそれを用いてResolutionやその他の証明システムの新しい下限値を導出した。^[28]
• Pudlák（1997）は実行可能な補間により切断面の指数下限を証明した。^[29]
• ベン・サッソンとウィグダーソン（1999）は、レゾリューション反証のサイズの下限をレゾリューション反証の幅の下限に減らす証明方法を提供し、これはハーケンの下限の多くの一般化を捉えた。^[18]

フレーゲ系の非自明な下限値を導くことは長年の未解決問題である。

形式のトートロジーについて考えてみましょう。トートロジーは のあらゆる選択に対して真であり、 との評価を固定した後、それらは互いに素な変数の集合上で定義されているため独立です。つまり、と の両方が成り立つような補間回路 を定義できます。補間回路は、のみを考慮して、が偽であるか が真であるかを決定します。補間回路の性質は任意です。ただし、の構築方法のヒントとして、最初のトートロジーの証明を使用することは可能です。証明システムPは、補間がP内のトートロジーの任意の証明から効率的に計算できる場合、実行可能な補間を持つと言われています。効率は証明の長さに関して測定されます。証明が長いほど補間を計算する方が簡単なので、この特性は証明システムの強さにおいて反単調であるように思われます。 ${\displaystyle A(x,y)\rightarrow B(y,z)}$${\displaystyle y}$${\displaystyle y}$${\displaystyle A}$${\displaystyle B}$${\displaystyle C(y)}$${\displaystyle A(x,y)\rightarrow C(y)}$${\displaystyle C(y)\rightarrow B(y,z)}$${\displaystyle A(x,y)}$${\displaystyle B(y,z)}$${\displaystyle y}$${\displaystyle A(x,y)\rightarrow B(y,z)}$${\displaystyle C}$${\displaystyle C(y)}$${\displaystyle A(x,y)\rightarrow B(y,z)}$

以下の 3 つのステートメントは同時に真ではあり得ません: (a)ある証明システムで短い証明がある。 (b) そのような証明システムには実行可能な補間がある。 (c) 補間回路は計算上困難な問題を解決します。 (a) と (b) は小さな補間回路があることを意味していることは明らかですが、これは (c) と矛盾しています。 このような関係により、証明の長さの上限を計算の下限に変換でき、効率的な補間アルゴリズムを証明の長さの下限に変換できます。 ${\displaystyle A(x,y)\rightarrow B(y,z)}$

解像度や切断面などのいくつかの証明システムでは、実行可能な補間またはその変形が認められています。^{[28] [29]}

実行可能な補間は、弱い形式の自動化可能性と見なすことができます。実際、拡張フレーゲなどの多くの証明システムでは、実行可能な補間は弱い自動化可能性と同等です。具体的には、多くの証明システムPは、自身の健全性を証明できます。これは、「が式のP証明である場合、が成り立つ」と述べるトートロジーです。ここで、は自由変数によってエンコードされます。さらに、およびの長さが与えられれば、多項式時間でのP証明を生成することができます。したがって、 Pの健全性の短いP証明から得られる効率的な補間は、与えられた式が短いP証明を許容するかどうかを決定します。このような補間を使用して、 Pが弱く自動化可能であることを証明する証明システムRを定義できます。^[30]一方、証明システムPの弱い自動化可能性は、 P が実行可能な補間を許容することを意味します。しかし、証明システムP が自身の健全性を効率的に証明できない場合、実行可能な補間を認めていても弱自動化可能ではない可能性があります。 ${\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}$${\displaystyle \pi}$${\displaystyle \phi (x)}$${\displaystyle \phi (x)}$${\displaystyle \pi,\phi,x}$${\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}$${\displaystyle \pi}$${\displaystyle \phi}$${\displaystyle \phi}$${\displaystyle \pi}$

多くの非自動化結果により、それぞれのシステムで補間が実行可能ではないという証拠が提供されます。

• KrajíčekとPudlák（1998）は、RSAがP/polyに対して安全でない限り、拡張フレーゲは実行可能な補間を許容しないことを証明した。^[31]
• ボネット、ピタッシ、ラズ（2000）は、ディフィー・ヘルマン方式がP/polyに対して安全でない限り、-フレーゲシステムは実行可能な補間を許容しないことを証明した。^[32]${\displaystyle TC^{0}}$
• Bonet、Domingo、Gavaldá、Maciel、Pitassi（2004）は、Diffie-Helman方式が指数関数的時間で動作する非均一な敵に対して安全でない限り、定数深度のFregeシステムは実行可能な補間を許容しないことを証明した。^[33]

証明のサイズを比較するという考え方は、証明を生成するあらゆる自動推論手順に使用できます。命題非古典的論理、特に直観論理、様相論理、非単調論理の証明のサイズについていくつかの研究が行われてきました。

Hrubeš (2007–2009)は、単調実行可能補間のバージョンを使用して、いくつかの様相論理と直観主義論理における拡張フレーゲシステムの証明のサイズの指数下限を証明しました。^{[34] [35] [36]}

• 計算の複雑さ
• 回路の複雑さ
• コミュニケーションの複雑さ
• 数学的論理
• 証明理論
• 複雑度クラス
• NP（複雑さ）
• 共NP

• ビーム、ポール、ピタッシ、トニアン(1998)、「命題証明の複雑さ: 過去、現在、そして未来」、欧州理論計算機科学協会紀要、65 :66–89、MR  1650939、ECCC  TR98-067
• クック、スティーブン、グエン、フォン（2010）、論理的証明複雑性の論理的基礎、Perspectives in Logic、ケンブリッジ：ケンブリッジ大学出版局、doi：10.1017/CBO9780511676277、ISBN 978-0-521-51729-4、MR  2589550（2008年の草案）
• Krajíček, Jan (1995)、有界算術、命題論理、計算量理論、ケンブリッジ大学出版局
• Krajíček, Jan (2005)、「証明の複雑さ」(PDF)、Laptev, A. (編)、第 4 回ヨーロッパ数学会議の議事録、チューリッヒ: ヨーロッパ数学協会、pp. 221–231、MR  2185746
• Krajíček、Jan、Proof Complexity、ケンブリッジ大学出版局、2019 年。
• パドラック、パベル (1998)、「証明の長さ」、Buss、SR (編)、証明理論ハンドブック、論理学と数学の基礎研究、第 137 巻、アムステルダム: 北ホラント、pp. 547–637、doi :10.1016/S0049-237X(98)80023-2、MR  1640332

• 証明の複雑さ
• 証明の複雑さに関するメーリング リスト。