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