九九热视频精品在线_国产成人mv视频在线观看_国产精品三级一区二区_亚洲精品国产av成拍色拍婷婷_久久伊人一区二区_国产高清精品网站_九九99热久久精品离线6_国产在线一卡2卡三卡4卡免费_日韩美女乱淫aaa高清视频_亚洲大胆_啪啪一级视频_午夜av免费观看_国产高清精品福利私拍国产写真_亚洲婷婷五月综合狠狠_日韩欧美一区二区三区视频_岛国av免费看_精品国产乱码久久久久久久软件_亚洲国产成人精品无码区99_www日本色_免费黄色看片

現(xiàn)在，數(shù)學(xué)輔助證明工具都用上了大模型。

「我預(yù)計(jì)，如果使用得當(dāng)，到 2026 年，AI 將成為數(shù)學(xué)研究和許多其他領(lǐng)域值得信賴的合著者。」數(shù)學(xué)家陶哲軒在之前的一篇博客中說道。陶哲軒這樣說了，也這樣做了。他最近一直在用 GPT-4、Copilot、Lean 等工具進(jìn)行數(shù)學(xué)研究，并且還在 AI 的幫助下發(fā)現(xiàn)了自己論文中的一處隱藏 bug。

不僅如此，前幾天，陶哲軒表示：對(duì)多項(xiàng)式 Freiman-Ruzsa 猜想（PFR）的證明進(jìn)行形式化的 Lean4 項(xiàng)目成功完成，并且耗時(shí)僅三周時(shí)間。Lean 編譯器也報(bào)告該猜想符合標(biāo)準(zhǔn)公理，可以說這是計(jì)算機(jī)和 AI 輔助證明的一項(xiàng)巨大成功。

關(guān)于上述研究的更多內(nèi)容，感興趣的讀者可以參考《陶哲軒用 AI 形式化的證明究竟是什么？一文看懂 PFR 猜想的前世今生》?？吹竭@，細(xì)心的讀者可能已經(jīng)發(fā)現(xiàn)了端倪，陶大神在進(jìn)行數(shù)學(xué)研究時(shí)，多次都提到過 Lean。簡單來講，Lean 是一種可幫助數(shù)學(xué)家驗(yàn)證定理的編程語言，用戶可以在其中編寫和驗(yàn)證證明。相比初代 Lean，現(xiàn)在最新的 Lean 4 版本進(jìn)行了多項(xiàng)優(yōu)化，包括更快的編譯器、改進(jìn)的錯(cuò)誤處理和更好的與外部工具集成的能力等。在數(shù)學(xué)領(lǐng)域被廣泛使用的 Lean，在大模型（LLM）刷屏的今天，兩者有沒有更好的結(jié)合方式呢？現(xiàn)在已經(jīng)有人實(shí)現(xiàn)了，開放平臺(tái) LeanDojo 團(tuán)隊(duì)（關(guān)于 LeanDojo，可參考「AI 大模型幫陶哲軒解題，還能證明數(shù)學(xué)定理了？」）和加州理工學(xué)院的研究者推出了 Lean Copilot，這是一款專為 LLM 與人類交互而設(shè)計(jì)的協(xié)作工具，旨在通過人機(jī)協(xié)作給出 100% 準(zhǔn)確的形式化數(shù)學(xué)證明。

值得注意的是，LeanDojo 團(tuán)隊(duì)的研究主要集中在使用 LLM 自動(dòng)化定理證明方面，從這點(diǎn)也不難看出，他們推出的 Lean Copilot 和 LLM 相關(guān)也不會(huì)令人吃驚。

對(duì)于這項(xiàng)研究，大家除了說 Cool，就是 very cool，評(píng)價(jià)還是很高的。

在 Lean 中使用 LLM，加快數(shù)學(xué)證明速度一直以來，自動(dòng)化定理證明面臨重重困難，傳統(tǒng)上，數(shù)學(xué)證明依賴于手工推導(dǎo)，需要細(xì)致的驗(yàn)證?，F(xiàn)在隨著 AI 的進(jìn)步，研究者開始借助人工智能進(jìn)行深入探索，但又免不了出現(xiàn)這種問題，即 LLM 在數(shù)學(xué)和推理任務(wù)中有時(shí)不是很靠譜，容易出現(xiàn)錯(cuò)誤和幻覺。Lean Copilot 允許用戶在 Lean 中使用大型語言模型來自動(dòng)化證明過程，從而顯著加快證明合成的速度，在必要時(shí)還允許人類無縫介入和修改，從而在機(jī)器和人類智力之間提供平衡的協(xié)作。Lean Copilot 允許在 Lean 中使用 LLM 來使證明自動(dòng)化，如策略建議（suggesting tactics）、前提（premises）以及搜索證明（searching for proofs）。用戶可以選擇使用 LeanDojo 提供的內(nèi)置模型，或者導(dǎo)入自己的模型。這些模型可以在本地運(yùn)行（無論是否有 GPU），或者在云端運(yùn)行。

簡而言之，Lean Copilot 為用戶提供了一個(gè)靈活的方式，通過引入 LLM 來增強(qiáng)和優(yōu)化在 Lean 中進(jìn)行定理證明的過程。Lean Copilot 的主要特點(diǎn)可總結(jié)為：LLM 能夠提出證明步驟，搜索證明，并從大型數(shù)學(xué)庫中選擇有用的引理。Lean Copilot 可作為 Lean 包進(jìn)行設(shè)置，并且能夠無縫地在 Lean 的 VS Code 工作流中運(yùn)行。用戶可以使用 LeanDojo 中的內(nèi)置模型，或者使用自己的模型，這些模型可以在本地（有或沒有 GPU）或云端運(yùn)行。該工具可在各種平臺(tái)上運(yùn)行，包括 Linux、macOS 和 Windows WSL。為了使 LLM 更易于 Lean 用戶使用，Lean Copilot 希望能夠啟動(dòng)一個(gè)正反饋循環(huán)：證明自動(dòng)化將帶來更好的數(shù)據(jù)，并最終提高 LLM 在數(shù)學(xué)上的性能。Lean Copilot 效果展示大家可以根據(jù)官方教程配置 Lean Copilot，配置好后就可以進(jìn)行實(shí)驗(yàn)了。項(xiàng)目作者也給出了一些官方示例。