論文の概要: AI with Authority, from Application to Silicon

• arxiv url: http://arxiv.org/abs/2608.21356v2
• Date: Tue, 25 Aug 2026 22:53:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-27 14:15:14.904133
• Title: AI with Authority, from Application to Silicon
• Title（参考訳）: オーソリティによるAI - アプリケーションからシリコンへ
• Abstract要約: 5週間で、消費者向けAIサブスクリプションの研究者の1人が、コミュニティのシリコンシャトルに搭載されたRISC-Vプロセッサに、少数のAIエージェントを誘導した。 人間によるレビューを通した証拠はなく、RTLは人間によって書かれたものでもない。 作業の規律 -- ソルト法 -- は、幻覚的証明が通過できない証明カーネルに依存している。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: For sixty years, machine verification has been a major cost overhead, affordable only for exceptional artifacts. Here we report that generative AI inverts this relationship: at AI speed, machine verification is not only economical but essential to productivity --- it is the incorruptible referee that lets one person safely direct autonomous machine work at scale. In five weeks, one researcher on consumer AI subscriptions directed a small fleet of AI agents from application code, through a verified compiler and executive, to a RISC-V processor taped out on a community silicon shuttle; no proof passed through human review, and no RTL was written by a human. The working discipline --- the Salt method --- rests on a proof kernel no hallucinated proof can pass: mathematical claims travel between agents as kernel-checked artifacts, and human attention is reserved for statements, designs, and rulings. Verification is stated link by link, from the Lean 4 kernel to SAT-checked equivalence at the silicon boundary. We publish the complete accounting: theorem provenance, a pre-registered token meter, floor-bounded human time, and an error ledger whose catch numbering runs to #256 --- a monotone counter over the mathematics campaign's append-only flags ledger, maintained 2026-07-07 to 2026-07-20 (one number, #79, was never assigned; later catches are recorded un-numbered) --- against zero incorrect proofs reaching the record.
• Abstract（参考訳）: 60年間、マシン検証はコストのオーバヘッドであり、例外的なアーティファクトに対してのみ安価である。 AIのスピードでは、マシン検証は経済的なだけでなく、生産性にも不可欠です。 5週間で、消費者向けAIサブスクリプションの研究者が、検証済みのコンパイラとエグゼクティブを通じて、アプリケーションコードからRISC-Vプロセッサまで、少数のAIエージェントを指示した。 数学的なクレームは、カーネルチェックされたアーティファクトとしてエージェント間を移動し、人間の注意はステートメント、デザイン、および決定のために予約されている。 検証は、Lean 4カーネルからシリコン境界におけるSATチェックされた等価性へのリンクによって記述される。 定理証明、事前登録されたトークンメーター、フロアバウンドされた人的時間、キャッチ番号が#256に走るエラー台帳 -- 2026-07-07から2026-07-20(1つの番号、#79は割り当てられず、後に記録された) -- は、レコードに到達したゼロの不正な証明に対して、数学のキャンペーンの追加専用フラグ台帳に対するモノトンカウンター -- を発行する。

関連論文リスト

• AI-Assisted Design of a Post-Quantum Cryptographic Accelerator: A Deployed-Silicon Case Study [0.4251773265892765]
  我々は、標準の受け入れゲートを、事実上のゴールデンレファレンスオラクルに置き換える。 エージェント型大規模言語モデルがML-KEM-768とML-DSA-65アクセラレータを駆動する実験を232回報告した。
  論文  参考訳（メタデータ） (2026-09-03T16:34:50Z)
• Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free [0.0]
  2026年5月、OpenAIモデルはアーズ単位距離予想に対する反例を生み出した。 同じ日に5人の数学者が人間による検証版を出版し、その結果は数週間以内に文献に載った。 2026年8月、同研究所は10の数学的および理論的コンピュータ科学結果を発表し、それぞれにマシンチェック可能なLean 4証明書を添付した。
  論文  参考訳（メタデータ） (2026-08-29T02:09:18Z)
• $Z^2$-ACT: End-to-End Verifiable Agentic Intent Control for Open 6G RAN [43.15181031994434]
  本稿では,ゼロ知識監査制御とゼロ信頼検証エージェントインテントアーキテクチャを提案する。 実大規模言語モデルは、オペレータの意図をIntent Contractsに変換するために、非リアルタイムパスで使用される。 その結果、動作フィルタリングと攻撃レジリエンスを適度なレイテンシとシグナリングコストで改善したことが示唆された。
  論文  参考訳（メタデータ） (2026-08-21T12:44:03Z)
