Fugu-MT 論文翻訳(概要): Aristotle: IMO-level Automated Theorem Proving

論文の概要: Aristotle: IMO-level Automated Theorem Proving

arxiv url: http://arxiv.org/abs/2510.01346v2
Date: Fri, 10 Oct 2025 20:12:14 GMT
ステータス: 翻訳完了
システム内更新日: 2025-10-14 15:48:09.721131
Title: Aristotle: IMO-level Automated Theorem Proving
Title（参考訳）: Aristotle: IMOレベルの自動定理証明
Abstract要約: アリストテレス(Aristotle)は、公式な検証と非公式な推論を組み合わせたAIシステムである。 2025年の国際数学オリンピックにおいて、金と薬の同等のパフォーマンスを達成している。
参考スコア（独自算出の注目度）: 34.21499442790805
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. Our system demonstrates state-of-the-art performance with favorable scaling properties for automated theorem proving.
Abstract（参考訳）: 我々は,2025年の国際数学オリンピック問題において,公式な検証と非公式な推論を組み合わせたAIシステムであるAristotleを紹介した。アリストテレスは、リーン証明探索システム、レムマの生成と形式化を行う非公式推論システム、専用の幾何学解法という3つの主要なコンポーネントを統合している。本システムでは, 自動定理証明に好適なスケーリング特性を有する最先端性能を示す。

関連論文リスト

MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文参考訳（メタデータ） (2026-07-16T05:22:40Z)
ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。 ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文参考訳（メタデータ） (2026-06-09T06:50:15Z)
MMFormalizer: Multimodal Autoformalization in the Wild [79.24853896733154]
MMFormalizerは、適応グラウンドを現実の数学的および物理的ドメインのエンティティと統合することにより、テキスト以外の自動形式化を拡張する。 MMFormalizerを新しいベンチマークであるPhyX-AFで評価し,MathVerse,PhyX,Synthetic Geometry,Analytic Geometryから115個のキュレートされたサンプルを作成した。その結果, GPT-5 と Gemini-3-Pro が最も高いコンパイル精度と意味的精度が得られ, GPT-5 は物理的推論に優れていた。
論文参考訳（メタデータ） (2026-01-06T13:42:51Z)
Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions [129.877899436804]
本稿では、ニューラルネットワークに基づく推論に頼ることなく、CPU上で完全に動作する幾何定理証明の高効率な方法を提案する。 IMO(International Mathematical Olympiad)において,補助点を追加するための単純なランダム戦略により,銀・医療レベルの人的パフォーマンスが達成できることを示す。さらに,HAGeo-409という,人為的な難易度を持つ409の幾何学的問題からなるベンチマークを構築した。
論文参考訳（メタデータ） (2025-11-27T01:05:00Z)
Comparing Dialectical Systems: Contradiction and Counterexample in Belief Change (Extended Version) [0.0]
我々は、q-述語系がp-述語系よりも厳密に強力であることを示す。この結果は、自動信念修正における反例と矛盾の相補的な役割を強調している。
論文参考訳（メタデータ） (2025-07-09T12:35:20Z)
Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework [117.6508659085231]
本稿では論理完全推論フレームワークであるAristotleについて,論理解法,論理解法,論理解法,論理解法の3つの主要なコンポーネントを提案する。本フレームワークでは,記号表現と論理規則を総合的に推論プロセスに統合する。いくつかのデータセットの実験結果は、Aristotleが最先端の推論フレームワークを精度と効率の両方で一貫して上回っていることを示している。
論文参考訳（メタデータ） (2024-12-22T10:14:09Z)
Proposing and solving olympiad geometry with guided tree search [63.824930029019995]
木探索に基づくガイド付き問題解決を支援するユークリッド幾何学システムであるTongGeometryを紹介する。 TongGeometryは、補助的な構成を必要とする67億の幾何学定理を発見した。トンゲメトリーはIMO-AG-30ですべての国際数学オリンピック幾何学を解き、金メダリストを初めて上回った。
論文参考訳（メタデータ） (2024-12-14T04:20:47Z)
Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。自己形式化定理文の自動意味評価を行う。
論文参考訳（メタデータ） (2024-05-27T14:35:10Z)
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文参考訳（メタデータ） (2024-01-22T12:49:08Z)
A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文参考訳（メタデータ） (2023-06-29T18:35:41Z)
Lemmas: Generation, Selection, Application [2.0646127669654826]
本稿では,自動定理証明器に有用な補題を生成する学習技術を含む複合システムによる実験について述べる。凝縮分枝問題に焦点をあてることで、設定を大幅に単純化し、補題の本質と証明探索におけるそれらの役割を理解できるようになる。
論文参考訳（メタデータ） (2023-03-10T11:06:43Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文参考訳（メタデータ） (2020-09-07T19:50:10Z)
Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems [3.222802562733787]
我々は、特異な論理に容易に適応したり、新たな推論プロセスを統合するように設計された、自動定理のための新しいフレームワークMATRを提案する。我々はMATRの高レベル設計と実装の詳細について説明する。次に、G"odelの不完全性定理の証明に適した形式化されたメタロジックを記述し、MATRにおける我々のメタロジックを用いて、第一不完全性定理と第二不完全性定理の両方の証明を半自動生成する進捗について報告する。
論文参考訳（メタデータ） (2020-05-06T03:29:34Z)
Incompleteness for stably consistent formal systems [0.0]
まず、人間の実際の一貫性性を反映した安定な一貫性の数学的概念を部分的に展開する。次に、第1および第2のG"odel不完全性定理を安定に1,2$一貫性のある形式系に一般化する。
論文参考訳（メタデータ） (2020-01-21T15:04:15Z)

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