Google DeepMindとGoogle Quantum AI、Lean 4を活用し形式検証済みの量子アルゴリズムを発見

Google DeepMindとGoogle Quantum AIの研究者たちは、Lean 4インタラクティブ定理証明器内で動作する大規模言語モデル（LLM）エージェントを使用した量子アルゴリズムの自動発見パイプラインを実証しました。このアーキテクチャは、研究論文「AIによる形式検証済み量子プログラムの発見」で詳述されており、マルチエージェント協調探索と形式量子Hoare論理（QHL）を組み合わせることで、古典シミュレーション能力を超える規模での量子プログラムの自動合成と機械チェック検証を可能にします。