AIが形式化検証を再興

人工知能のプログラム大量生成で、形式化検証が再注目されている。10月26日、アクシオム・マスは数十のエージェントを指揮し、数学史上最大の証明を24日で4310万行のリーンコードへ変換した。グーグルは新コードの約75％が人工知能生成と公表。アンスロピックでは内部コードの80％超をクロードが書いた。コードラビットは人工知能関与の修正で欠陥が人力1.7倍と報告し、機械検証需要が急増した。 形式化検証は仕様を数学命題化し、リーンやロックで機械検査する。スタンフォード大は暗号庫で人力5人8月を、上位仕様を与えた人工知能が11.4時間、約467ドルに短縮したと報告。アンスロピックとシアラムは123ライブラリで1.8億行証明を生成し、数百欠陥を修正。ハーモニックは10月27日からプログラムとチップ検証へ展開し、テンソルダインで深い欠陥を検出した。 資金調達も加速。アクシオム評価16億ドル超、ハーモニック14.5億ドル、アンドトゥルー7000万ドル、プラマーナ2700万ドル。中国でもリーン定理証明モデルが増え、北京大学が長期未解決の代数問題をリーンで検証可能な証明に変換した。ただし検証は仕様の誤りは防げず、人工知能が仕様と証明を同時生成する循環がリスク。仕様と標準のガバナンス、独立性が課題だ。