論文の概要: A Milestone in Formalization: The Sphere Packing Problem in Dimension 8
- arxiv url: http://arxiv.org/abs/2604.23468v2
- Date: Tue, 28 Apr 2026 16:27:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-29 14:06:43.829085
- Title: A Milestone in Formalization: The Sphere Packing Problem in Dimension 8
- Title（参考訳）: 形式化のマイルストーン:次元8の球充填問題
- Abstract要約: 2024年3月、ハリハランとヴィアゾフスカは、この解とその関連する数学的事実をLean Theorem Proverで公式化するプロジェクトを立ち上げた。
2026年2月に重要なマイルストーンが達成され、結果が正式に検証され、Math, Inc.のオートフォーマライゼーションモデル「Gauss」による検証の最終段階が実施された。
このマイルストーンを達成するために使用される技術について議論し、人間とガウスの独特なコラボレーションを反映し、残るプロジェクトの目的について議論する。
- 参考スコア（独自算出の注目度）: 0.785690292052871
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.
- Abstract（参考訳）: 2016年、ヴィアゾフスカは、2003年にコーンとエルキースによって決定された最適条件を満たす「魔法の」関数を構築するためにモジュラー形式を用いて、次元8$で球充填問題を解いたことで有名である。
2024年3月、ハリハランとヴィアゾフスカは、この解とその関連する数学的事実をLean Theorem Proverで公式化するプロジェクトを立ち上げた。
2026年2月に重要なマイルストーンが達成され、結果が正式に検証され、Math, Inc.のオートフォーマル化モデルであるGaussによる検証の最終段階が実施された。
このマイルストーンを達成するために使用される技術について議論し、人間とガウスの独特なコラボレーションを反映し、残るプロジェクトの目的について議論する。
関連論文リスト
- A Reponse to the Sheldon Goldstein Objection to a Series of Covariant Relativistic Bohmian Models [0.0]
我々は、Covariant Bohmian Models type Nikoli と Hernndez-Zapata に対する非常に重要な反論に答えようとしている。
N の時空構成密度が有限積分であることを示すことは非常に有益である。
論文 参考訳（メタデータ） (2026-07-18T18:45:42Z) - On the Wasserstein Gradient Flow Interpretation of Drifting Models [82.3193475501435]
最近、Deng et al. (2026) は、生成タスクのための新しいフレームワークである、Drifting (GMD) による生成モデリングを提案した。
本稿では、WGF(Wasserstein Gradient Flows)のレンズによるGMDの分析、すなわち確率測度空間における関数の最も急降下経路について述べる。
論文 参考訳（メタデータ） (2026-05-06T16:48:46Z) - Munkres' General Topology Autoformalized in Isabelle/HOL [2.5899040911480182]
我々は,85,000行以上のIsabelle/HOLコードを生成するLDM支援オートフォーマル化実験について述べる。
形式化は完備であり、806の形式的な結果はすべて、ゼロ・ノウハウで完全に証明される。
得られた形式化を詳細に分析し,セッションログから人間-LLM相互作用パターンを分析し,関連する自己形式化の取り組みと比較した。
論文 参考訳（メタデータ） (2026-04-08T18:00:36Z) - Openpi Comet: Competition Solution For 2025 BEHAVIOR Challenge [54.28288180330569]
2025 BEHAVIOR Challengeは、シミュレーション環境での物理エージェントによる長期タスクの解決に向けた進捗を厳格に追跡するように設計されている。
本報告では,2025 BEHAVIOR チャレンジを2位に近づき,残りの提案を著しく上回っている。
論文 参考訳（メタデータ） (2025-12-10T20:46:40Z) - Geometrically-Constrained Agent for Spatial Reasoning [53.93718394870856]
視覚言語モデルは空間的推論において基本的な意味-幾何学的ギャップを示す。
現在のパラダイムは、このギャップを埋めることに失敗します。
本稿では,形式的タスク制約を導入することにより,このギャップを解消する学習自由エージェントパラダイムを提案する。
論文 参考訳（メタデータ） (2025-11-27T17:50:37Z) - Finding Kissing Numbers with Game-theoretic Reinforcement Learning [34.01788794245267]
我々は,高次元空間を効率的に探索するゲーム理論強化学習システムであるPackingStarを訓練する。
PackingStarは以前の設定を再現し、25から31の次元から既知のすべてのレコードを上回ります。
14次元やその他の次元で6000以上の新しい構造が発見された。
論文 参考訳（メタデータ） (2025-11-17T14:02:00Z) - Large Language Models Imitate Logical Reasoning, but at what Cost? [0.42970700836450487]
本稿では,18カ月間のフロンティア大言語モデルの推論能力を評価する。
我々は,2023年12月,2024年9月,2025年6月の3つの主要モデルの精度を,真偽の質問に対して測定した。
2023年から2024年までのパフォーマンス向上は、シークレットの隠された連鎖によるものである。
論文 参考訳（メタデータ） (2025-09-16T04:03:42Z) - Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。
低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。
提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
論文 参考訳（メタデータ） (2025-07-07T22:38:49Z) - Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。
創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか?
本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。
ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
論文 参考訳（メタデータ） (2025-05-24T03:52:25Z) - Self-supervised Shape Completion via Involution and Implicit Correspondences [89.18705005095359]
3次元形状の完成は、教師付きトレーニングや、完全な形状の例による分布学習によって伝統的に解決される。
近年, 完全な3次元形状の例を必要としない自己指導型学習手法が注目されている。
形状完遂作業のための非対角的自己教師型手法を提案する。
論文 参考訳（メタデータ） (2024-09-24T10:04:38Z) - Llemma: An Open Language Model For Mathematics [46.557804525919785]
数学のための大きな言語モデルであるLlemmaを紹介します。
MATHベンチマークでは、Llemmaはすべての既知のオープンベースモデルより優れている。
レムマは道具の使用と公式な定理を証明することができるが、それ以上の微調整は行わない。
論文 参考訳（メタデータ） (2023-10-16T17:54:07Z) - Bayesian Quadrature on Riemannian Data Manifolds [79.71142807798284]
データに固有の非線形幾何学構造をモデル化する原則的な方法が提供される。
しかし、これらの演算は通常計算的に要求される。
特に、正規法則上の積分を数値計算するためにベイズ二次(bq)に焦点を当てる。
先行知識と活発な探索手法を両立させることで,BQは必要な評価回数を大幅に削減できることを示す。
論文 参考訳（メタデータ） (2021-02-12T17:38:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。