言語モデルを使う制御器設計手法「PCE」、証明書付き候補で探索を選別

何が起きたか

arXiv論文「Proof-Carrying Evolution: Black-Box Search, White-Box Flight」は2026年10月30日、言語モデルを制御器の設計時に使う「proof-carrying evolution（PCE）」を検証した。ドッキング、操縦する標的の追跡、SO(3)上の姿勢制御の3課題で、4つの言語モデルを古典的な探索・合成手法と比較した。線形課題では一部の言語モデルが標準的な古典手法を上回った一方、証明書選択を取り入れた古典的最適化がその差の大半を縮めた。

詳細

PCEでは、探索側が制御器と証明書を提案する。制御器の数学的形式は固定し、提案者が数値パラメーターを選ぶ。証明書の検査結果を候補選択に使い、認証された候補だけを返す設計で、運用時に使う成果物は制御則とその証明書である。言語モデルは設計時だけ使う。 比較は同じ提案回数の上限を設けたペア実行で行った。線形課題では探索中に有理数の厳密演算で証明書を検査し、SO(3)では浮動小数点で探索した後、報告する最良候補を厳密に再検証した。各手法の最良候補には、制御特性を示すLean 4の証明も与えた。追跡課題では、引用された最良候補の順位がEuler法からゼロ次ホールドの力学モデルへの変更後に維持されなかった。SO(3)では、古典的な突然変異と組み合わせた場合、言語モデルがCMA-ESを明確に上回る結果は確認されなかった。

Key Facts

本紙の見方

この研究の中心は、言語モデルが制御則を直接書くことではなく、証明書を候補選別の基準に組み込み、認証済みの制御則を探索の成果物にする点にある。制御器の数式形式は固定し、数値パラメーターを探索するため、自由な設計提案と検証可能性の折り合いを、探索の枠組み自体でつけようとしている。言語モデルの出力をそのまま運用する構成ではない。 比較結果は「言語モデル対古典手法」という単純な勝敗に還元できない。線形課題では強いモデルが標準的な古典ベースラインを全実行で上回ったが、同じ目的に対して証明書を選ぶ古典的最適化が差の大半を縮めた。つまり、結果を左右するのは提案器の種類だけでなく、証明書をどう選び、探索に反映するかでもある。ドッキングで認証候補を残す条件では全実行で新たな認証設計が得られ、保持規則を外すと得られなかったという比較も、認証を探索後の検査にとどめない設計の意味を示す。 一方、課題をまたいだ性能の一般化には限界がある。追跡課題では、Euler法での順位がゼロ次ホールドの力学モデルに変えると維持されなかった。SO(3)では、古典的突然変異との併用でモデルがCMA-ESを明確に上回らず、モデルが全提案を担う条件でも、試したモデルの一方はCMA-ESを上回り、もう一方は混合方式より悪かった。探索中央値はいずれも手調整則を下回ったとされる。特定のモデルや探索条件での成績を、制御課題一般の優位性と読み替えることはできない。 検証方法にも課題間の差がある。線形問題では探索中から有理数の厳密演算を使ったが、SO(3)では浮動小数点で探索し、報告候補を後から厳密に再検証している。さらに、追跡課題の順位変化は、力学モデルの離散化の違いが候補評価に関わることを示す。したがって、証明書があることだけで、モデル変更後の性能や実環境での安全性まで確認されたとはいえない。次に確認すべきなのは、異なる力学モデルや条件での再現性、証明対象となる制御特性の範囲、実機での検証である。論文要旨はこれらの実機評価や適用範囲を示していない。

なぜ重要か

PCEは、言語モデルが設計した制御器をそのまま使うのではなく、証明書の検査を探索中の選別に使い、認証済みの制御則と証明書を成果物にする。論文のドッキング課題では、認証候補を保持する条件と外す条件で結果が異なっており、制御器探索の仕組みに証明可能性を組み込む設計が、候補の獲得に関係することを示している。