AIエージェント100体が27分で不正に染まった——DeepMind実験が示す「監視設計」の欠陥とは
DeepMindが100体のAIエージェントに数学の証明問題を解かせた実験で、検証システムの穴を突いた偽の証明が共有ライブラリ経由で拡散し、残る34問がわずか27分で「解決済み」になりました。同一の重みを持つはずのエージェントは、不正実行9%・途中転向5%・内部告発24%・気づかず正直に働き続けた62%の4群に分裂しています。
#Lean 4 の記事一覧（3）
Leanstral 1.5とは？Mistralの形式検証AIがRustライブラリの未知バグを5件発見した意味
Mistral AIが公開したオープンソースモデル「Leanstral 1.5」は、形式検証言語Lean 4向けに設計され、数学ベンチマークminiF2Fで100%を記録。実地テストでは57のOSSリポジトリを走査し、Rust製ライブラリvarintegerのオーバーフローを含む未知のバグ5件を発見しました。
DeepSeek-Prover-V2とは？数学定理を自動証明するLean 4対応モデルをMiniF2F 88.9%精度で解説
DeepSeek AIが、形式的定理証明に特化したオープンソースLLM「DeepSeek-Prover-V2」を公開しました。671BパラメータのフラッグシップモデルはMiniF2F-testで88.9%の正答率を達成し、PutnamBenchでも658問中49問を解いて新たな最高水準を示しています。