証明書と検査
Structure Computer のどの答えにも証明書が付く。証明書があれば、計算をした側を信じなくても、答えが正しいことを確かめ直せる。この文書は、証明書が何のためにあり、何が入っていて、どう検査し直せるかを説明する。
なぜ証明書を付けるのか
答えを計算する部分は大きく複雑で、間違いを含みうる。そこで Structure Computer は、計算する部分を信頼しなくてよいように作られている。
- 計算する部分は、答えと一緒に、それを安く確かめるための手がかりを作る。
- 問い・答え・手がかり・前提と、よりどころにする定理の名前を、証明書にまとめる。
- 計算する部分とは別のプログラム（検査器）が、証明書だけを使って、定義どおりに確かめ直す。検査器は計算する部分のプログラムを読み込まない。
- 検査に通らなければ計算し直し、それでも通らなければ、理由を付けて「結果なし」を返す。検査に通っていない答えを、確定した答えとして返すことはない。
答えを出すのは難しくても、正しい答えを確かめるのはやさしい、という場合が多い。証明書はその差を使う。
証明書に入っているもの
証明書は JSON の文書で、大まかに次のものが入っている。
| 中身 | 意味 |
|---|---|
| 問いと入力 | どの問いを、どの系・パラメータ・状態・体について問うたか |
| 答え（主張） | 答えそのもの。たとえば「t = σⁿ s ⇔ n ≡ r (mod M)」 |
| 確かさの種類 | 確定・確率的に確定・復元値・統計・結果なし。前提・仮定・誤り確率の上界・統計量・理由があれば、それも |
| 手がかり | 検査器が答えを安く確かめるための材料。検査器は、どの手がかりも使う前にそれ自体が正しいかを確かめる |
| 定理の名前 | 答えのよりどころにする、Lean で証明した定理の名前 |
| 種 | 計算の中の乱択に使った種。同じ種なら同じ証明書になる |
| 検査の記録 | 計算し直した回数など、検査がどう行われたか |
検査器は、引用すべき定理の一覧も自分で決め、証明書の一覧と完全に一致することを求める。また、証明書の外側に書いた答えが、中身で示した答えと食い違っていれば不合格にする。
何を信頼の土台にしているか
| 答え | 信頼するもの |
|---|---|
| 主な答え | 「検査器が確かめる条件が成り立てば答えは正しい」という、Lean で事前に証明した定理（Lean の核と数学ライブラリ Mathlib を信頼する）と、検査器 |
| 𝔽_q 上の Lyness 写像の Id(s, t) | 上に加えて、正しさ自体を Lean で証明した検査プログラムでも検査できる。その場合に信頼するのは、Lean（コンパイラと実行時を含む）と、証明書を読み取る部分だけになる |
| 確率的に確定 | 軌道をたどる代わりに付けた確率的な証明の検証と、その誤り確率の上界 |
| 統計 | 定理ではない。標本にもとづく推定であることを、答えの種類で明示する |
正直に書いておくと、検査器が Lean の定理の定義を正しく写していることは、試験で確かめているが、証明はしていない。また、一部の問い（可積分性の判定の一部など）には、Lean で証明していない部分がある。確率的な証明が軌道を正しく表していることも、説明はあるが Lean の定理ではない。Lean で正しさを証明した検査器が引き受ける範囲を広げることが、信頼の土台を小さくする道である。
サイトで検査し直す
試すページで、次のように証明書を検査し直せる。
- 結果カードから：カードの「詳細」を開くと、「検査器でもう一度検査」で同じ証明書を検査し直せる。「証明書をダウンロード」で保存もできる。
- 証明書を読み込んで：試すページの下の「証明書の検査（改竄テスト）」を開き、証明書を貼り付けるか、ファイルを読み込んで「検査する」を押す。「最後に開いた結果の証明書を入れる」で、直前に見た答えの証明書を入れることもできる。
- 改竄テスト：貼り付けた証明書の数字（たとえば答えの歩数）を 1 つ書き換えて検査すると、検査器はそれを不合格にする。手がかりと答えが食い違うからである。
- Lean の検査器：「Lean の検査器でも検査する」を選ぶと、𝔽_q 上の Lyness 写像の Id(s, t) を、正しさを Lean で証明した検査プログラムでも検査する。計算サーバーでその検査器が使えないときは「unavailable」と表示される。
保存した証明書は、ほかの人に渡して、同じように検査してもらうことができる。
証明書が示すこと、示さないこと
- 証明書が示すのは、「この入力について、この答えが成り立つ」ことである。入力が違えば、別の証明書が要る。
- 「前提」が付いた答えは、その条件のもとでの答えである。
- 「復元値」は、書かれた仮定（たとえば歩数の大きさの上界）のもとで一意に決まる値である。
- 「統計」は定理ではない。
- 「結果なし」には主張がなく、理由だけが書かれる。