OProver 係一個圍繞 Lean 4 建立的形式化證明框架，重點唔係單次叫模型「寫答案」，而係讓系統一邊嘗試、一邊讀取已驗證證明，再根據編譯器回饋反覆修正。對非研究背景讀者來講，可以理解成 AI 做數學題時，不只交卷一次，而係會睇提示、改錯，再重新整理答案。

實際使用上，這個專案較適合已有 Lean 4 或機器學習環境的人：一類會用它做證明推理與驗證流程，另一類會直接研究訓練管線、資料建構同檢索庫管理。儲存庫同時提供模型與資料方向，包括 OProver-8B、OProver-32B，以及 OProofs 語料，較適合想評估模型表現、重現論文流程，或建立自家證明代理系統的團隊。

它要解決的核心問題，是形式化證明往往唔能夠靠一次生成成功，尤其 Lean 4 對語法、型別同邏輯正確性要求非常嚴格。OProver 的特別之處，在於把「找相似證明」、「接收編譯器錯誤訊息」同「多輪修補」由臨時技巧，變成訓練時已經學會的整體策略，這點比只在推理階段追加外掛模組更完整。

• 支援多輪修正，而唔係只生成一次證明
• 會利用已驗證證明作檢索參考，提升命中率
• 透過 Lean 4 伺服器做機械驗證，結果更可靠
• 提供 CPT、SFT、RL 等訓練流程，覆蓋研究到實作
• 附帶大型 OProofs 資料集，方便分析 pass@k 與修復軌跡

以公開資訊看，OProofs 規模相當大，包含 1.77M 個 Lean 陳述、6.86M 個經編譯器驗證的證明，亦保留失敗嘗試與後續修復過程，這對研究「模型點樣由錯變對」尤其有價值。論文亦提到它在 MiniF2F、ProverBench、PutnamBench 等基準有突出表現；不過這類成果仍主要面向形式化數學、定理證明研究者，同一般應用型開發者的距離會稍遠。

GitHub： https://github.com/multimodal-art-projection/OProver

Paper： https://arxiv.org/pdf/2605.17283

如果你對「AI識答數學題」有興趣，SU-01是一個幾有代表性的案例。它是一個 30B-A3B 推理模型，目標不是單靠背答案，而是嘗試完成較長步驟、較講求證明結構的數學與科學題目，尤其接近競賽題風格。

對一般讀者而言，最易理解的用法，是把它當成一個專注於複雜解題的模型來看，而不是萬能聊天機械人。官方資訊顯示，模型已公開權重，亦有技術報告與專案頁面；如果你本身會用 Hugging Face 一類平台，就可以進一步了解它的輸出表現與測試方式。

SU-01較特別的地方，在於它不依賴外部工具、寫程式執行，或者專門符號求解器，仍然想把長鏈條推理做好。訓練上，它用了較有策略的資料排序方式，以及分兩階段強化學習，先追求可驗證答案，再逐步改善證明質素，這點對處理多步驟題目尤其重要。