• F(AI)2R: Who Did What, and Who Checked? Verifiable AI Provenance as an Executable Skill [0.0]
  F(AI)2Rは、AIを使ったFAIR研究であり、AI支援のオーサリングパスと、すべてのアーティファクトに対するマシン可読な監査パスである。 本稿では,AI-in-the-loopアーティファクトをカバーするPROV-O拡張であるaiprovに,学術的な記述以上の証明モデルを一般化する。 プロダクションにおけるすべてのアクティビティ、クレーム、ソースは、2つのインの下にリポジトリの証明グラフに記録される。
  論文  参考訳（メタデータ） (2026-07-28T12:17:53Z)
• The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
  検証者主導のループにおいて、AIエージェントは古典的および後量子暗号、TLS 1.3、IKEv2、X.509、マトリックスクライアントにまたがるAda/SPARKのベアメタルセキュリティソフトウェアを書いて検証した。 GNATproveは49,280の証明義務を解除し、選択されたプリミティブに対して機能的正当性を確立し、残りのプリミティブに対して実行時のエラーがないことを証明した。 それぞれのレイヤが障害をキャッチし,中心的な教訓を引き出す方法を報告します。エージェントが確立するために信頼できるものは,そのフィードバックの強さに縛られているのです。
  論文  参考訳（メタデータ） (2026-07-15T20:09:05Z)
• Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems [0.0]
  本稿では、そのような2つの計算に関する人間-AIコラボレーションについて報告する。 特異な自己随伴シュルディンガー作用素に対して、証明された零数とディリクレ=ノイマンブラケットは、完全な負スペクトルを10個の十進点に証明する。 微妙な非正規原子分子ベンチマークでは、以前は未解決の共鳴対が分離され、各部材は10桁に囲まれている。
  論文  参考訳（メタデータ） (2026-06-22T18:03:59Z)
• 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)
• Characterizing initial human-AI proof formalization workflows [66.06866890889131]
  AIシステムのコード生成能力の進歩と、証明を形式化し、検証する人々の能力を変えるための高度な数学的推論の約束への関与。 我々は、AIが人々のフォーマル化に与える影響について、混合メソッド分析を行う。 質的な調査では、人々の好みは多様であるが、形式化におけるAI支援に対する一般的な欲求が示されている。
  論文  参考訳（メタデータ） (2026-06-02T22:58:19Z)
• Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
  本稿では,インダクティブ・デダクティブ・シンセシス(IDS)について述べる。 IDSは約6.8時間で7/7を達成し、1仕様あたり106ドル、専門家の努力の約200倍、SOTAエージェントの約17%を達成している。 IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。
  論文  参考訳（メタデータ） (2026-05-22T00:05:36Z)
• The Last Human-Written Paper: Agent-Native Research Artifacts [106.47848184955576]
  本稿では,物語紙を機械処理可能な研究パッケージに置き換えるプロトコルであるAgent-Native Research Artifact(ARA)を紹介する。 通常の開発において決定と終了をキャプチャするLive Research Manager、レガシPDFとリポジトリをARAに変換するARAコンパイラ、人間レビュアーが重要性、ノベルティ、味にフォーカスできるように客観的チェックを自動化するARAネイティブレビューシステムである。
  論文  参考訳（メタデータ） (2026-04-27T16:23:09Z)
• SWE-chat: Coding Agent Interactions From Real Users in the Wild [70.18158706281724]
  SWE-chatは、オープンソースの開発者から収集された実際のコーディングエージェントセッションの大規模なデータセットである。 現在、データセットには6000のセッションが含まれており、63,000以上のユーザプロンプトと355,000のエージェントツールコールが含まれている。
  論文  参考訳（メタデータ） (2026-04-22T17:08:19Z)
• The Novelty Bottleneck: A Framework for Understanding Human Effort Scaling in AI-Assisted Work [4.726153739634646]
  新規性ボトルネックと呼ばれるメカニズムを分離した人間とAIのコラボレーションモデルを提案する。 モデルはタスクが原子的な決定に分解されると仮定する。 私たちの貢献は、人間の努力が線形にスケールしなければならないという証拠ではありません。
  論文  参考訳（メタデータ） (2026-03-28T22:50:13Z)
• Right to History: A Sovereignty Kernel for Verifiable AI Agent Execution [8.55919915871212]
  既存のシステムは、AIエージェントが何をしたか、独立して検証可能な記録を提供していません。 個人は、自身のハードウェア上で、すべてのAIエージェントアクションを完全かつ検証可能な記録を持つ権利を持つ。
  論文  参考訳（メタデータ） (2026-02-23T07:09:36Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。