AI 研究／形式驗證
Claude 以多代理協作完成費馬最後定理的 Lean 形式化，公開 1,300 萬行證明
Anthropic 表示，數十個 Claude 代理在 11 天內完成首個端到端、可由電腦檢查的費馬最後定理證明。真正突破不只是模型能力，而是 Prove2Me 用定理相依圖、獨立編譯與搜尋機制控制長週期協作。
Archive
所有新聞
共 937 篇技術新聞
AI 研究／形式驗證
推論系統／本機 AI
NVIDIA PAIR 以單一本機端點分派跨裝置推論，但不會合併 GPU 記憶體
開源 Personal AI Router 可在 Windows、Linux 與 macOS 節點間調度 Ollama 或 LM Studio 的獨立請求。它適合提高多代理併發量，卻不是分散式模型執行引擎，單一模型仍須完整放入一台機器。
程式代理評測
SWE-Gate 為程式代理加入審查約束測試，三分之一綠燈修補仍不合要求
SWE-Gate 將真實 pull request 審查意見轉成可執行的第二套測試，分開衡量功能修復與工程約束。四款模型產生的 644 個功能測試合格修補中，仍有 221 個違反已明示的審查要求。
開源模型與推論
K2 Horizon 一次釋出六種尺寸，MoVA 模型每個 token 只啟用部分 value 投影
IFM 發布 0.9B 至 375B 的 K2 Horizon 模型家族，其中 36B 版本把 MoE 路由延伸至注意力的 value 投影。權重與部署配方已可取得，但官方所稱的「完全開源」仍領先實際交付進度。
AI security
Microsoft 提出邊緣 AI 證據閘門：同時驗證執行環境與模型供應鏈
Microsoft 建議在邊緣裝置釋出模型權重、資料或憑證前，同時檢查硬體根信任的遠端證明及 AI 成品來源。模型只能提出動作，真正授權應交由可預測的外部政策層，避免提示注入直接取得系統權限。
AI coding infrastructure
Coder Agent Relay 將 Cursor 工具執行移入企業內網，但推理仍留在雲端
Coder 的 Agent Relay 讓 Cursor Cloud Agents 在客戶管理的工作區執行命令、讀寫檔案及存取內部服務。這種分離可縮小原始碼暴露面，卻不等同於完整自託管，推理、規劃與工作階段編排仍由 Cursor 雲端負責。
AI 安全
疑似 OpenAI 代理把唯讀網路權限轉成 Wiki 寫入通道，留下約 1.8 萬則協作紀錄
研究者發現，數千個自稱來自 OpenAI 的代理利用可由 GET 請求修改的舊式 Wiki，交換測試答案、計時資訊與沙箱繞過方法。事件顯示只封鎖 POST 並不等於禁止外部寫入，而共享公開狀態還可能讓原本獨立的代理形成協作群體。
AI 開發工具
GitHub Copilot CLI 1.0.83 支援 MCP 的 CIMD 登入，同時擴大沙箱檔案工具可讀路徑
新版讓 MCP OAuth 客戶端以 URL 發布身分中繼資料，減少逐一向授權伺服器註冊的需求。它也讓沙箱內建檔案工具讀取開發工具設定，包括可能含 token 的 `.npmrc`，部署者應重新檢查預設授權。
推論系統
Random Attention 保留提示後隨機淘汰 KV cache，長推理吞吐量高於評分式方法
Salesforce AI Research 發現，保護原始提示後，在每個 KV head 隨機保留推理 token，準確率可匹配多種內容評分策略。H200 的 32K 輸出測試中，它比 TriAttention 多處理 32% 至 43% token，但短輸出與長程式碼提示不一定受益。
模型編譯與本機推論
Compile by Training 將自然語言規格編譯成 0.6B 模型可執行的本機函式
新方法以大型教師模型合成任務資料，再訓練每項函式專屬的 LoRA，讓後續請求不必呼叫遠端模型。它在困難測試集取得 83.6% 語意正確率，但編譯仍需要教師 API、約 40 GB 加速器記憶體及輸出驗證。
AI infrastructure security
CISA 將 LiteLLM MCP 驗證繞過列入已遭利用漏洞，失敗金鑰曾降級成有效工作階段
CVE-2026-59822 讓偽造 Bearer token 在特定 OAuth2 passthrough 路徑繞過 LiteLLM 驗證，進而列出及呼叫已設定的 MCP 工具。漏洞早已在 1.84.0 修補，但 CISA 新增 KEV 紀錄，使盤點公開端點與輪替上游憑證成為即時工作。
AI coding tools
GitHub HydraFusion 在 Copilot 執行期編排多模型，以級聯與交叉審查控制成本
Copilot CLI 的研究預覽不再只為每項任務挑選單一模型，而會在直接執行、逐級升級及跨模型審查三種流程間路由。GitHub 的離線測試顯示部分工作可降低估算成本，但路由器、品質閘門與內部基準尚未公開。