論文の概要: 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の球充填問題
- Authors: Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska,
- 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による検証の最終段階が実施された。
このマイルストーンを達成するために使用される技術について議論し、人間とガウスの独特なコラボレーションを反映し、残るプロジェクトの目的について議論する。
関連論文リスト
- Openpi Comet: Competition Solution For 2025 BEHAVIOR Challenge [54.28288180330569]
2025 BEHAVIOR Challengeは、シミュレーション環境での物理エージェントによる長期タスクの解決に向けた進捗を厳格に追跡するように設計されている。
本報告では,2025 BEHAVIOR チャレンジを2位に近づき,残りの提案を著しく上回っている。
論文 参考訳（メタデータ） (2025-12-10T20:46:40Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。