論文の概要: Aristotle: IMO-level Automated Theorem Proving
- arxiv url: http://arxiv.org/abs/2510.01346v1
- Date: Wed, 01 Oct 2025 18:21:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-03 16:59:20.816852
- Title: Aristotle: IMO-level Automated Theorem Proving
- Title（参考訳）: Aristotle: IMOレベルの自動定理証明
- Authors: Tudor Achim, Alex Best, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leister, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, Lawrence Wu,
- Abstract要約: アリストテレス(Aristotle)は、公式な検証と非公式な推論を組み合わせたAIシステムである。
2025年の国際数学オリンピックにおいて、金と薬の同等のパフォーマンスを達成している。
- 参考スコア（独自算出の注目度）: 26.6288413621226
- 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つの主要なコンポーネントを統合している。
本システムでは, 自動定理証明に好適なスケーリング特性を有する最先端性能を示す。
関連論文リスト
- 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。