人工知能・形式手法・数学的推論（AIMing）

「人工知能・形式手法・数学的推論」（AIMing）プログラムは、革新的な計算技術と人工知能（AI）技術、および数学的推論における新たな戦略や技術が交差する領域の研究を支援し、知識発見の自動化を目指している。数学的推論は人間の知能の中核をなす能力であり、知識発見において重要な役割を果たす。過去数十年にわたり、数学と計算機科学の両コミュニティが、予想・証明・検証を含む機械支援による数学的推論の研究に貢献してきた。そのアプローチは、形式手法や対話型定理証明器を用いるものから、人工知能の技術を活用するものまで多岐にわたる。近年の技術的進歩により、数理科学・形式手法・AIの各コミュニティの間で、機械支援による数学的推論への関心が急速に高まっている。こうした進展は、AI研究そのものにも影響を与える可能性を秘めている。