上海人工智能研究所の青年科学者・付杰率いるVeri-Codeチームが、AIが生成するプログラムの信頼性を自動検証する新手法を提案した。この研究は、AIによるソフトウェア開発が核電所制御系や自動運転システムなど安全に直結する分野に進出する中で、現行のテストベース検証の限界を克服するものだ。現在のAIシステムは、人間が作成したテストケースに依存しており、複雑なコードではテストケースの数が指数的に増加し、すべての実行経路を網羅できない。また、人間の判断に依存するため、誤った検証結果や論理的抜け漏れが生じるリスクがある。 付杰チームは、形式化言語Dafnyを用いて、AIが生成したコードの正しさを数学的定理レベルで検証するアプローチを構築。強化学習を活用し、人間の先験知識（例：長文の思考過程CoT）に依存せず、AIが自ら形式的仕様を生成・検証する能力を育成。この方法により、AIが生成したコードがユーザーの意図に完全に合致しているかを、客観的かつ自動的に評価できる。特に、Dafnyのコード構造は数学的論理と密接に結びついており、検証の探索空間が小さく、複雑度とコード行数が線形に比例するため、段階的学習（Curriculum Learning）が可能。これにより、単一の断言から複数モジュールの組み合わせまで、段階的に能力を拡張できる。 研究チームは、既存のPythonコードをDafnyに自動変換するパイプラインを構築し、学習データを生成。さらに、生成された仕様の質を評価する新たな指標「規格優越率（SSR）」を導入。これは、生成された仕様が元の正解より入力制約を緩く、出力の記述をより厳密にしているかを測定するもので、強化学習の報酬信号として有効に活用された。実験結果では、14B規模のモデルが、GPT-4oやClaude4など閉鎖型モデルを上回る検証通過率とSSRを達成。 付杰氏は「AIが生成するコードの正しさを、人間の主観ではなく数学的証明で保証する。これにより、医療、金融、自動運転、OSなど安全が求められる分野で、AIの信頼性を根本から高められる」と述べ、今後の目標として、数千行規模のコードに対応する拡張と、AIが自ら思考過程（CoT）を学習する仕組みの開発を掲げる。本研究の論文はarXivに掲載され、コード・データはオープンソースで公開されている。