速報
MathlibPR：以 LLM 評估 Lean/Mathlib Pull Request 的基準初探
背景：Lean與Mathlib為LLM輔助形式化推理的主流。方法：提出MathlibPR基準，從Mathlib4真實PR歷史擷取資料並設計分階段評估，測試多款大型語言模型與代理人。結果：模型難以區分可合併PR與僅通過建置但未合併的PR，MathlibPR提供審查輔助的監督信號。
LLM
深度分析
GASim：結合EDG、GOM與GMP的圖加速混合多代理社會模擬框架
大規模社會模擬常受LLM記憶檢索與序列式ABM更新造成延遲與成本瓶頸。GASim以Graph-Optimized Memory用稀疏記憶圖與輕量圖傳播取代昂貴檢索，並以Graph Message Passing透過圖注意力在批次中並行更新一般代理，另以Entropy-Driven Grouping動態辨識核心代理。結果顯示系統在效能與令牌消耗上有顯著改善。
深度分析
FactoryBench 基準：用多變數時序資料測量工業機器人之因果推理與工程決策能力
研究聚焦工業機器人時序資料以評估機器理解能力。本文建立FactoryBench與FactoryWave，使用分層問答檢驗狀態、干預、反事實與決策四層因果推理。零樣本評估顯示主流大型模型在結構化解析未超過50%、決策層低於18%，揭示語言模型直接讀取工業訊號的明顯不足並指向工具化代理的需求。
深度分析
DoLQ 框架：以 LLM 融合語意評估與數值優化進行 ODE 發現
科學上需從觀測資料推導微分方程，數值擬合 alone 無法保證物理合理。DoLQ 採三代理流程：Sampler 提出符號候選並解釋物理依據、Optimizer 擬合參數、Scientist Agent 用 LLM 做定性語意與定量誤差的綜合評估。實驗在多維 ODE 基準上顯示 DoLQ 更常回復正確符號結構並提升發現成功率。
深度分析
SAFE：以 LLM 情境化靜態分析評估公開研究工件的安全風險
本研究檢視509份公開研究工件，指出現行工件評估偏重可重現性而忽略安全風險。提出SAFE框架，結合靜態分析、程式語意與執行脈絡，並以大型語言模型協助判斷可利用性。結果顯示大量靜態警示並非全部可利用，但約四成常見標示在實務使用下具安全疑慮，SAFE能有效區分實務風險。
深度分析
從回饋到採納：以 RelScore、SuccScore 與 10,235 次提交比較兩款 LLM 驅動 AI 輔導器
在教室中部署的 LLM 驅動 AI 輔導系統，傳統上以回饋的教學品質為主要評估指標，但忽略了學生是否以及如何採納回饋的行為層面。
深度分析
驗證導向知識圖譜：以多代理與 LLM 驅動自動化 SystemVerilog Assertion 生成
研究提出一套以驗證為中心的知識圖譜（KG）與多代理流程，將規格、RTL 與形式工具回饋轉為結構化中介表示，並匯入執行時 KG 作檢索與追溯。系統用 KG 提供設計接地的上下文，驅動 SVA 生成與三種精煉迴圈──語法修復、以反例（CEX）追溯的修正、以及覆蓋率導向的屬性擴增。
深度分析
以大型語言模型進行哲學概念分析：反例生成與演員-評論家迭代實驗
研究以哲學反例修正遊戲測試語言模型的概念分析能力，透過模型產生反例再修正定義的迭代流程。結果顯示模型接受的反例約為人工兩倍，迭代僅使定義變長而未提升準確性，此外，人類與模型在判斷有效性上呈中等一致，且不同概念呈現出不同的穩定性，顯示哲學概念的多樣性仍是挑戰。
深度分析
LLM 與 AI 審稿風險：ICLR 2026 證據顯示 hivemind 與論文漂白問題
審稿負擔激增，研究以ICLR2026評審資料比較人類與AI評論，發現AI評審出現明顯群體思維與論文漂白現象；透過零次自動重寫，AI評分可被文風改動顯著提升，且使評論語態與內容趨同。研究主張在全面採用前須建立嚴謹實證評估、抗操弄測試與多元意見保護。
生成式 AI
以結構感知與核心熵量化：以異質再生（xeno‑reproduction）對抗生成式 AI 同質化
研究指出生成式人工智慧在資料偏見與模式崩潰下，會造成輸出同質化。論文提出「異質再生」策略與結構感知多樣性追求，將模型輸出視為字串樹，透過核心熵與偏離度量化多樣性，並提出分布級與軌跡級的干預評分。此框架強調把多樣性納入AI安全核心，為後續算法與實證研究提供概念架構。
深度分析
大型語言模型（LLM）預測錯誤高度相關，可能削弱群體多樣性
研究在Metaculus平台上評估大型語言模型在預測任務的誤差相依性；以三款主流模型的568個已解題目、社群時間序列和類別指紋做對照。主要發現：模型間預測錯誤高度相關，但在該精英社群中尚未觀察到明顯的偏誤傳播。該現象構成潛在的認知單一化風險。
深度分析
U-Define：結合 LLM 與模型檢查的硬性/軟性約束規劃工作流
在大型語言模型成為常見規劃工具的情境下，黑盒特性帶來可靠性與可控性挑戰。U-Define 提出以自然語言讓使用者定義約束，並將約束標記為「硬性」或「軟性」，分別採用形式化模型檢查與 LLM-as-judge 的驗證機制。系統自動把使用者語句轉成可驗證的形式，並在生成多個候選計畫後以對應方法檢驗與回饋。