論文の概要: Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research
- arxiv url: http://arxiv.org/abs/2608.15052v2
- Date: Thu, 20 Aug 2026 15:44:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-21 14:00:35.323295
- Title: Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research
- Title（参考訳）: Andy: 厳密な証明と自律的な研究のための数学的エージェント
- Authors: Zi'an Wang,
- Abstract要約: Andyは、数学の問題をトレース可能な証明に変える、自律的な数学的研究エージェントだ。
提案された問題を解いたり検証したりし、研究価値ゲートを通じて文学的な新しい問題を定式化し、証明構築と最終的な検証を行う。
実行可能DAGで証明ステップを編成し、各ステップを独立して検証し、その結果を証明書にバインドする。
- 参考スコア（独自算出の注目度）: 8.964774625644965
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Andy is an autonomous mathematical research agent that turns a mathematical problem into a traceable proof. It solves or verifies a submitted problem, formulates a literature-grounded new problem through a research-value gate, and carries it through proof construction and final verification. It organizes proof steps in an executable DAG, verifies each step independently and binds the result to a certificate, retains verified work whose interfaces remain unchanged during local repair, and records the full path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. Starting from a self-triggered impulsive consensus result, Andy formulates a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The proposed hybrid control combines self-triggered impulses with execution delay and continuous feedback over a recovery window. After each delayed impulse, the feedback cancels the delayed error channel until the pre-impulse history leaves the active delay interval. Sufficient conditions for global exponential synchronization are established, Zeno behavior is excluded for both timing sequences, and a numerical example illustrates the result.
- Abstract（参考訳）: Andyは、数学の問題をトレース可能な証明に変える、自律的な数学的研究エージェントだ。
提案された問題を解いたり検証したりし、研究価値ゲートを通じて文学的な新しい問題を定式化し、証明構築と最終的な検証を行う。
実行可能DAG内の証明ステップを整理し、各ステップを独立して検証し、その結果を証明書にバインドし、局所的な修復中にインターフェースが変化しない検証作業を保持し、問題定式化から最終証明までの完全なパスを記録する。
このシステムは、正当性評価から証明生成を分離し、既存の結果から知識を取得し、保持し、回収し、再利用することができる。
自己トリガーインパルスコンセンサスの結果から始まり、アンディは通信トポロジを切り替えた遅延ヘテロジニアスネットワークに対するグローバル指数的リーダー-フォローラー同期問題を定式化する。
提案したハイブリッド制御は、自己トリガーインパルスと実行遅延とリカバリウィンドウ上での継続的なフィードバックを組み合わせたものである。
遅延インパルス毎にフィードバックは遅延エラーチャネルをキャンセルし、プレインパルス履歴はアクティブ遅延間隔を逸脱する。
グローバル指数同期のための十分条件が確立され、両方のタイミングシーケンスに対してゼノの挙動が除外され、数値的な例が結果を示す。
関連論文リスト
- When benchmark inferences do not compose: Projectibility in AI evaluation [0.0]
AIベンチマークの結果が1ステップで連続的なクレームに達することはめったにない。
評価者はそれをさらなるケースに一般化し、能力の証拠として解釈し、新しいタスクに外挿し、他のシステムやサイトへ輸送する。
保証リンクは保証チェーンを自動的に作らない。
論文 参考訳（メタデータ） (2026-07-28T18:07:04Z) - Temporal-Causal Unity as an Operational Framework for Collective Dynamics: Causal-Progress Clocks, Synchronization, and Polarization [5.995482369040288]
本稿では,プロセス哲学的論文時間と因果変化の順序的展開を結びつける枠組みを開発する。
このフレームワークは意図的に3つの主張を分離する: 成立に関する解釈論、測定可能な因果関係座標、ネットワークモデル。
本論文は、因果関係と時系列モデルを比較するための、偽装可能な仮説とサンプル外プロトコルを導出する。
論文 参考訳（メタデータ） (2026-07-21T01:39:53Z) - One Reflection Is Not Enough: Self-Correcting Autonomous Research via Multi-Hypothesis Failure Attribution [85.65263343588026]
我々は,自己修正型,自律型,接地型実験機であるSAGEを提案する。
その中核的なメカニズムであるMHFA(Multi-Hypothesis Failure Attribution)は、回復を構造的因果診断として扱う。
12のトピック、5ドメインのベンチマークでは、SAGEは基準リフレクションでメトリクスを含むアウトプットを42%から92%に増やしている。
論文 参考訳（メタデータ） (2026-06-30T10:54:16Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving [13.446180044466324]
メカニック(Mechanic)は、謝罪駆動の形式的分解戦略を採用した新しいエージェントシステムである。
未解決のサブゴールを正確に分離するために、リーンの残念なプレースホルダーを活用することで、Mechanicは失敗するサブプロブレムを、クリーンで自己完結したコンテキストに抽出し、独立して解決する。
論文 参考訳（メタデータ） (2026-03-25T16:12:08Z) - ExDR: Explanation-driven Dynamic Retrieval Enhancement for Multimodal Fake News Detection [23.87220484843729]
マルチモーダルのフェイクニュースは 深刻な社会的脅威を引き起こします
Dynamic Retrieval-Augmented Generationはキーワードベースの検索をトリガーすることで、有望なソリューションを提供する。
マルチモーダルフェイクニュース検出のための説明駆動動的検索生成フレームワークであるExDRを提案する。
論文 参考訳（メタデータ） (2026-01-22T10:10:06Z) - Circular Reasoning: Understanding Self-Reinforcing Loops in Large Reasoning Models [66.11277323593475]
Circular Reasoningは、生成されたコンテンツが自身の再発の論理的前提として機能する自己強化トラップである。
機械学的には、円の推論は異なる境界を示す状態崩壊として特徴付けられる。
自己強化型V字型アテンション機構によって駆動される不自由なサイクルとして継続するループ開始を誘導する推論が阻害されることを明らかにする。
論文 参考訳（メタデータ） (2026-01-09T10:23:55Z) - Adversarial Yet Cooperative: Multi-Perspective Reasoning in Retrieved-Augmented Language Models [72.4149653187766]
本稿ではAdrialversa Reasoning RAG(ARR)というReasoner-Verifierフレームワークを提案する。
ReasonerとVerifierは、回収された証拠を推論し、プロセス認識の利点によってガイドされながら、互いの論理を批判する。
複数のベンチマーク実験により,本手法の有効性が示された。
論文 参考訳（メタデータ） (2026-01-08T06:57:03Z) - Althea: Human-AI Collaboration for Fact-Checking and Critical Reasoning [26.796186521236194]
本稿では,オンラインクレームのユーザ主導評価を支援するために,質問生成,証拠検索,構造化推論を統合した検索強化システムであるAltheaを紹介する。
AVeriTeCベンチマークでは、Altheaは0.44のマクロF1を達成し、標準的な検証パイプラインを上回り、サポートされたクレームと反証されたクレームの識別を改善している。
論文 参考訳（メタデータ） (2025-12-29T18:23:35Z) - Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
We present WebDetective, a benchmark of hint-free multi-hop questions with a control Wikipedia sandbox。
25の最先端モデルに対する我々の評価は、すべてのアーキテクチャにまたがる体系的な弱点を明らかにしている。
私たちはエージェントワークフローであるEvidenceLoopを開発し、ベンチマークが特定する課題を明示的にターゲットしています。
論文 参考訳（メタデータ） (2025-10-01T07:59:03Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。