Formal Mathematical Reasoning: A New Frontier in AI

要約

AI for Mathematics (AI4Math) は、知的に興味深いだけでなく、科学、工学などにおける AI を活用した発見にとっても重要です。
AI4Math に対する広範な取り組みは、NLP のテクニックを反映しており、特に、テキスト形式で注意深く厳選された数学データセットで大規模な言語モデルをトレーニングしています。
補完的ではありますが、あまり研究されていない手段として、正式な数学的推論は、推論の正しさを検証し、自動的なフィードバックを提供できる証明アシスタントなどの正式なシステムに基づいています。
このポジションペーパーでは、私たちは形式的な数学的推論を提唱し、それが AI4Math を次のレベルに進化させるために不可欠であると主張します。
近年、定理の証明や自動形式化などの中核的なタスクだけでなく、検証可能なコードの生成やハードウェア設計などの新たなアプリケーションを含む、形式的推論を実行するための AI の使用が着実に進歩しているのが見られます。
しかし、AI が数学を真に習得し、より広範な影響を与えるには、解決すべき重要な課題が残っています。
私たちは既存の進捗状況を要約し、未解決の課題について話し合い、将来の成功を測るための重要なマイルストーンを構想します。
正式な数学的推論の転換点にある今、私たちは研究コミュニティが団結してこの分野の変革的な進歩を推進するよう呼びかけます。

要約(オリジナル)

AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. Extensive efforts on AI4Math have mirrored techniques in NLP, in particular, training large language models on carefully curated math datasets in text form. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as proof assistants, which can verify the correctness of reasoning and provide automatic feedback. In this position paper, we advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level. In recent years, we have seen steady progress in using AI to perform formal reasoning, including core tasks such as theorem proving and autoformalization, as well as emerging applications such as verifiable generation of code and hardware designs. However, significant challenges remain to be solved for AI to truly master mathematics and achieve broader impact. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success. At this inflection point for formal mathematical reasoning, we call on the research community to come together to drive transformative advancements in this field.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google