表現限界が現れる最小規模は、6頂点。
対象とする実行モデルでは、5頂点以下で識別条件を満たす構造は、元の頂点上の非負な有向ハイパーエッジの和で表現できます。6頂点では、同じ条件を満たしていても、その形式では表現できない構造が現れます。
今回、5頂点以下の対象クラスを網羅し、8,675インスタンスを検証することで、既存の六頂点構成の最小性を確定しました。
この結果は、計算機支援証明と独立した検証プログラムによって支えられています。観測元の共通失効を扱う表現の限界を、最小規模まで明らかにした成果です。
安全性に加え、証拠構成の費用にも根拠を。
実行を検証するには、どの観測元を組み合わせ、どこまで証拠を収集するかを設計する必要があります。その選択は、信頼性と運用コストの両方に影響します。
ChoiceProofの新しい手法は、候補となる観測元、その費用、要求する耐故障条件から、要件を満たす最小費用の証拠構成を求めます。
選ばれた構成が安全性の要件を満たすことを証明し、同じ要件を満たすために必要な費用の下界も示します。構成コストとこの下界が一致するとき、その候補集合内での大域的な最適性が確定します。
同じ要件で、構成コストを10から7へ。
10の候補観測元を用いた構成例では、同じ耐故障要件を維持したまま、全候補を使用する費用10から、費用7の構成へ削減しました。
この例では、費用7が最適であることも確認しています。同じ候補集合で、より安い構成によって同じ要件を満たすことはできません。
実行の安全性と、それを支える証拠の経済性を、ともに検査可能な根拠で支える研究です。
信頼の根拠を、独立に検査できる形へ。
ChoiceProofの研究は、数理的な証明と独立した検証実装に基づいています。結論を、同じ入力から再確認できる形で支えます。
私たちが構築しているのは、AIエージェントの実行を第三者が確かめられるインフラです。その基盤を、計算可能な基準と検査可能な証明によって強化しています。