大模型推理與驗證：MLLM感知圖靈測試；可驗證獎勵跨領(lǐng)域沖突與互補；LLM形式化代碼驗證
Pixels, Patterns, but No Poetry: To See The World like Humans
2025-07-21｜UCAS, NJU, NUS, BUPT, NKU, PSU, PKU, BJTU|??46
???http://arxiv.org/abs/2507.16863v1????
????https://huggingface.co/papers/2507.16863????
????https://TuringEyeTest.github.io???
研究背景與意義
- 多模態(tài)大語言模型（MLLMs）近年來在視覺理解與語言處理的結(jié)合上取得了顯著進展，成為人工智能領(lǐng)域的重要研究方向。
- 盡管已有研究多聚焦于提升MLLMs的推理能力，但“MLLMs是否能像人類一樣感知世界”的根本問題尚未解決。
- 本文提出了“圖靈之眼測試”（Turing Eye Test, TET），一個專注于感知能力的基準測試，設(shè)計了四個診斷任務(wù)，考察模型對合成人類直觀處理的圖像的感知表現(xiàn)。
- 研究發(fā)現(xiàn)，當前最先進的MLLMs在這些感知任務(wù)上表現(xiàn)極差，顯示出視覺感知與理解方面的顯著瓶頸，尤其是視覺編碼器（vision tower）的泛化能力不足，而非語言推理或知識能力的缺陷。
研究方法與創(chuàng)新
- 基準設(shè)計創(chuàng)新：TET基于四個視覺感知任務(wù)構(gòu)建，涵蓋隱藏文本識別、3D驗證碼識別、色盲測試圖案識別以及復(fù)雜漢字結(jié)構(gòu)識別，任務(wù)設(shè)計貼近人類直觀視覺感知，區(qū)別于傳統(tǒng)以推理為核心的多模態(tài)評測。
- 多模型廣泛評測：選取15個不同架構(gòu)和規(guī)模的MLLMs，涵蓋統(tǒng)一多模態(tài)模型、閉源API模型及開源模型，全面評估其在TET任務(wù)上的表現(xiàn)，體現(xiàn)了研究的廣泛適用性和代表性。
- 深入機制分析：利用Grad-CAM技術(shù)揭示模型視覺編碼器及語言解碼器的注意力分布，發(fā)現(xiàn)模型難以準確聚焦關(guān)鍵視覺區(qū)域，視覺編碼器常偏重整體物體特征而忽視文本或細節(jié)特征，語言解碼器則缺乏對視覺信息的有效利用。
- 細粒度微調(diào)實驗：通過監(jiān)督微調(diào)對模型不同組件（視覺編碼器、語言骨干、視覺語言適配器等）進行參數(shù)更新，發(fā)現(xiàn)僅視覺編碼器微調(diào)能顯著提升任務(wù)表現(xiàn)，驗證了視覺編碼器泛化能力的核心瓶頸。
- 學(xué)習(xí)范式探索：嘗試上下文學(xué)習(xí)（in-context learning）以提升模型感知能力，結(jié)果顯示上下文示例對感知任務(wù)無明顯提升，進一步凸顯架構(gòu)及視覺表征的根本限制。
- 圖像處理實驗：通過對輸入圖像進行下采樣和模糊處理，發(fā)現(xiàn)下采樣能提升模型在隱藏文本任務(wù)上的表現(xiàn)，說明視覺編碼器對圖像分塊處理機制的敏感性及當前視覺特征提取方法的局限。
- 理論基礎(chǔ)：研究基于視覺編碼器（如ViT）與語言模型的聯(lián)合架構(gòu)，強調(diào)視覺編碼器對感知任務(wù)的核心作用，提出感知與推理能力需分開考察，呼吁未來結(jié)合感知階段的推理能力以提升視覺泛化。
實驗設(shè)計與結(jié)果分析
- 數(shù)據(jù)集構(gòu)建：TET包含四個子任務(wù)，分別為150張隱藏文本圖像、150個3D驗證碼、150張色盲測試圖以及40個復(fù)雜漢字組合，任務(wù)難度設(shè)計貼近人類直覺，確保評測的真實性和挑戰(zhàn)性。
- 模型評測結(jié)果：15個MLLMs在四個任務(wù)上的Pass@1和Pass@32指標均極低，多數(shù)任務(wù)表現(xiàn)為零，最高也未超過約5%，顯示模型在感知任務(wù)上的“災(zāi)難性失敗”。
- 性能曲線：隨著Pass@K增大，模型表現(xiàn)提升極其有限，說明增加生成嘗試次數(shù)無法彌補視覺感知的根本不足。
- Grad-CAM可視化：模型視覺編碼器注意力多偏離關(guān)鍵字符區(qū)域，語言解碼器注意力散亂，表明模型未能有效聚焦任務(wù)相關(guān)視覺信息。
- 微調(diào)效果：僅視覺編碼器微調(diào)顯著提升準確率（最高達90%以上），而語言骨干微調(diào)或視覺語言適配器微調(diào)效果甚微，驗證視覺編碼器是當前性能瓶頸。
- 上下文學(xué)習(xí)無效：多模型上下文學(xué)習(xí)示例加入后，感知任務(wù)表現(xiàn)無明顯提升，反映出知識補充無法解決感知架構(gòu)缺陷。
- 圖像處理影響：下采樣處理提升隱藏文本任務(wù)表現(xiàn)，模糊處理效果不佳，揭示視覺編碼器對圖像分塊的依賴性及潛在的視覺特征提取不足。
結(jié)論與展望
- 本文通過TET基準揭示了當前最先進的多模態(tài)大語言模型在視覺感知方面存在的根本性缺陷，尤其是視覺編碼器泛化能力不足，導(dǎo)致模型無法像人類一樣直觀地理解圖像內(nèi)容。
- 研究明確區(qū)分了視覺感知與語言推理能力，指出提升模型推理能力不足以解決感知瓶頸，強調(diào)未來工作應(yīng)聚焦視覺編碼器的結(jié)構(gòu)改進和視覺泛化能力提升。
- 微調(diào)實驗表明，針對視覺編碼器的專門訓(xùn)練是提升感知能力的關(guān)鍵路徑。
- 建議未來探索將推理能力注入感知階段，融合像GRPO等先進訓(xùn)練方法，以促進視覺編碼器對復(fù)雜視覺模式的理解和泛化。
- 計劃發(fā)布更豐富多樣的TET任務(wù)集，推動多模態(tài)模型在感知能力評測和提升上的持續(xù)進步，促進構(gòu)建更接近人類視覺認知的智能系統(tǒng)。
Can One Domain Help Others? A Data-Centric Study on Multi-Domain Reasoning via Reinforcement Learning
2025-07-23｜OpenDataLab, Shanghai AI Lab|??23
???http://arxiv.org/abs/2507.17512v1????
????https://huggingface.co/papers/2507.17512????
????https://github.com/Leey21/A-Data-Centric-Study???
研究背景與意義
- 研究背景：隨著大型語言模型（LLMs）推理能力的快速發(fā)展，強化學(xué)習(xí)與可驗證獎勵（RLVR）成為提升模型推理水平的重要范式?，F(xiàn)有研究多聚焦于單一領(lǐng)域（如數(shù)學(xué)、編程、邏輯推理）的強化學(xué)習(xí)應(yīng)用，然而現(xiàn)實應(yīng)用往往涉及多領(lǐng)域綜合推理，領(lǐng)域間的交互機制尚未充分理解。
- 研究意義：本研究系統(tǒng)性探討了數(shù)學(xué)、代碼生成和邏輯謎題三大推理領(lǐng)域在RLVR框架下的協(xié)同訓(xùn)練效果，揭示了跨領(lǐng)域訓(xùn)練的互補性與沖突，深入分析了監(jiān)督微調(diào)（SFT）、課程學(xué)習(xí)、獎勵設(shè)計及語言差異對多領(lǐng)域推理性能的影響，旨在為構(gòu)建具備綜合推理能力的多領(lǐng)域強化學(xué)習(xí)模型提供理論和實踐指導(dǎo)。
研究方法與創(chuàng)新
- 技術(shù)框架：采用Group Relative Policy Optimization（GRPO）算法，結(jié)合Qwen-2.5-7B模型家族，針對數(shù)學(xué)、代碼、邏輯謎題三領(lǐng)域構(gòu)建了多維度訓(xùn)練與評估體系，涵蓋單域訓(xùn)練、跨域聯(lián)合訓(xùn)練、監(jiān)督微調(diào)前后的對比分析，以及課程學(xué)習(xí)和獎勵設(shè)計的系統(tǒng)探究。
- 創(chuàng)新點：
多領(lǐng)域系統(tǒng)性分析：首次系統(tǒng)揭示數(shù)學(xué)、代碼與邏輯推理三領(lǐng)域在強化學(xué)習(xí)中的相互作用，包括相互促進與潛在沖突。
監(jiān)督微調(diào)與強化學(xué)習(xí)結(jié)合：深入比較基礎(chǔ)模型與經(jīng)過指令微調(diào)模型在強化學(xué)習(xí)中的表現(xiàn)差異，明確SFT對RL效果的關(guān)鍵促進作用。
課程學(xué)習(xí)策略創(chuàng)新：提出策略刷新機制，通過階段性更新參考模型和優(yōu)化器狀態(tài)，顯著提升課程學(xué)習(xí)的收斂速度和最終性能。
獎勵設(shè)計多樣化：針對不同任務(wù)特性設(shè)計并比較二元獎勵、部分獎勵、格式獎勵和重新縮放獎勵，優(yōu)化訓(xùn)練信號以提升學(xué)習(xí)效率。
語言敏感性研究：首次系統(tǒng)評估中文與英文訓(xùn)練數(shù)據(jù)對模型推理能力的影響，發(fā)現(xiàn)語言差異顯著影響RLVR的泛化能力。
- 理論基礎(chǔ)：基于強化學(xué)習(xí)理論，結(jié)合多任務(wù)學(xué)習(xí)與遷移學(xué)習(xí)原理，構(gòu)建了適應(yīng)多領(lǐng)域推理的訓(xùn)練框架，突破了傳統(tǒng)單域強化學(xué)習(xí)的局限。
實驗設(shè)計與結(jié)果分析
- 實驗設(shè)計：
使用數(shù)學(xué)（DeepScaleR、CountDown）、代碼（CodeR1-12k）、邏輯謎題（Knights-and-Knaves、LogicPuzzleBaron）數(shù)據(jù)集，統(tǒng)一規(guī)模采樣，確保多領(lǐng)域訓(xùn)練數(shù)據(jù)平衡。
評估采用多任務(wù)基準，包括MATH500、AIME24、HumanEval、MBPP及ZebraLogicBench，覆蓋不同推理難度與類型。
訓(xùn)練配置細致調(diào)整，數(shù)學(xué)任務(wù)設(shè)置更長的推理鏈條，代碼任務(wù)采用安全沙箱執(zhí)行環(huán)境，邏輯謎題任務(wù)設(shè)計多階段課程學(xué)習(xí)。
- 關(guān)鍵結(jié)果：
單域訓(xùn)練中，數(shù)學(xué)與邏輯推理任務(wù)互相促進，提升模型推理深度；代碼訓(xùn)練提升代碼生成能力，但對基礎(chǔ)模型存在一定抑制效應(yīng)。
多域聯(lián)合訓(xùn)練表現(xiàn)出復(fù)雜的協(xié)同效應(yīng)，雙域和三域組合均提升整體性能，但不同任務(wù)間的沖突需通過精細設(shè)計緩解。
模板一致性對模型性能至關(guān)重要，訓(xùn)練與測試模板不匹配會顯著降低推理準確率，暴露當前RLVR方法在模板魯棒性上的不足。
課程學(xué)習(xí)顯著提升模型在復(fù)雜邏輯謎題上的表現(xiàn)，策略刷新機制加快收斂并提高最終精度，驗證了分階段訓(xùn)練的有效性。
獎勵設(shè)計對模型訓(xùn)練影響顯著，部分獎勵在復(fù)雜任務(wù)中優(yōu)于簡單二元獎勵，合理調(diào)整獎勵函數(shù)有助于提升訓(xùn)練穩(wěn)定性和泛化能力。
語言差異導(dǎo)致性能差距，英文訓(xùn)練數(shù)據(jù)普遍優(yōu)于中文，提示未來需針對多語言環(huán)境優(yōu)RLVR策略。
統(tǒng)計顯著性：所有提升均在多次實驗中重復(fù)驗證，顯著優(yōu)于基線，展示了方法的穩(wěn)健性和廣泛適用性。
結(jié)論與展望
- 總結(jié)貢獻：
本文首次系統(tǒng)性揭示多領(lǐng)域強化學(xué)習(xí)推理的內(nèi)在機制和交互效應(yīng)，明確了數(shù)學(xué)、代碼和邏輯推理三領(lǐng)域的協(xié)同與沖突關(guān)系。
創(chuàng)新性地結(jié)合監(jiān)督微調(diào)、課程學(xué)習(xí)和多樣化獎勵設(shè)計，顯著提升了多領(lǐng)域推理模型的性能與泛化能力。
通過詳細的模板一致性和語言敏感性分析，指出了當前強化學(xué)習(xí)推理方法的關(guān)鍵瓶頸和改進方向。
- 局限性分析：
當前研究主要基于7B參數(shù)規(guī)模模型，尚未驗證更大規(guī)模模型的適用性和擴展性。
語言敏感性分析集中于中英文，缺少更多語言的廣泛驗證。
多領(lǐng)域訓(xùn)練中任務(wù)權(quán)重和數(shù)據(jù)比例的自動調(diào)節(jié)機制仍待深入研究，以進一步緩解領(lǐng)域間沖突。
- 未來展望：
探索更大規(guī)模模型和更復(fù)雜任務(wù)的多領(lǐng)域強化學(xué)習(xí)訓(xùn)練，推動模型推理能力向更高層次發(fā)展。
開發(fā)更魯棒的模板設(shè)計和自適應(yīng)訓(xùn)練策略，提升模型在不同應(yīng)用場景下的泛化穩(wěn)定性。
深入研究多語言、多文化背景下的強化學(xué)習(xí)推理，構(gòu)建真正通用的跨領(lǐng)域推理模型。
引入自動化數(shù)據(jù)選擇和任務(wù)調(diào)度機制，優(yōu)化多領(lǐng)域訓(xùn)練過程，最大化協(xié)同效應(yīng)，減少負遷移。
Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
2025-07-22｜Shanghai AI Lab|??15
???http://arxiv.org/abs/2507.16331v1????
????https://huggingface.co/papers/2507.16331????
????https://github.com/Veri-Code/ReForm???
研究背景與意義
- 研究背景隨著大型語言模型（LLMs）在自動代碼生成領(lǐng)域的迅猛發(fā)展，確保生成代碼的正確性成為關(guān)鍵挑戰(zhàn)，尤其是在安全關(guān)鍵領(lǐng)域如醫(yī)療、金融和自動駕駛中。傳統(tǒng)的單元測試和人工代碼審查存在覆蓋不足和依賴專家經(jīng)驗的局限，形式化驗證作為一種數(shù)學(xué)上嚴謹?shù)奶娲桨福芴峁┏绦蛐袨榈膰栏褡C明。然而，現(xiàn)有LLMs在形式化驗證任務(wù)中表現(xiàn)不佳，主要因數(shù)據(jù)稀缺和對人類先驗知識的高度依賴。
- 研究意義本文首次系統(tǒng)探討了如何減少對人類先驗的依賴，通過將LLMs置于形式語言Dafny的環(huán)境中，實現(xiàn)自動且可擴展的形式軟件驗證。該研究不僅突破了傳統(tǒng)依賴大量人工注釋的瓶頸，還為未來實現(xiàn)大規(guī)模、可靠的形式化軟件驗證奠定了基礎(chǔ)。通過自動生成和驗證形式規(guī)范，本文推動了代碼生成向真正語義理解和行為保證的轉(zhuǎn)變。
研究方法與創(chuàng)新
- 技術(shù)方法描述研究設(shè)計了一套端到端自動化的數(shù)據(jù)構(gòu)建和訓(xùn)練管線，核心包括：
- 數(shù)據(jù)構(gòu)建：利用LLMs自動生成Dafny代碼及其形式規(guī)范，結(jié)合Python代碼轉(zhuǎn)換和自動迭代驗證修正，完全去除人工單樣本注釋。
- 基準設(shè)計：構(gòu)建了DafnyComp基準，涵蓋合成的復(fù)雜多函數(shù)程序，支持評估模型的組合推理和跨域泛化能力。
- 訓(xùn)練策略：采用兩階段訓(xùn)練，先通過有限監(jiān)督微調(diào)（SFT）掌握基礎(chǔ)語法和語義，再利用強化學(xué)習(xí)（RL）結(jié)合Dafny自動驗證信號進行開放式探索和策略優(yōu)化。
- 獎勵設(shè)計：創(chuàng)新引入三類獎勵機制——語法正確性獎勵、驗證獎勵和邏輯子集獎勵，后者通過邏輯蘊含關(guān)系衡量生成規(guī)范優(yōu)于或等同于真實規(guī)范，極大促進了模型生成更強、更準確的規(guī)范。
- 創(chuàng)新點突出
- 極大降低人類先驗依賴：完全摒棄自然語言鏈式思維（CoT）和人工注釋，依賴自動化數(shù)據(jù)和系統(tǒng)反饋，實現(xiàn)訓(xùn)練過程的可擴展性。
- 形式語言空間內(nèi)的強化學(xué)習(xí)應(yīng)用：首次將RL反饋完全基于形式驗證器的自動信號，保證了獎勵的準確性和嚴謹性。
- 邏輯子集獎勵機制：創(chuàng)新性地利用形式邏輯關(guān)系指導(dǎo)規(guī)范生成，推動模型超越訓(xùn)練數(shù)據(jù)，發(fā)掘更優(yōu)規(guī)范。
- 小模型有效性驗證：證明了0.5B至14B參數(shù)規(guī)模模型在該任務(wù)中的有效性，挑戰(zhàn)了大型模型獨占優(yōu)勢的常規(guī)認知。
- 理論基礎(chǔ)討論研究基于強化學(xué)習(xí)理論和形式驗證的數(shù)學(xué)邏輯基礎(chǔ)，結(jié)合最新的策略優(yōu)化算法（如GRPO），確保訓(xùn)練過程既能探索新策略，又能穩(wěn)定收斂。形式邏輯中預(yù)條件松弛和后條件強化的驗證機制為獎勵設(shè)計提供了堅實的理論支撐。
實驗設(shè)計與結(jié)果分析
- 實驗設(shè)計
- 模型與數(shù)據(jù)：使用Qwen-2.5架構(gòu)，涵蓋0.5B至14B參數(shù)規(guī)模，訓(xùn)練數(shù)據(jù)包含2萬條自動注釋的Dafny程序。
- 訓(xùn)練流程：先進行有限監(jiān)督微調(diào)，再以Dafny驗證器為反饋信號進行強化學(xué)習(xí)，訓(xùn)練細節(jié)包括采樣溫度、批量大小和學(xué)習(xí)率等均經(jīng)過精細調(diào)優(yōu)。
- 評估指標：采用語法正確率、驗證通過率及規(guī)范優(yōu)越率（SSR）三維度衡量模型性能，特別強調(diào)SSR以體現(xiàn)規(guī)范質(zhì)量提升。
- 結(jié)果分析
- 監(jiān)督微調(diào)效果顯著：即使是0.5B模型，SFT階段也能達到80%以上的語法正確率，優(yōu)于GPT-4o等大型商業(yè)模型。
- 強化學(xué)習(xí)帶來實質(zhì)提升：RL階段不僅提升了語法和驗證通過率，更顯著提高了規(guī)范優(yōu)越率，表現(xiàn)出模型在探索更優(yōu)規(guī)范方面的能力。
- 模型規(guī)模效應(yīng)明顯：隨著模型參數(shù)增長，性能持續(xù)提升，尤其是在驗證通過率和規(guī)范優(yōu)越率上展現(xiàn)出良好的擴展性。
- 探索能力驗證：RL訓(xùn)練產(chǎn)生了超出訓(xùn)練語料的新穎且語義豐富的規(guī)范，證明了RL驅(qū)動的探索有效突破了監(jiān)督學(xué)習(xí)的局限。
- 消除CoT影響：實驗中完全去除自然語言鏈式思維，確保性能提升源于模型在形式語言空間內(nèi)的真實推理能力而非人工提示。
結(jié)論與展望
- 研究貢獻總結(jié)本文提出了一種極大減少人類先驗、依賴自動化形式驗證反饋的訓(xùn)練管線，實現(xiàn)了小規(guī)模LLMs在形式軟件驗證任務(wù)中的突破。通過創(chuàng)新的獎勵設(shè)計和數(shù)據(jù)構(gòu)建方法，模型展現(xiàn)出強大的組合推理和泛化能力，超越了現(xiàn)有商業(yè)模型。該工作為實現(xiàn)大規(guī)模、可靠的自動形式化驗證奠定了堅實基礎(chǔ)。
- 局限性分析
- 數(shù)據(jù)仍主要依賴自動生成和合成，真實世界代碼的多樣性和復(fù)雜度可能導(dǎo)致泛化挑戰(zhàn)。
- Dafny驗證器雖強大，但完備性有限，可能影響?yīng)剟钚盘柕慕^對準確性。
- 訓(xùn)練資源消耗較大，尤其是中大型模型的RL訓(xùn)練，限制了更大規(guī)模模型的探索。
- 未來方法展望
- 探索更豐富的形式語言和驗證工具，提升獎勵信號的全面性和準確性。
- 結(jié)合符號執(zhí)行和靜態(tài)分析等多模態(tài)驗證手段，增強模型對復(fù)雜程序行為的理解。
- 研究更高效的RL算法和模型蒸餾技術(shù)，降低訓(xùn)練成本，推動更大規(guī)模模型的應(yīng)用。
- 拓展到多語言、多范式的形式化驗證，提升跨領(lǐng)域適應(yīng)性和實用價值。
本文轉(zhuǎn)載自?????AI研究前瞻?????，作者：胡耀淇
