論文の概要: Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
- arxiv url: http://arxiv.org/abs/2610.40551v1
- Date: Thu, 29 Oct 2026 17:39:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-01 01:32:10.126319
- Title: Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
- Title（参考訳）: Ramanujan Challengeの結果: 複数形式の証明のためのAI支援評価パイプライン
- Abstract要約: 我々は、異なるAIモデル、コンピュータ代数システム(CAS)、およびラマヌジャンチャレンジにおけるフォーマルツールの相対的な成功を分析した。
我々は、概念的には公式な解とは異なる正しい命題と、公表された開予想の一つの証明を見つける。
我々は、自然言語証明、CASコード、そして意味論的および論理的正当性を評価するリーン形式化のためのAI支援評価パイプラインを導入する。
- 参考スコア（独自算出の注目度）: 2.460905080745209
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: As AI's mathematical capabilities rapidly improve, meaningful benchmarks are shifting from university-level problems and math olympiads to research-level mathematics. The Ramanujan Challenge is a benchmark comprised of research-level problems in number theory, including unpublished results and open conjectures. It presented concrete formulas for mathematical constants whose correctness can be checked numerically, while their proofs may require non-obvious mathematics. Here, we analyze the Challenge submissions, measuring the relative success of different AI models, Computer Algebra Systems (CAS), and formal tools. We find correct submissions that are conceptually distinct from the official solutions, and a proof of one of the published open conjectures. Evaluating the submissions exposed a second challenge: judging complex proofs reliably at scale. We introduce an AI-assisted evaluation pipeline for natural language proofs, CAS code, and Lean formalizations that assesses semantic and logical correctness. Compared with the conventional one-shot LLM judgment, our pipeline reduces false-positive verdicts on natural language proofs from 23% to 6% and improves judgment accuracy on supporting code from 46% to 58%. This approach provides a methodology for evaluating research-level mathematics at scale, with potential applications across mathematics and AI for science.
- Abstract（参考訳）: AIの数学的能力が急速に向上するにつれて、有意義なベンチマークは大学レベルの問題や数学のオリンピックから研究レベルの数学へとシフトしつつある。
ラマヌジャン・チャレンジ(Ramanujan Challenge)は、数論における研究レベルの問題からなるベンチマークである。
数値的に正当性を確認することができる数学的定数に関する具体的な公式を提示し、それらの証明は不可避な数学を必要とするかもしれない。
ここでは、さまざまなAIモデル、コンピュータ代数システム(CAS)、フォーマルツールの相対的な成功を評価する。
我々は、概念的には公式な解とは異なる正しい命題と、公表された開予想の一つの証明を見つける。
提出品の評価は2つ目の課題を露呈した: 複雑な証明を大規模に確実に判断する。
我々は、自然言語証明、CASコード、そして意味論的および論理的正当性を評価するリーン形式化のためのAI支援評価パイプラインを導入する。
従来の一発LPM判定と比較すると,自然言語証明の偽陽性判定を23%から6%に減らし,サポートコードの判定精度を46%から58%に改善する。
このアプローチは、研究レベルの数学を大規模に評価するための方法論を提供する。
関連論文リスト
- MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
MathAdvは、学部および大学院レベルの数学で13のドメインにまたがる診断ベンチマークである。
本稿では, 定理証明精度が不明瞭であるモデル機能と故障モードを, コンポーネント単位で評価することで明らかにする方法について述べる。
論文 参考訳（メタデータ） (2026-08-26T07:12:54Z) - MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - 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) - HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification [54.06301039725887]
計算および応用数学において8つの領域にまたがる100以上の未解決問題のベンチマークであるHorizonMathを紹介する。
我々のベンチマークは、発見が困難であり、意味のある数学的洞察を必要とする問題のクラスをターゲットにしているが、検証は計算的に効率的で簡単なものである。
論文 参考訳（メタデータ） (2026-03-16T17:59:53Z) - Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。
本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。
我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
論文 参考訳（メタデータ） (2025-08-21T14:15:40Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。
既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
論文 参考訳（メタデータ） (2024-12-20T17:19:24Z) - Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
本稿では,Large Language Models (LLMs) を用いて,形式的証明ステップと完全形式的証明を生成する。
目標は、AIをどのように活用して数学的形式化プロセスを支援し、パフォーマンスを向上させるかを決定することである。
論文 参考訳（メタデータ） (2024-09-09T18:21:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。