論文の概要: Formal Mathematical Reasoning: A New Frontier in AI

• arxiv url: http://arxiv.org/abs/2412.16075v1
• Date: Fri, 20 Dec 2024 17:19:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-23 16:21:06.437241
• Title: Formal Mathematical Reasoning: A New Frontier in AI
• Title（参考訳）: フォーマルな数学的推論 - AIの新しいフロンティア
• Authors: Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song,
• Abstract要約: 我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
• 参考スコア（独自算出の注目度）: 60.26950681543385
• License:
• Abstract: 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.
• Abstract（参考訳）: AI for Mathematics(AI4Math)は、知的なだけでなく、科学、工学などにおけるAI駆動の発見にも欠かせない存在だ。 AI4Mathに対する大規模な取り組みは、特にテキスト形式で慎重にキュレートされた数学データセット上で、大きな言語モデルをトレーニングするNLPのテクニックを反映している。 補足的かつ探求の少ない方法として、公式な数学的推論は証明アシスタントのような形式的なシステムに基礎を置いており、推論の正しさを検証し、自動的なフィードバックを提供することができる。 本稿では,形式的数学的推論を提唱し,AI4Mathを次のレベルに進めることは不可欠であると主張する。 近年、定理証明や自己形式化といったコアタスクや、検証可能なコード生成やハードウェア設計などの新興アプリケーションなど、AIによる形式推論の実施が着実に進んでいることが分かっています。 しかし、AIが真に数学をマスターし、より大きなインパクトを達成するためには、大きな課題が解決される必要がある。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。 フォーマルな数学的推論のためのこの転換点において、我々は研究コミュニティにこの分野での変革的進歩を推進するよう呼びかける。

関連論文リスト

• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。 目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
  論文  参考訳（メタデータ） (2024-09-09T18:21:28Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。 このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。 興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
  論文  参考訳（メタデータ） (2024-03-07T15:12:06Z)
• AI for Mathematics: A Cognitive Science Perspective [86.02346372284292]
  数学は人間によって開発された最も強力な概念体系の1つである。 AIの急速な進歩、特に大規模言語モデル(LLM)の進歩による推進により、そのようなシステム構築に対する新たな、広範な関心が生まれている。
  論文  参考訳（メタデータ） (2023-10-19T02:00:31Z)
• Mathematics, word problems, common sense, and artificial intelligence [0.0]
  本稿では,基本知識とコモンセンス推論を組み合わせた単語問題の解法として,現在の人工知能(AI)技術の能力と限界について論じる。 我々は、AI自然言語技術を用いて開発されている3つのアプローチについてレビューする。 純粋な数学的研究のためのAI技術を開発する上で、このような制限が重要であるかどうかは明らかではない、と我々は主張する。
  論文  参考訳（メタデータ） (2023-01-23T21:21:39Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding [74.12405417718054]
  本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。 他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。 基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
  論文  参考訳（メタデータ） (2022-06-13T17:03:52Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。