論文の概要: At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier

• arxiv url: http://arxiv.org/abs/2610.22603v2
• Date: Mon, 19 Oct 2026 11:28:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-21 06:32:45.326577
• Title: At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier
• Title（参考訳）: 計算可能性の限界: ベイビービーバーフロンティアにおける自律的なAI発見に向けてのステップ
• Abstract要約: 我々は、チューリングマシンの加速度を自動的に検出するジェミニベースのエージェントパイプラインを提案する。 我々のシステムは、パターン認識、自動推論、非公式な数学的推論、そしてリーンで証明される公式な定理を統合する。
• 参考スコア（独自算出の注目度）: 12.326543568808098
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recent breakthroughs in AI for mathematics---ranging from Olympiad medal performances to resolving long-standing open conjectures---have rapidly expanded what automated systems can achieve. Yet these successes primarily concern predefined, human-formulated problems, leaving open how AI systems can autonomously uncover mathematical structure and formulate new questions. To push beyond static challenges, we explore the Busy Beaver (BB) domain, an uncomputable frontier that is fundamentally open-ended. Because no algorithm can compute the Busy Beaver number $\mathrm{BB}(n)$ for every $n$, this domain provides a natural setting for sustained exploration through mathematical conjecture and proof. In this paper, we introduce a Gemini-based agentic pipeline that automatically discovers accelerations of Turing machines, expressed as compact mathematical rules summarizing many execution steps. Our system integrates pattern recognition, automated conjecturing, informal mathematical reasoning, and formal theorem proving in Lean. With this framework, our system autonomously discovered and formally verified novel Collatz-like accelerations for eleven machines in $\mathrm{BB}(6)$. Subject to community acceptance, we provisionally classify these machines as Cryptids, namely machines whose blank-tape executions admit exact, compact mathematical descriptions but whose halting behavior remains unresolved. These results advance the analysis of $\mathrm{BB}(6)$ holdouts on the Busy Beaver frontier and demonstrate the potential of autonomous AI systems for open-ended mathematical discovery in fundamental computer science.
• Abstract（参考訳）: 数学におけるAIの最近のブレークスルー - オリンピアードのメダルパフォーマンスから長年続くオープンな予想の解決まで - は、自動化システムが達成できることを急速に拡大した。 しかし、これらの成功は主に、事前に定義された人為的な問題に関心を持ち、AIシステムが数学的構造を自律的に発見し、新しい質問を定式化する方法をオープンにしておく。 静的な課題を超えて、基本的にオープンな計算不可能なフロンティアであるBusy Beaver(BB)ドメインを探索する。 任意の$n$に対して、Busy Beaver number $\mathrm{BB}(n)$を計算できないので、この領域は数学的予想と証明を通じて持続的な探索の自然な設定を提供する。 本稿では,多数の実行ステップを要約したコンパクトな数学的ルールとして表現されたチューリングマシンの加速度を自動的に検出するジェミニベースのエージェントパイプラインを提案する。 我々のシステムは、パターン認識、自動推論、非公式な数学的推論、そしてリーンで証明される公式な定理を統合する。 この枠組みにより、我々のシステムは11台のマシンに対して、自動でコラッツ様の加速度を検定し、正式に検証した。 コミュニティが受け入れられる中で、我々はこれらの機械をCryptidsと仮に分類する。つまり、空白テープの実行には正確なコンパクトな数学的記述があるが、停止動作は未解決のままである。 これらの結果は、Busy Beaverフロンティアにおける$\mathrm{BB}(6)$ホールドアウトの分析を進め、基礎計算機科学におけるオープンエンドな数学的発見のための自律型AIシステムの可能性を実証している。

関連論文リスト

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
  論文  参考訳（メタデータ） (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。 この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
  論文  参考訳（メタデータ） (2026-07-08T17:46:36Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。 具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。 我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
  論文  参考訳（メタデータ） (2026-02-10T18:50:15Z)
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
  本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。 本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。 我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
  論文  参考訳（メタデータ） (2025-08-21T14:15:40Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• Algorithm-assisted discovery of an intrinsic order among mathematical constants [3.7689882895317037]
  基礎数学的定数に対する連続的な分数式を前例のない数で発見するコンピュータアルゴリズムを開発した。 多数の公式は、保守行列場と呼ばれる新しい数学的構造を明らかにする。 そのような行列場は数千の既存の公式を統一し、無限に多くの新しい公式を生成し、異なる数学的定数間の予期せぬ関係をもたらす。
  論文  参考訳（メタデータ） (2023-08-22T23:27:47Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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