論文の概要: Formalizing Cooperation and Competition: An AI-Assisted Mathematical Addendum to a 2018 Planning Thesis
- arxiv url: http://arxiv.org/abs/2610.29637v1
- Date: Wed, 21 Oct 2026 12:17:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-23 00:40:06.355504
- Title: Formalizing Cooperation and Competition: An AI-Assisted Mathematical Addendum to a 2018 Planning Thesis
- Title（参考訳）: フォーマライズ協力と競争 - 2018年の計画論へのAI支援の数学的追加
- Abstract要約: 我々は,戦略的選択,協力的安定,参加承認,執行機関の関係を再構築する。
固定された外部者および明示的な効率条件下での2人の関係を検証した。
形式化のサポートは、幾何の取得と後悔に基づく効率性に対処する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present an AI-assisted mathematical addendum to Strategic Trip Planning: Striking a Balance Between Competition and Cooperation (Amar, 2018). We reconstruct selected relationships between strategic choice, cooperative stability, participant approval and enforcement. The thesis's Nash-to-core proposition is under-specified until outsider opportunities are stated. We verify two-person implications under fixed outsiders and explicit efficiency conditions. Under isolation, the original example has an empty TU core; its funded counterpart uses an explicit external subsidy. For a monotone resource model we characterize the exact financing gap. A finite negotiation procedure implemented in Lean is proved to terminate with participant approval, joint-cost non-worsening and local optimality against permitted approved moves. Supporting formalizations address bargaining geometry and regret-based efficiency. A resource-game counterinstance shows why monotonicity alone provides no uniform price-of-anarchy bound. Reproducible computations compare a documented heuristic reconstruction with the verified procedure on 44 source-based instances and 96 starting cases from four additional synthetic network families. Acceptance-matched heuristic and randomized pairwise-search controls contextualize the optimization results. The mathematical ingredients are established results; the contribution is a traceable reconstruction linking source statements, explicit assumptions, checked proofs, executable code and retained counterinstances. The study illustrates how AI-assisted investigation can turn engineering intuitions from legacy research into precise mathematical claims whose conditions and computational consequences can be inspected and reproduced.
- Abstract（参考訳）: 我々は,ストラテジック・トリップ・プランニング:競争と協力のバランスを取る(Amar, 2018)。
我々は,戦略的選択,協力的安定,参加者の承認,執行の間の選択された関係を再構築する。
論文のナッシュ・ツー・コアの提案は、外部の機会が述べられるまで未定である。
固定された外部者および明示的な効率条件下での2人の関係を検証した。
元々のサンプルは空のTUコアを持ち、資金源は明示的な外部補助金を使用する。
単調な資源モデルでは、正確な資金調達ギャップを特徴付ける。
リーンで実施された有限の交渉手続きは、承認された動きに対して、参加者の承認、共同コストの非警告、局所的最適性によって終了することが証明される。
形式化のサポートは、幾何と後悔に基づく効率の獲得に対処する。
資源ゲームカウンターインスタンスは、なぜ単調性だけで均一な価格-アナーキー境界を提供しないのかを示している。
再現可能な計算は、文書化されたヒューリスティックな再構成と、44のソースベースインスタンスの検証手順と、追加の4つの合成ネットワークファミリーからの96の開始事例を比較した。
アクセプタンスマッチング型ヒューリスティックおよびランダム化されたペアワイズ検索制御は、最適化結果を文脈化する。
コントリビューションは、ソースステートメント、明示的な仮定、チェックされた証明、実行可能コード、および保持された反インスタンスをリンクするトレース可能な再構成である。
この研究は、AIが支援する調査によって、レガシー研究からのエンジニアリングの直感を、条件や計算結果が検査され再現できる正確な数学的クレームに変換する方法を示している。
関連論文リスト
- Parallel AI Agent Collaboration as Graph-Structured Distributed Block Optimization [51.43213415859029]
並列AIエージェントは、有効なローカル編集を生成できるが、編集が組み合わされた場合、共有ソリューションを分解できることが示される。
独立集合は、同じ現在の解に対して測定された検証されたゲインが正確に加算された互換性のある編集を認証する。
最適な分数カラー化は、検証された局所改善の合計の1/f(G)=1/f(G)の分数を保持する合併をもたらすことを証明している。
論文 参考訳（メタデータ） (2026-10-21T17:27:17Z) - ReTAC: Residual Test-Time Agentic Computation for Video Spatial Reasoning [75.14564822108872]
テストタイムエージェント計算は多モーダルな言語モデルを改善することができる。
ビデオ空間推論のためのトレーニング不要なマルチエージェントフレームワークであるReTACで、この定式化をインスタンス化する。
論文 参考訳（メタデータ） (2026-10-12T07:39:58Z) - ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization [5.053793874612475]
本稿では,ProofLoomを紹介した。Proof-Obligation-Driven Theory Constructionのための,完全に自動化されたLLMエージェントシステムである。
ProofLoomは、公開されたアルゴリズム、ターゲット定理、およびソース証明を与えられた後、リーンモデルとサポート理論を自律的に構築する。
33の開発で、490,693行のアルゴリズムローカルなリーンコードを生成する。
論文 参考訳（メタデータ） (2026-09-28T11:45:27Z) - Autoformalizing Argumentative Material Inferences [26.35292656634472]
我々は、ガード補完として議論材料推論のための自己形式化を開発する。
GUARDは、証明された信条を大幅に改善する。
シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
論文 参考訳（メタデータ） (2026-09-15T11:05:26Z) - Compute-Bounded Security Assurance - Coverage, Verification, and Response under Resource Constraints [0.0]
追加の推論計算は、正しく解決されたセキュリティ保証タスクの数を増やすことができる。
我々は、成功、ユニークなカバレッジ、承認された証拠、運用上の保護を分離するリソース制約のあるフレームワークを開発する。
概念的防御アーキテクチャは、証拠分析、判断、運用権限を分離する。
論文 参考訳（メタデータ） (2026-09-07T13:07:55Z) - When benchmark inferences do not compose: Projectibility in AI evaluation [0.0]
AIベンチマークの結果が1ステップで連続的なクレームに達することはめったにない。
評価者はそれをさらなるケースに一般化し、能力の証拠として解釈し、新しいタスクに外挿し、他のシステムやサイトへ輸送する。
保証リンクは保証チェーンを自動的に作らない。
論文 参考訳（メタデータ） (2026-07-28T18:07:04Z) - VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。
VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。
Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文 参考訳（メタデータ） (2026-06-03T20:02:35Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - Preventing the Collapse of Peer Review Requires Verification-First AI [49.995126139461085]
我々は、真理結合、すなわち、過度に科学的真理をトラックする場所のスコアの厳密さを提案する。
プロキシ・ソブリン評価に向けた相転移を駆動する2つの力の形式化を行う。
論文 参考訳（メタデータ） (2026-01-23T17:17:32Z) - Model-free Methods for Event History Analysis and Efficient Adjustment (PhD Thesis) [55.2480439325792]
この論文は、モデルフリーの観点から統一された統計学への独立した貢献のシリーズである。
第1章では、機械学習から予測技術を活用する柔軟なメソッドを定式化するために、モデルフリーの視点をどのように利用できるか、詳しく説明している。
第2章では、あるプロセスの進化が他のプロセスに直接影響されるかどうかを記述した地域独立の概念を研究している。
論文 参考訳（メタデータ） (2025-02-11T19:24:09Z) - Anti-Concentrated Confidence Bonuses for Scalable Exploration [57.91943847134011]
固有の報酬は、探検と探検のトレードオフを扱う上で中心的な役割を果たす。
楕円ボーナスを効率的に近似するためのエンファンティ集中型信頼境界を導入する。
我々は,Atariベンチマーク上での現代固有の報酬と競合する,深層強化学習のための実用的な変種を開発する。
論文 参考訳（メタデータ） (2021-10-21T15:25:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。