記号・代数計算による最適化問題解法と定理自動証明の研究

点击翻译按钮获取中文摘要

最適化問題に対する新しいアプローチである記号・代数計算を用いたパラメータを含んだまま正確に解く方法の確立を目指し、(1)ベースとなる記号・代数計算理論とその技術の展開と(2)成功事例の発掘とそのためのアルゴルズムの改良と支援ツール構築を行った。(1)では、上位レベルである限定子除去法、パラメータ付きの多項式イデアル操作、パラメータ無しの多項式イデアル操作、に分け、最下層のパラメータ無し多項式イデアル操作については、正標数の場合の素イデアル分解アルゴリズムの更なる改良とその計算機上の実装を行い、正標数での問題の克服と計算の効率化に成功した。次のレベルであるパラメータ付きの多項式イデアル操作については、海外共同研究者Weipsfenning教授との研究討論を通じ、指数部分にパラメータを持つ場合を世界に先駆けて取り扱い、0次元の場合において、零点の周期性や有限性を発見し、その計算法を得た。この成果は、preprintとし、国際会議に投稿中である。さらに、係数にパラメータを含む場合についての一般的な解法についてもComprehensive Groebner basis計算法の拡張として考え、研究を進めている。(2)では、研究分担者の穴井と定期的にセミナーおよび研究討論を行い、実際の制御計算への限定子除去法の適用を検討してきた。穴井は独自の支援計算ツールSyNRACの構築を開始し、計算機実験を行った。また、記号・代数計算の啓蒙活動として、グレブナー計算に関する書籍を東京大学出版会より出版し、さらに限定子除去法に関する啓蒙書を準備している。また、研究分担者の鈴木は定理自動証明に関して、より一般的な枠組である「数学知識データの数学研究・教育への活用」の中で、計算機上での実現のためのフォーミュレーションを開始した。今後、代表者と穴井は、原教授(東京大学)と共同で、萌芽研究での成果を集約し、この経験をベースに、新たなシミュレーション技術の開発と実際のシステムを構築計画を立て、科学技術振興機構・戦略的創造研究推進事業「シミュレーション技術の革新と実用化基盤の構築」の中の「数値/数式ハイブリッド計算に基づくロバスト最適化プラットフォームの構築」として発展させることになった。