証明付き進化：ブラックボックス探索とホワイトボックス検証

- 言語モデル(LM)が設計段階で制御器とその証明書(certificate)を提案し、証明書検査に通った候補のみを返す枠組み「proof-carrying evolution (PCE)」の研究。 - 数学的形式は固定で、提案者は数値パラメータを選ぶ。 - 成果物は制御則とその証明書であり、LMは設計時にのみ使用される。 - docking under a speed limit、maneuvering targetの追跡、SO(3)上のattitude controlの3課題で評価。

- 4つのLMを古典的search/synthesisと比較し、提案回数を揃えたpaired runsで評価。 - 線形問題では最強のモデルが標準的な古典baselineを全runで上回った。 - ただし同一目的関数に対し証明書を選ぶ古典optimizerがその差の大半を埋める。 - SO(3)ではCMA-ESに混合した場合、検出可能な優位性はどのモデルにもなかった。 - 全search中央値はhand-tuned lawを下回る。

- 探索が制御器と証明書を同時に提案し、証明書検査が選択を導く。 - 線形問題では探索中にexact rational arithmeticで証明書を検査。 - SO(3)では浮動小数点で検査し、報告されたchampionは全てexactに再検証。 - 各手法の最良runにはLean 4による制御性質の証明を付与。 - docking制御では目的関数とmutation operatorを固定し、certified候補の保持則の有無を比較。

- docking under a speed limit、maneuvering targetの追跡、SO(3)上のattitude controlの3課題で検証。 - paired runsと共有されたproposal allowancesを用いて4つのLMと古典手法を比較。 - 線形問題はexact rational arithmetic、SO(3)は浮動小数点検査後にexact re-verification。 - 最良runにLean 4証明を付与。 - certified候補を保持する則を外すと新規certified設計が得られないことをdocking制御で確認。

- 線形問題でのLMの優位は、証明書を選ぶ古典optimizerで大半が説明される。 - 引用されたpursuit championsの順位はEulerからzero-order-hold dynamicsへの変更で維持されない。 - SO(3)では混合時にCMA-ESを検出可能に上回るモデルはない。 - 全提案をモデルが書く場合、一方はCMA-ESを上回るが他方は混合変種より悪化。 - 全search中央値はhand-tuned law未満であり、実用上の限界が議論される。

- CMA-ES(SO(3)での比較対象)。 - Lean 4による証明支援。 - exact rational arithmeticおよびzero-order-hold dynamicsに関する制御/検証研究。 - 要旨で参照/比較されている個別論文は明示されていないため、上記の関連手法・ツールを次に読む候補とする。