在人工智能研究中數(shù)學(xué)推理一直被視為衡量機器智能的重要試驗場。傳統(tǒng)自動定理證明和數(shù)學(xué)軟件更多依賴人工定義規(guī)則、搜索策略或預(yù)置題庫系統(tǒng)本身并沒有“提出問題”的能力。而“開放世界多智能體環(huán)境中的自主數(shù)學(xué)發(fā)現(xiàn)”這個方向嘗試讓多個智能體在一個可持續(xù)探索的數(shù)學(xué)環(huán)境中自己生成猜想、驗證猜想、尋找反例并在多輪博弈中不斷修正結(jié)論。它不是讓你給模型背答案而是讓模型學(xué)會像研究者一樣發(fā)現(xiàn)問題再用嚴謹工具確認問題。本文將圍繞一條可落地的技術(shù)主線展開如何使用 Python 構(gòu)建一個“提議-驗證-攻擊-裁決”的多智能體數(shù)學(xué)發(fā)現(xiàn)環(huán)境。在這個環(huán)境里提議者負責生成數(shù)學(xué)猜想驗證者使用符號計算或數(shù)值采樣檢查猜想攻擊者主動尋找反例裁判負責終結(jié)無意義的爭論。整個過程是開放式的智能體可以不斷引入新的數(shù)字域、新的運算規(guī)則和新的關(guān)系約束從而形成一個可持續(xù)擴展的自主發(fā)現(xiàn)閉環(huán)。這個方向適合以下讀者正在做多智能體協(xié)作框架選型的算法工程師希望把大模型接入數(shù)學(xué)驗證工具鏈的研究者以及想在強化學(xué)習(xí)或群體智能項目里加入“共同推理”機制的開發(fā)者。讀完本文后你會得到一個最小可運行的 Python 工程骨架理解每個智能體扮演的角色知道如何讓系統(tǒng)真正運行起來也了解它距離自動化數(shù)學(xué)研究還有哪些工程差距。1. 先想清楚為什么自主數(shù)學(xué)發(fā)現(xiàn)需要多智能體環(huán)境1.1 單智能體做數(shù)學(xué)發(fā)現(xiàn)的三個瓶頸單個智能體直接做數(shù)學(xué)發(fā)現(xiàn)時最容易出現(xiàn)的問題是“自說自話”。它可能生成一個結(jié)構(gòu)看起來很漂亮的結(jié)論但由于缺少外部檢驗常常把偶然的數(shù)值巧合當作一般規(guī)律。例如一個模型在 1 到 100 的整數(shù)范圍內(nèi)驗證了某個不等式成立就認為它是全局定理實際上第 101 個數(shù)就是反例。這種問題不能單純靠更大規(guī)模的模型解決。數(shù)學(xué)發(fā)現(xiàn)包含兩個不同性質(zhì)的任務(wù)生成候選結(jié)論和驗證候選結(jié)論。生成是發(fā)散性的驗證是收斂性的。單個模型很難同時扮演這兩種角色讓生成者去驗證它會傾向于維護自己寫出的結(jié)論讓驗證者去生成它會變得保守失去探索能力。把兩個角色拆開讓不同智能體負責不同目標函數(shù)是工程上的自然選擇。第二個瓶頸是局部搜索。一個智能體如果只在一個固定數(shù)字域里探索很容易陷入自己熟悉的模式反復(fù)提出類似猜想。開放世界環(huán)境則需要智能體有能力跳出現(xiàn)有邊界去改變數(shù)字域、改變運算規(guī)則、改變關(guān)系約束。這種“跳出舒適區(qū)”的動作只有在環(huán)境中存在競爭或激勵差異時才會穩(wěn)定發(fā)生。第三個瓶頸是可信度。數(shù)學(xué)發(fā)現(xiàn)的最終產(chǎn)物應(yīng)該是可驗證的命題而不是自然語言表述的“感覺”。單智能體輸出一段文字說這個猜想成立沒有結(jié)構(gòu)化表達也沒有工具參與校驗后續(xù)人類無法復(fù)查。多智能體環(huán)境中加入驗證者和裁判角色后每個結(jié)論都帶上了驗證記錄可信度會明顯提高。1.2 把“開放世界”理解成可擴展的狀態(tài)空間這里的“開放世界”并不是指一個圖形化的 3D 場景而是指數(shù)學(xué)生成環(huán)境的狀態(tài)空間可以動態(tài)擴展。環(huán)境內(nèi)部維護一組數(shù)學(xué)對象比如整數(shù)、有理數(shù)、模數(shù)、圖、函數(shù)以及一組操作符比如加法、乘法、取模、連接。智能體可以建立新的對象并把新對象加入環(huán)境供后續(xù)回合使用。從工程實現(xiàn)上看開放世界環(huán)境至少需要三層抽象對象層保存當前環(huán)境中的數(shù)學(xué)實體每個實體有類型和值。規(guī)則層保存可用的運算規(guī)則規(guī)則定義了輸入類型、輸出類型和求值函數(shù)。關(guān)系層保存智能體關(guān)心的關(guān)系例如“相等”“整除”“同余”“小于”以及已經(jīng)被驗證或證偽的命題記錄。與傳統(tǒng)封閉題庫不同環(huán)境本身不預(yù)先知道哪些結(jié)論是正確的。它的職責是提供計算工具和存儲記錄讓智能體在探索過程中逐步積累知識。這也是“自主數(shù)學(xué)發(fā)現(xiàn)”區(qū)別于“自動求解已知問題”的核心差異。1.3 多智能體在這里不是聊天群而是角色分工模型很多項目把多個大模型實例放在一起讓它們互相聊天美其名曰多智能體系統(tǒng)。這種做法在開放世界數(shù)學(xué)發(fā)現(xiàn)里效率很低因為每個智能體沒有明確的生存目標消息很快會漂移成泛泛而談。真正有效的多智能體環(huán)境每個角色必須有獨立的效用函數(shù)和決策邊界。在本文的框架中環(huán)境內(nèi)部至少存在四類角色角色核心目標典型行為失敗表現(xiàn)提議者生成新猜想數(shù)量優(yōu)先于質(zhì)量構(gòu)造表達式、關(guān)系、邊界條件重復(fù)陳舊猜想驗證者對給定猜想執(zhí)行確定性檢查或高精度檢查符號化簡、數(shù)值采樣、定理調(diào)用誤判為真攻擊者尋找反例驗證猜想邊界隨機搜索、邊界掃描、遺傳搜索只做隨機數(shù)生成裁判判斷論戰(zhàn)是否收斂決定記錄或終止匯總驗證記錄和反例證據(jù)偏袒某個角色這種結(jié)構(gòu)類似工業(yè)界的“紅隊對抗”提議者提出一個假設(shè)攻擊者負責打掉它驗證者負責給出專業(yè)結(jié)論裁判負責維護交流協(xié)議。它并不是為了熱鬧而是為了讓每個智能體的失敗都能被其他角色發(fā)現(xiàn)并糾正。2. 設(shè)計一套可運行的“提議-驗證-攻擊-裁決”框架2.1 消息不是自然語言而是結(jié)構(gòu)化 Hypothesis 對象多智能體系統(tǒng)最容易踩的坑是讓智能體之間傳遞自然語言。數(shù)學(xué)表達對精確性要求極高一句話里含糊一點整個推導(dǎo)鏈條就全錯了。因此在工程實現(xiàn)中智能體之間的所有通信都應(yīng)當使用結(jié)構(gòu)化對象本文統(tǒng)一稱為Hypothesis。一個 Hypothesis 至少包含四個字段id假設(shè)的唯一編號用于追溯。expression數(shù)學(xué)表達式使用 Python 可求值的字符串或 AST。domain這個假設(shè)適用的集合例如整數(shù)集、正整數(shù)集、模 7 整數(shù)集。relation關(guān)心哪種關(guān)系例如“對一切 xexpression(x) 為真”還是“存在某個 x 使 expression(x) 成立”。用 Python 表示如下from dataclasses import dataclass, field from typing import List, Any dataclass class Hypothesis: id: str expression: str domain: str relation: str # forall 或 exists variables: List[str] constraints: dict field(default_factorydict) status: str pending # pending / verified / refuted / disputed這個對象在提議者生成后立即廣播給驗證者和攻擊者。驗證者在同一個對象上執(zhí)行檢查攻擊者在這個對象上生成反例搜索。裁判最后根據(jù)兩者返回的記錄更新 status。2.2 環(huán)境黑板讓智能體共享歷史而不是各自記憶每個智能體如果只在本地維護自己的歷史知識的復(fù)用就會很弱。提議者提出的猜想被驗證為真后攻擊者下一次搜索應(yīng)該避開已被驗證的區(qū)域同樣的被證偽的表達式模式也應(yīng)該被記錄下來。為了實現(xiàn)這一點環(huán)境內(nèi)部設(shè)計一個共享黑板保存所有歷史命題和驗證記錄。黑板的數(shù)據(jù)結(jié)構(gòu)可以設(shè)計成以 Hypothesis id 為主鍵的字典值為驗證記錄集合class Blackboard: def __init__(self): self.records {} def add_hypothesis(self, hypothesis: Hypothesis): self.records[hypothesis.id] { hypothesis: hypothesis, evidence: [] } def add_evidence(self, hypothesis_id: str, evidence: dict): self.records[hypothesis_id][evidence].append(evidence) def get_verified(self): return [ r[hypothesis] for r in self.records.values() if r[hypothesis].status verified ] def get_refuted(self): return [ r[hypothesis] for r in self.records.values() if r[hypothesis].status refuted ]有了黑板之后新的提議者可以查詢已經(jīng)證偽的模式避免重復(fù)提出完全相同的猜想。驗證者也可以參考歷史證據(jù)如果某個表達式曾經(jīng)在高精度數(shù)值采樣中失敗它可以選擇更快地返回 refuted。2.3 回合制調(diào)度一輪發(fā)現(xiàn)中每個智能體只做一件事為了防止智能體之間互相阻塞或無限爭論調(diào)度器采用回合制。每個回合包含四個階段每個階段由對應(yīng)角色執(zhí)行一次動作Round N: 1. Proposer proposes 1 new hypothesis. 2. Verifier checks numeric/symbolic status. 3. Attacker searches for counterexamples. 4. Judge aggregates evidence and sets status.這種設(shè)計借鑒了游戲開發(fā)中的固定時間步長調(diào)度。每個角色在一個回合內(nèi)只做有限計算系統(tǒng)整體保持確定性和可控性。否則一旦攻擊者陷入大規(guī)模搜索整個環(huán)境的推進就會被卡住。class DiscoverySession: def __init__(self, proposer, verifier, attacker, judge, blackboard): self.proposer proposer self.verifier verifier self.attacker attacker self.judge judge self.blackboard blackboard def run_round(self, round_id: int): hyp self.proposer.propose(self.blackboard.get_refuted()) self.blackboard.add_hypothesis(hyp) verify_result self.verifier.check(hyp) self.blackboard.add_evidence(hyp.id, verify_result) attack_result self.attacker.attack(hyp) self.blackboard.add_evidence(hyp.id, attack_result) final_status self.judge.decide(hyp, verify_result, attack_result) self.blackboard.update_status(hyp.id, final_status) return final_status這個 minimal 調(diào)度器已經(jīng)能讓系統(tǒng)跑起來。后續(xù)所有擴展例如并行提議、多攻擊者協(xié)同、驗證緩存等都可以在保持回合結(jié)構(gòu)不變的前提下加入。3. Python 環(huán)境準備與工程骨架搭建3.1 依賴選擇符號計算、數(shù)值計算、基礎(chǔ)工具庫實現(xiàn)這個框架不需要重型深度學(xué)習(xí)框架。核心依賴是 Python 3.9 以上版本搭配 sympy 做符號驗證和表達式化簡numpy 做向量化數(shù)值采樣pydantic 或 dataclass 做結(jié)構(gòu)化通信對象。推薦環(huán)境清單如下依賴用途安裝命令sympy符號化簡、模式匹配、安全表達式求值pip install sympynumpy大規(guī)模候選點采樣、數(shù)組計算pip install numpypydantic假設(shè)對象校驗與序列化pip install pydanticpytest驗證器和裁決邏輯測試pip install pytest學(xué)習(xí)環(huán)境可以直接在 Jupyter Notebook 中運行。生產(chǎn)環(huán)境建議使用 Python 3.11 或 3.12安裝依賴前先鎖定版本文件避免 sympy 和 numpy 版本不兼容導(dǎo)致表達式解析行為變化。3.2 項目目錄結(jié)構(gòu)為了讓這個工程具備擴展性建議按角色拆分模塊而不是把所有邏輯寫在一個文件里math_discovery_env/ ├── core/ │ ├── __init__.py │ ├── hypothesis.py # 假設(shè)對象定義 │ ├── blackboard.py # 共享黑板 │ └── session.py # 回合調(diào)度器 ├── agents/ │ ├── __init__.py │ ├── proposer.py # 提議者 │ ├── verifier.py # 驗證者 │ ├── attacker.py # 攻擊者 │ └── judge.py # 裁判 ├── domains/ │ ├── __init__.py │ ├── integer_domain.py # 整數(shù)域 │ ├── modular_domain.py # 模數(shù)域 │ └── poly_domain.py # 多項式域 ├── experiments/ │ └── run_discovery.py # 運行入口 └── tests/ ├── test_verifier.py └── test_session.py3.3 早期協(xié)議先用“通用規(guī)則”跑通最小系統(tǒng)不要一開始就接入大模型。這個階段的目標是讓多智能體框架在簡單數(shù)學(xué)域中工作即使智能體邏輯非常幼稚。可以先實現(xiàn)一個固定規(guī)則提議者它根據(jù)預(yù)設(shè)模版生成猜想例如“對任意正整數(shù) nn 是奇數(shù)則 n^2 是奇數(shù)”class RuleProposer: def __init__(self): self.counter 0 def propose(self, refuted_hypotheses): self.counter 1 expression x ** 2 1 return Hypothesis( idfhyp_{self.counter}, expressionexpression, domainpositive_integers, relationforall, variables[x] )這里提議者雖然傻但它已經(jīng)能進入完整的驗證循環(huán)。等系統(tǒng)跑通后可以逐步替換成基于大模型的提議者讓它生成更有探索性的表達式。早期協(xié)議的重要性在于排除“框架問題”和“模型能力問題”的混淆如果你一開始就接入大模型出現(xiàn) bug 時很難判斷是框架錯了還是模型錯了。4. 核心代碼實現(xiàn)四個角色的職責與參數(shù)設(shè)計4.1 提議者從模板生成到開放式探索提議者的核心功能是把“靈光一現(xiàn)”變成一個結(jié)構(gòu)化的 Hypothesis。模板式提議者雖然簡單但它能保證生成內(nèi)容的安全性和可驗證性。在數(shù)字域內(nèi)常用的數(shù)學(xué)表達式模板包括多項式恒等式例如 x^2 y^2 與 (x y)^2 的關(guān)系。整除性關(guān)系例如 n^2 - 1 是否能被 8 整除。同余關(guān)系例如 x^2 mod p 的取值集合。不等關(guān)系例如 x^2 1 2x 是否對全體整數(shù)成立。實現(xiàn)時提議者內(nèi)部維護一個候選運算符池和變量池隨機組合成一個表達式再選擇一個關(guān)系類型生成 Hypothesis。為了防止生成無意義的純隨機字符串應(yīng)該限制表達式深度并確保所有變量在使用前出現(xiàn)在變量列表中。class RandomProposer: def __init__(self, operators, domainintegers, max_depth3): self.operators operators self.domain domain self.max_depth max_depth self.counter 0 def propose(self, refuted_hypothesesNone): self.counter 1 expr self._random_expression(x, depth2) hyp Hypothesis( idfhyp_{self.counter}, expressionexpr, domainself.domain, relationforall, variables[x] ) return hyp注意refuted_hypotheses 參數(shù)在這個簡單實現(xiàn)里暫時沒被使用但在完整系統(tǒng)中應(yīng)該傳入給模型避免重復(fù)提出相同類型的問題。4.2 驗證者用 sympy 做符號校驗用 numpy 做邊界采樣驗證者負責對 Hypothesis 做“確定性檢查”和“高置信度檢查”。確定性檢查適合多項式恒等關(guān)系可以通過 sympy 展開表達式差值看化簡結(jié)果是否為 0。例如要驗證“x^2 1 2x 是否恒成立”可以化簡表達式x**2 1 - 2*x結(jié)果應(yīng)該為(x - 1)**2。import sympy as sp class SympyVerifier: def check(self, hypothesis: Hypothesis): x sp.Symbol(x) try: expr sp.sympify(hypothesis.expression) if hypothesis.relation forall: simplified sp.simplify(expr) return {result: unknown, simplified: str(simplified)} except Exception as e: return {result: error, message: str(e)}對于不確定的情況驗證者需要調(diào)用數(shù)值采樣。采樣點不是均勻取 1000 個隨機數(shù)而是要在邊界處密集取值因為數(shù)學(xué)反例最常出現(xiàn)在“接近邊界”的位置。例如如果 domain 是正整數(shù)采樣應(yīng)該是 1 到 1000 的數(shù)。如果 domain 是實數(shù)則需要對負數(shù)、零、小數(shù)、大數(shù)分別采樣。數(shù)值采樣永遠無法證明“恒成立”但能暴露反例。因此驗證者的返回值必須包含check_type字段區(qū)分是symbolic還是numeric。裁判在決定結(jié)論時對 symbolic 驗證結(jié)果給予更高權(quán)重。4.3 攻擊者給反例搜索加一點策略而不是純隨機攻擊者是最容易出現(xiàn)“看起來在干活實際上沒效果”的角色。如果攻擊者只是生成 uniform 隨機數(shù)它很難發(fā)現(xiàn)邊界反例。更有效的做法是結(jié)合遺傳算法或領(lǐng)域啟發(fā)式規(guī)則。攻擊策略可以拆成三部分邊界掃描在 domain 的邊界附近集中采樣。候選變異從已驗證為真的點出發(fā)加入小的擾動檢查擾動后性質(zhì)是否仍然成立。模式生成根據(jù)驗證者返回的疑似問題點反向構(gòu)造新的測試點。在 Python 中攻擊者可以維護一個候選點隊列class Attacker: def __init__(self, rngNone): self.rng rng or np.random.default_rng() def attack(self, hypothesis: Hypothesis): expr hypothesis.expression counterexamples self._search_counterexamples(expr, hypothesis.domain) if counterexamples: return {result: refuted, counterexamples: counterexamples[:5]} return {result: not_found, counterexamples: []} def _search_counterexamples(self, expr, domain): examples [] # 邊界和中心采樣策略 candidates list(range(1, 100)) [10**6, 10**9] for val in candidates: x val if not self._check_expression(expr, x): examples.append(x) return examples實際運行中攻擊者的搜索時間應(yīng)該被限制。每個 Hypothesis 最多允許 1000 次采樣或 0.5 秒計算時間避免整個會話被卡住。4.4 裁判用加權(quán)證據(jù)決定命題狀態(tài)裁判是最終裁決者。它讀取驗證者的符號結(jié)果、數(shù)值采樣結(jié)果和攻擊者給出的反例列表然后決定該 Hypothesis 的狀態(tài)。設(shè)計一個簡單但嚴謹?shù)牟脹Q邏輯如果存在反例直接判定為refuted。如果 sympy 給出確定性的符號化簡結(jié)果且證明等式恒成立判定為verified。如果只有數(shù)值采樣沒有反例且采樣數(shù)量超過閾值判定為disputed表示有初步支持但還沒得到證明。如果驗證者和攻擊者都沒有結(jié)果判定為disputed。class Judge: def decide(self, hypothesis, verify_result, attack_result): if attack_result[result] refuted: return refuted if verify_result.get(result) verified: return verified if verify_result.get(result) unknown and attack_result[result] not_found: return disputed return pending裁判的價值在于把“數(shù)值上沒找到反例”和“數(shù)學(xué)上證明了正確性”區(qū)分開。很多初級實現(xiàn)把兩者混為一談最后輸出的所謂定理其實只是“在采樣范圍內(nèi)沒被發(fā)現(xiàn)錯誤”。這會讓整個系統(tǒng)的可靠性下降。4.5 把四個角色接入調(diào)度器最后把四個角色組合成完整的發(fā)現(xiàn)會話def main(): blackboard Blackboard() proposer RandomProposer(operators[, *, **], domainpositive_integers) verifier SympyVerifier() attacker Attacker() judge Judge() session DiscoverySession(proposer, verifier, attacker, judge, blackboard) for round_id in range(10): status session.run_round(round_id) print(fRound {round_id}: {status})運行后你會在終端看到每個回合的命題狀態(tài)變化。這個最小系統(tǒng)已經(jīng)能讓“規(guī)則提議者”提出猜想由驗證者和攻擊者檢查并由裁判歸檔結(jié)論從而形成自主發(fā)現(xiàn)的完整循環(huán)。5. 運行驗證跑通一輪并檢查結(jié)果質(zhì)量5.1 最小驗證用一個已知結(jié)論驗證框架判斷能力為了確認框架沒有邏輯錯誤建議先準備一個已知為真的數(shù)學(xué)事實。例如“對任意整數(shù) nn^2 不等于 2 mod 4”。這個結(jié)論很容易用符號方法驗證攻擊者也找不到反例。將這個結(jié)論以 Hypothesis 形式手動放入黑板運行驗證者和攻擊者確認裁判狀態(tài)輸出為verified。known_true Hypothesis( idknown_true_1, expression(x**2 - 2) % 4, domainintegers, relationforall, variables[x] ) # 期望 verify_result 為 symbolic verified # 期望 status 為 verified這個測試能快速發(fā)現(xiàn)基礎(chǔ)錯誤比如表達式解析失敗、模運算域未定義、裁判狀態(tài)轉(zhuǎn)換邏輯寫反等。5.2 再測一個已知為假的猜想看看反例會不會被抓住另一個關(guān)鍵測試是傳入一個錯誤命題例如“對任意正整數(shù) nn^2 n 41 總是素數(shù)”。這個命題在 n 較小時成立但當 n 40 時結(jié)果是 1681 41 * 41這是經(jīng)典反例邊界。攻擊者的邊界掃描策略應(yīng)該能在候選點中覆蓋這個位置。如果攻擊者沒有返回反例問題通常出在采樣范圍過小或沒有覆蓋邊界值。解決方法是把采樣策略從“均勻隨機”調(diào)整為“等比數(shù)列 特殊值列表”并將諸如 40、41、42 這類常見反例點加入候選集。5.3 驗證指標不要只統(tǒng)計通過率要看探索覆蓋率衡量一個自主發(fā)現(xiàn)系統(tǒng)不能只記錄“驗證通過了多少個猜想”。更有價值的指標包括指標含義計算方式新假設(shè)率提議者生成與歷史假設(shè)不重復(fù)的比例重復(fù)假設(shè)數(shù) / 總假設(shè)數(shù)反例攻擊命中率攻擊者返回反例的假設(shè)比例被證偽數(shù) / 參與攻擊數(shù)驗證置信度已驗證假設(shè)中符號驗證占比符號驗證數(shù) / 已驗證數(shù)探索覆蓋率新變量、新操作符、新域出現(xiàn)頻率環(huán)境變化計數(shù)器這些指標缺一不可。只有通過率高說明提議者太保守只有新假設(shè)率高說明提議者太發(fā)散。要在探索性和可靠性之間取得平衡最好的辦法是讓攻擊者樣本數(shù)和驗證者采樣數(shù)成為可調(diào)參數(shù)并觀察系統(tǒng)輸出隨參數(shù)變化的情況。6. 常見問題排查從現(xiàn)象定位到根因6.1 假設(shè)對象校驗失敗表達式中存在未知符號現(xiàn)象運行驗證者時拋出sympy.SympifyError或NameError提示y未定義。可能原因提議者在變量列表中沒有聲明所有變量而驗證者直接把字符串傳給 sympy 求值。處理方式在Hypothesis創(chuàng)建時對變量列表做嚴格校驗驗證者在解釋表達式前先用 sympy 的symbols()顯式初始化變量再從作用域中查詢表達式里的自由符號確保所有自由符號都在變量列表中。def _validate_variables(expr: str, variables: List[str]): free_symbols {str(s) for s in sp.sympify(expr).free_symbols} declared set(variables) if not free_symbols.issubset(declared): raise ValueError(fFree symbols {free_symbols - declared} not declared)6.2 數(shù)值采樣沒有找到反例但狀態(tài)被判為 verified現(xiàn)象攻擊者跑了 10000 次隨機采樣沒有反例裁判直接判定為 verified。原因驗證者的返回值里包含了result: verified字段但它的邏輯只做了數(shù)值采樣沒有做符號化簡。裁判無法區(qū)分“已證明”和“未發(fā)現(xiàn)反例”。處理方式在驗證者中增加check_type字段。數(shù)值采樣階段不能返回verified只能返回maybe或not_found。只有 sympy 化簡或定理證明接口返回確定性結(jié)果時才允許返回verified。裁判端再做一次最終校驗。6.3 探索過程發(fā)散提議者不斷提出無意義的復(fù)雜表達式現(xiàn)象10 輪后黑板里全是x**7 y**3 - x*y**2 1這類混亂表達式驗證者和攻擊者只能勉強執(zhí)行但系統(tǒng)沒有積攢任何有價值的結(jié)論。原因提議者的表達式深度和復(fù)雜度沒有限制導(dǎo)致生成的 Hypothesis 超出了現(xiàn)有驗證器能力范圍。處理方式在提議者中設(shè)置復(fù)雜度評分表達式深度超過閾值時直接重新生成。同時提供一個“溫度參數(shù)”控制表達式中的操作符數(shù)量。對純模板生成的表達式建議先使用限定操作符集合、*、**、%并限制指數(shù)不超過 3。這樣能夠保證每個假設(shè)至少是“可分析”的。6.4 裁判只依賴攻擊者結(jié)果導(dǎo)致命題狀態(tài)反復(fù)橫跳現(xiàn)象同一個假設(shè)攻擊者偶發(fā)采樣到反例時狀態(tài)為 refuted下一輪攻擊者隨機采樣沒找到反例狀態(tài)又變回 disputed。原因裁判沒有保存歷史裁決結(jié)果每一輪都根據(jù)當前攻擊結(jié)果重新決定。處理方式裁決邏輯應(yīng)該是單調(diào)的——一旦某個假設(shè)被 refuted就不能再變回 verified 或 disputed。實現(xiàn)時在 Judge 的 decide 方法中加入狀態(tài)機判斷并且建議把攻擊結(jié)果緩存到黑板上避免重復(fù)計算。問題現(xiàn)象常見原因檢查方式處理建議表達式校驗失敗變量列表與表達式自由符號不一致打印 free_symbols 與 variables校驗變量聲明沒有反例卻被判為真驗證者把數(shù)值采樣當成證明檢查 check_type 字段數(shù)值采樣只能返回未發(fā)現(xiàn)系統(tǒng)生成過于復(fù)雜提議者沒有復(fù)雜度控制統(tǒng)計表達式節(jié)點數(shù)設(shè)置深度和操作符上限狀態(tài)反復(fù)橫跳裁判沒有歷史記憶查看同一 id 的多條記錄狀態(tài)機單調(diào)更新7. 最佳實踐從最小原型走向可信賴的數(shù)學(xué)發(fā)現(xiàn)環(huán)境7.1 先讓環(huán)境“可信”再讓模型“聰明”許多團隊拿到 “自主數(shù)學(xué)發(fā)現(xiàn)” 這個題目后第一反應(yīng)就是接入一個大型語言模型讓模型直接輸出數(shù)學(xué)猜想。這種做法的風(fēng)險在于模型輸出帶有隨機性而驗證環(huán)境如果本身不可信最終結(jié)論就完全無法依賴。工程上正確的順序是先讓環(huán)境具備可信驗證能力再逐步替換智能體內(nèi)部邏輯。早期使用規(guī)則模板生成假設(shè)用 sympy 做確定性檢查用人工已知反例測試驗證器和攻擊者確保基礎(chǔ)設(shè)施沒錯之后才讓模型承擔提議和攻擊中的策略部分。這樣即使模型輸出質(zhì)量不高環(huán)境也能兜底不會把錯誤結(jié)論當作定理保存下來。7.2 使用黑板緩存驗證結(jié)果避免重復(fù)計算數(shù)學(xué)探索過程中大量假設(shè)在結(jié)構(gòu)上是相似的。例如x^2 1和(x1)^2 - 2x在化簡后可能等價。如果每次都對這類假設(shè)重新做符號化簡和數(shù)值采樣計算成本會線性膨脹。黑板系統(tǒng)可以緩存表達式規(guī)范化后的摘要鍵已經(jīng)驗證失敗的表達式模式可以直接被拒絕。def _normalize_expr(expr: str): x sp.Symbol(x) return sp.srepr(sp.sympify(expr))使用srepr獲取表達式的規(guī)范表示形式比使用字符串拼接更可靠因為x1和1x會在規(guī)范化后變成同一個鍵。7.3 限制每個智能體的單輪預(yù)算保證系統(tǒng)可控多智能體環(huán)境里的智能體如果不受資源限制任何一個角色的死循環(huán)都可能拖垮整個會話。實際工程建議為每個角色設(shè)置獨立的預(yù)算包括時間預(yù)算、采樣點預(yù)算和調(diào)用次數(shù)預(yù)算。例如攻擊者每輪最多采樣 2000 點驗證者每輪最多執(zhí)行 2 秒符號計算提議者每輪最多生成 3 個候選假設(shè)。這樣做除了防止失控還讓系統(tǒng)時間可預(yù)期便于調(diào)試和壓測。注意限制預(yù)算不只是為了性能更是為了語義清晰。當命題狀態(tài)是 disputed 時如果沒有預(yù)算限制你無法區(qū)分“搜索得不夠久”和“確實沒有反例”的區(qū)別。有了預(yù)算每一輪驗證結(jié)果都附帶了搜索強度信息便于后續(xù)分析。7.4 生產(chǎn)環(huán)境還需要補上日志、監(jiān)控和回滾如果這個系統(tǒng)要長期運行那么建議輸出結(jié)構(gòu)化日志把每個假設(shè)的ID、表達式、驗證結(jié)果、攻擊結(jié)果和裁決狀態(tài)記錄為 JSON 行。這樣后續(xù)可以重放某一段探索過程分析提議者策略的變化是否有效。{event: hypothesis_verified, id: hyp_001, expr: x**2 % 4, check_type: symbolic} {event: counterexample_found, id: hyp_002, value: 40}7.5 三個可以直接落到自己項目里的做法如果你的項目只是想利用這個框架的一部分能力建議從下面三個做法開始把“提議者”和“驗證者”拆成獨立服務(wù)通過消息隊列通信。這樣可以方便地把數(shù)學(xué)發(fā)現(xiàn)能力嵌入流水線而不是在一個進程里強行耦合。把驗證者從 sympy 擴展到更專業(yè)的定理證明工具。先定義統(tǒng)一驗證接口再為不同工具寫適配器避免把環(huán)境綁定到某個具體庫。給攻擊者加入強化學(xué)習(xí)策略。攻擊者在不斷尋找反例的過程中實際上是在做獎勵稀疏的搜索。把它訓(xùn)練成一個能優(yōu)先在“可疑區(qū)域”采樣的策略網(wǎng)絡(luò)是目前這個方向比較自然的大模型接入點。8. 擴展方向從數(shù)字游戲走向自動化數(shù)學(xué)研究目前這套最小系統(tǒng)只能處理簡單的數(shù)字域和表達式關(guān)系。真正要讓多智能體環(huán)境做出更有價值的數(shù)學(xué)發(fā)現(xiàn)還需要三個層面的擴展。第一層是領(lǐng)域擴展。除了整數(shù)和多項式新的領(lǐng)域可以包括密碼學(xué)里的有限域、代數(shù)中的群論、拓撲中的圖結(jié)構(gòu)以及組合數(shù)學(xué)中的格路徑。環(huán)境每增加一個新的領(lǐng)域就必須同時提供對應(yīng)的規(guī)則、驗證工具和攻擊策略工作量不小但每個領(lǐng)域都能帶來新的研究問題。第二層是證明生成。當前框架只能判斷一個命題是否被反例推翻或者是否能用符號化簡驗證。真正的數(shù)學(xué)發(fā)現(xiàn)要求系統(tǒng)在 verified 狀態(tài)下能夠生成證明軌跡而不僅僅是返回一個布爾值。這意味著驗證者需要記錄完整推導(dǎo)步驟并把步驟結(jié)構(gòu)化存儲。這是向自動定理證明延伸的關(guān)鍵路徑。第三層是智能體之間的長期協(xié)作。當智能體數(shù)量增多后提議者可以依賴其他角色的歷史結(jié)果繼續(xù)做更復(fù)雜的抽象。例如在某個子問題被證明后提議者可以把該命題作為“引理”組合進更大的假設(shè)中。這種層次化推理能力是開放世界環(huán)境相比封閉題庫的最大優(yōu)勢。如果讀者想從最小工程開始練習(xí)建議順序是先把本文的框架在本地跑通再用 sympy 替換驗證器增加兩個數(shù)字域然后接入一個開源大模型作為提議者最后加入日志和可視化。每一層擴展都能獨立驗證而不是推到重來。這個方向真正困難的不是讓智能體說出一個結(jié)論而是讓它學(xué)會在一個擁有驗證、反例、爭論和證據(jù)的開放世界里不斷修正自己的判斷。多智能體機制的價值就在這里每個角色都有不同的功利目標它們的博弈讓系統(tǒng)的結(jié)論更加接近數(shù)學(xué)研究“可證明、可復(fù)現(xiàn)、可承認”的標準。