ADIC
Advanced Data Integrity by Ledger of Computation
通過条件を固定し、第三者検証を可能にする計算証明基盤
An infrastructure for fixing AI and computational outputs in a third-party verifiable form
※ADICのコア技術は、Lean定理証明器による形式証明を経ています。
Note:The core technology of ADIC has been formally verified using the Lean theorem prover.
※ADICの革新は、AIの判断をあとから説明する技術ではなく、どの判断だけを通してよいかという条件そのものを事前に固定し、第三者が機械的に確かめられる形に変えたことにあります。
Note:The innovation of ADIC lies not in explaining AI decisions after the fact, but in fixing in advance the very conditions under which decisions are allowed to pass, and turning them into something a third party can verify mechanically.
なぜ ADICが必要か
Why ADIC is Necessary
AIや統計モデルが社会の判断に入り込むほど、後から説明するだけでは足りません。
ADICは、出力や判断を通してよい条件を事前に固定し、第三者が再検証できる形で証拠を残すために必要です。
As AI and statistical models increasingly shape real-world decisions, post-hoc explanation is no longer enough.
ADIC is needed to fix in advance the conditions under which outputs may proceed, and to leave evidence that third parties can independently verify.
なぜ ADIC はデジタル証明として強いのか
Why ADIC Is Strong as a Digital Certificate
1. 論理を整数演算として固定できるから
ADICは、証明や検証手順を有限個の整数演算として記述し、解釈ではなく計算として扱える形に固定します。
そのため、正しさの確認は文章の読み方ではなく、演算が一致するかどうかで判定できます。
2. 検証が決定的だから
ADICの検証は、同じ入力に対して同じ計算を行えば同じ結果になる決定的な構造を持ちます。
「たぶん正しい」ではなく、条件を満たすか満たさないかを機械的に判定できます。
3. 第三者が独立に再検証できるから
ADICの記録は、特定の運用者や権威を信じなくても、第三者が独立に再計算して確認できます。
信頼を承認者ではなく、再現可能な計算に置ける点が、ADICの強さです。
1. Because it fixes logic as integer computation
ADIC represents proofs and verification procedures as finite sequences of integer operations, turning them from matters of interpretation into matters of computation.
This allows correctness to be checked by whether the computation matches, not by how a text is read.
2. Because verification is deterministic
Given the same input, ADIC produces the same verification result through the same calculation.
It does not rely on “probably correct” judgment, but on whether predefined conditions are satisfied or not.
3. Because third parties can verify it independently
ADIC records can be rechecked independently by third parties without relying on the authority of the original operator.
Its strength lies in grounding trust in reproducible computation rather than in approval by a particular institution or person.
※本アプローチは、和算における手順主義と有限性の思想を現代的に拡張した「和算2.0」に思想的基盤を持ちます。
Note: This approach is grounded in “Wasan 2.0,” a modern extension of the procedural and finiteness principles found in traditional Japanese mathematics.
