論文の概要: Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generation

• arxiv url: http://arxiv.org/abs/2606.10806v1
• Date: Tue, 09 Jun 2026 12:50:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-10 15:40:58.50516
• Title: Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generation
• Title（参考訳）: マンシャイン(Moonshine) - 概念生成を専門とする自律的な数学研究エージェント
• Authors: Xiaoyang Chen, Xiang Jiang,
• Abstract要約: ムーンシャイン(Moonshine)は、数学的な予想を生成することを目的とする自律エージェントである。 この記事では、ムーンシャインによるヤコビアン予想の探索を例に挙げる。
• 参考スコア（独自算出の注目度）: 5.836029794016965
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Moonshine is an autonomous agent whose central objective is to generate mathematical conjectures. Its core capability is to extract structure from classical problems, distill new concepts, and formulate conjectures of mathematical significance. Rather than treating the solution of a single proposition as its endpoint, Moonshine builds an extensible theoretical framework through conjecture generation, bridge building, and obstacle identification. This article uses Moonshine's exploration of the Jacobian conjecture as an example. It shows how the central logic of whether local nondegeneracy can force global injectivity is transferred to one-hidden-layer affine-ridge sigmoid networks. This leads to the formulation of the \emph{Neural Jacobian Conjecture} (NJC): if such a network has strictly positive Jacobian determinant on the whole space, then it must be globally injective. By invoking GPT-5.5-pro and DeepSeek-V4-pro separately, Moonshine obtained independent complete proofs for the case \(N=n+1\). In addition, with the assistance of ChatGPT through interactive use of its web interface with GPT-5.5-pro, a geometric-topological proof was developed. These results provide preliminary evidence for the plausibility of the conjecture. The general higher-width case \(N\ge n+2\), however, remains unresolved and is left for further investigation. This work illustrates Moonshine's ability to autonomously generate meaningful mathematical problems and make rigorous progress on them.
• Abstract（参考訳）: ムーンシャイン(Moonshine)は、数学的な予想を生成することを目的とする自律エージェントである。 その中心となる能力は、古典的な問題から構造を抽出し、新しい概念を蒸留し、数学的意義の予想を定式化することである。 一つの命題の解を終点として扱うのではなく、ムーンシャインは予想生成、橋梁構築、障害物識別を通じて拡張可能な理論的枠組みを構築する。 この記事では、ムーンシャインによるヤコビアン予想の探索を例に挙げる。 このことは、局所的非退化が大域的インジェクティビティを強制するかどうかの中心的論理が、一重層アフィンリッジシグモイドネットワークに伝達されることを示す。 このことは \emph{Neural Jacobian Conjecture} (NJC) の定式化につながります。 GPT-5.5-pro と DeepSeek-V4-pro を別々に呼び出すことで、ムーンシャインはケース \(N=n+1\) に対して独立した完全証明を得た。 さらに、WebインターフェースをGPT-5.5-proでインタラクティブに使用することでChatGPTの助けを借り、幾何学的トポロジカルな証明が開発された。 これらの結果は、予想の妥当性に関する予備的な証拠を与える。 しかし、一般的な高幅の場合 \(N\ge n+2\) は未解決のままであり、さらなる研究のために残されている。 この研究は、ムーンシャインが有意義な数学的問題を自律的に生成し、それらを厳格に前進させる能力を示している。

関連論文リスト

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• Mathematics with large language models as provers and verifiers [1.1029146548022293]
  ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
  論文  参考訳（メタデータ） (2025-10-11T20:35:25Z)
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。 制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
  論文  参考訳（メタデータ） (2024-06-30T13:34:54Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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