LLMsはロボットの経路計画の最適性を証明できるか？研究レベルのアルゴリズム検証のためのベンチマーク

要旨: ロボティックな経路計画問題はしばしばNP困難であり、実用的な解法は一般ケースに対して証明可能な性能保証を伴う近似アルゴリズムに通常依存します。そうしたアルゴリズムを設計することは困難ですが、それらの近似最適性を形式的に証明することはさらに要求が高く、領域特有の幾何学的洞察と複雑な運用制約の下での多段階の数学的推論を必要とします。最近の大規模言語モデル（LLMs）は数学的推論のベンチマークで高い性能を示していますが、ロボット経路計画における研究レベルの最適性証明を支援する能力はまだ十分には検証されていません。本研究では、ロボット経路計画アルゴリズムの近似比証明を評価するためのLLMsの初のベンチマークを導入します。ベンチマークは、多様な計画問題タイプと複雑さのレベルを横断する34件の研究レベルの証明タスクで構成され、各タスクはアルゴリズムの記述、問題制約、および理論的保証を踏まえた体系的な推論を要求します。最先端の商用・オープンソースのLLMsの評価結果は、最も強力なモデルであっても外部のドメイン知識なしには完全に有効な証明を生成するのが難しいことを示しています。しかし、タスク固有の文脈内補題をLLMsに提供することは推論品質を大幅に向上させ、汎用的なチェーン・オブ・思考を促すプロンプティングや事後知識として真の近似比を供給することよりも効果的な要因です。さらに、一般的な論理的欠陥と幻覚を特徴づける細かな誤り分析を提供し、それぞれの誤りタイプをターゲットを絞った文脈拡張によってどのように緩和できるかを示します。