• 重點放在數學、物理等需要嚴謹步驟的解題
• 嘗試處理長篇推理與證明修正，而非只輸出最終答案
• 在 IMO 2025（第66屆國際數學奧林匹亞）、USAMO 2026(美國數學奧林匹亞）、IPhO 2024/2025 有高水準成績
• 相關模型可留意同類推理系統，例如 DeepSeek-R1、OpenAI o1 類型模型，以及其他數理導向大型語言模型

如果你是研究員、教育科技開發者，或者想比較不同推理模型在高難度題目的差異，SU-01很值得觀察。對一般學生來說，它未必是即開即用的溫習工具，但作為理解 AI 如何由「識答題」走向「識證明」的例子，參考價值相當高。

整體來看，SU-01吸引之處不只在分數，而是在方法上走一條相對簡潔統一的路線。從公開資料判斷，它更像是一個展示「後訓練如何提升嚴謹推理」的研究型專案，適合關心 AI 推理上限的人細看。

網址： https://github.com/Simplified-Reasoning/SU-01

HiDream-O1-Image 是一個開源影像生成模型，主打把文字、圖片像素和不同任務條件放進同一個系統處理。對一般用家來說，可以將它理解為一個不只會「生圖」，亦能處理改圖、角色一致化，甚至長文字排版的多功能工具。

實際使用上，它較適合拿來做文字生成圖片、按指令修改現有圖片，或者用同一角色、產品去延伸出不同場景。官方亦提供 Hugging Face 上的模型與線上體驗，因此未必一定要自行搭建環境先感受到效果。

這個專案最值得留意的創新，是它採用所謂 Pixel-Level Unified Transformer，聲稱不依賴外部 VAE 或分開的文字編碼器。簡單講，即是想用更統一的方法直接理解像素與文字，理論上有助減少不同模組之間的割裂，對複雜提示、版面安排和文字渲染會更有幫助。

• 支援text-to-image、圖片編輯、主體個人化等多種任務
• 可原生輸出最高 2048×2048，較適合需要細節的畫面
• 內建 reasoning-driven prompt agent，強調先處理布局與隱含需求
• 提供 8B 規模版本，並有 distilled 與 undistilled 變體

若你常做海報草圖、分鏡、品牌角色延伸，這類模型會特別實用；如果重視圖片內長文字、指定區域排版，HiDream-O1-Image 亦屬值得關注的一類。不過實際效果仍會受提示寫法、任務類型和版本選擇影響，尤其編輯任務方面，官方就建議優先考慮完整模型。

硬體需求

GPU：需要 CUDA 支援的 NVIDIA GPU 。模型本身有兩個版本 — 標準版（Full）和蒸餾版（Dev）。標準版需要 50 個推理步驟，蒸餾版則需要 28 個步驟，因此蒸餾版對硬體的需求更低。

根據社群資訊，使用 FP8 量化的蒸餾版本可以用約 10GB VRAM 的 GPU 運行 。如果使用全精度模型（Full），VRAM 需求會更高，具體取決於生成的影像解析度（最高支持 2048×2048）。

軟體依賴

安裝後需要執行 pip install -r requirements.txt 。官方強烈建議安裝 flash-attn 以優化注意力運算，如果無法安裝，則需要手動編輯 models/pipeline.py 第 291 行，將 "use_flash_attn": True 改為 "use_flash_attn": False，否則推理會失敗 。

推理模式選擇

• Dev 模式（蒸餾版）：28 步，guidance scale 為 0.0，適合資源受限的環境
• Full 模式（標準版）：50 步，guidance scale 為 5.0，品質更高但運算成本更大

網址 https://github.com/HiDream-ai/HiDream-O1-Image

網址 https://huggingface.co/HiDream-ai/HiDream-O1-Image

如果你想要一個不一定依賴雲端、又能理解圖片同影片內容的 AI，MiniCPM-V 系列會幾值得留意。它屬於多模態模型，即是可以同時處理文字、影像，部分版本更進一步支援語音同即時串流互動。

實際使用上，它比較適合做圖片問答、文件與畫面內容理解、影片片段分析，甚至可延伸到手機上的 AI 助手。根據專案資料，MiniCPM-V 4.6 可部署到 iOS、Android 同 HarmonyOS，對想做裝置端應用的團隊尤其實際。

這個專案最值得講的，是它不只追求效果，亦非常重視效率。MiniCPM-V 4.6 只有 1.3B 參數，但官方表示表現可超越部分更大的模型，並透過 intra-ViT early compression 把視覺編碼計算成本降低五成以上，對手機或邊緣裝置來說相當關鍵。

另一條支線 MiniCPM-o 4.5 則更著重即時互動，支援視覺、語音、文字一齊運作，並有全雙工串流能力，即是「睇、聽、講」可以同步進行，不用等其中一項完成先再回應。這類設計特別適合即時助理、陪伴互動或主動提醒場景。

重點摘要：
– MiniCPM-V 4.6：主打高效率影像與影片理解，偏向手機端部署
– MiniCPM-o 4.5：加入語音與即時多模態互動，功能更全面
– 視覺壓縮技術有助減少運算成本，對流暢度與耗電更有幫助
– 適合 OCR、畫面理解、行動助理、即時視聽互動等場景
– 相關模型可留意 Gemma4-E2B-it、Qwen3.5-0.8B、Gemini 2.5 Flash、LLaVA-UHD v4

整體來看，MiniCPM-V 系列的吸引力不只是「開源」，而是它把多模態 AI 拉近到真正可落地的裝置使用。若你重視本地運行、回應速度同跨平台部署，這個專案比起單純追求大型模型規模，方向更加清晰。

Source: https://github.com/OpenBMB/MiniCPM-V

Relit-LiVE 是一個用來幫影片「重新打燈」的研究型專案。簡單講，就是把原本影片中的人物或場景，在不改動內容主體下，換成另一種光線效果，並盡量保持整段影片前後一致，不會一時光、一時暗。

這個專案較特別的地方，是它不依賴預先知道鏡頭姿態，並且會一同生成重打燈影片與環境光影片。這種做法有助提升物理一致性，令反光、陰影等細節看起來更合理，對比只逐格處理的方式，更重視時間上的穩定。

實際使用上，它目前較適合有 NVIDIA GPU 的使用者，官方亦建議至少 24GB VRAM，代表一般人未必適合在普通手提電腦直接試。現階段已提供推論程式與模型權重，但訓練流程、完整 inverse-forward pipeline，以及 Gradio 介面似乎仍未完全公開。

如果你是做影像研究、生成式影片實驗，或者想測試影片後期中的光照控制，這類工具會幾有參考價值。它未必是即開即用的消費級產品，但對需要高質感光影變化、又想減少畫面閃爍的人來說，方向相當清晰。

• 主要用途是把現有影片重新套用新的光照效果
• 重點創新是聯合生成環境光影片，提升連貫性與真實感
• 已公開推論代碼與 checkpoints，適合先做效果驗證
• 硬件要求偏高，較適合研究者或進階創作者
• 相關模型資訊可見權重路徑提到的 Wan2.1-T2V-1.3B，亦有 Hugging Face 模型發佈頁可供參考

整體來看，Relit-LiVE 最吸引之處不只是「換光」，而是嘗試令影片中的光影變化更像真實世界。若你關心影片生成中的物理合理性、時間穩定性，以及反射和陰影表現，這個專案值得加入觀察名單。

Source: https://github.com/zhuxing0/Relit-LiVE

seal-rg/streaming 是一個研究型專案，核心概念是令大型語言模型不再只按單一路徑逐步讀、想、答，而是把輸入、推理過程與輸出拆成多條「stream」並行處理。對一般讀者來說，可以理解成模型一邊讀題、一邊解題，甚至另一條路同時做檢查，減少傳統逐字等待的阻塞感。

實際使用上，這個儲存庫不是即開即用的聊天工具，而是分成三個可獨立運行的實驗資料夾，分別研究效率、安全性及可監察性。若你是研究員或工程團隊，可以按目標選擇對應部分，例如想測試「邊讀邊答」就看效率章節，想研究提示攻擊防護則集中安全章節。

它最有意思的創新，在於多串流共用權重的設計：不是為每條思路各自建一個完整模型，而是在同一模型內並行安排多個資訊通道。README 顯示它涵蓋 2、3 甚至 10 個 streams，並把思考、使用者輸入與模型輸出拆開處理；其中較大型版本還提到每個 stream 的 Gated-DeltaNet 狀態，顯示作者不只追求速度，亦想提升內部行為的可觀察程度。

• 三個重點面向：效率、安全、可監察性
• 相關模型包括：Qwen2.5-7B、Qwen3-1.7B、Qwen3-4B、Qwen3-8B、Qwen3.5-27B
• 已知實驗名稱包括：Stream-8B、Stream-27B
• 評估任務涵蓋 GSM8K、MATH500、SQuAD、PubMedQA、TensorTrust、IFEval 等

最適合的應用場景，是想研究下一代 LLM 推理流程的人，而不是只想部署一般客服機械人。特別是需要同時兼顧回答速度、抗攻擊能力，以及想更清楚監察模型「正在怎樣想」的團隊，這個專案提供了相當具體的實驗框架；不過它主要仍屬研究代碼，實際產品化前應預期要自行整合與驗證。

使用方法
這個模型需要 自定義推理代碼（標準 Hugging Face Transformers 不能直接支援 Multi-Stream 格式），推薦使用官方推理代碼。

Source: https://github.com/seal-rg/streaming