ACM ICAIF '26 · 論文配套 demo

看漏斗怎麼做決定

可以重播論文表格背後的實驗紀錄、試一次經過驗證的修改，或把自己的問題送進線上系統。全部都跑在論文用的 250 張合約上，檢索前 4 名，模型是 Gemini 2.5 Flash。

這一頁的每個輸出，都是論文實驗裡實際跑出來的紀錄，用論文的計分程式評分，這裡不會呼叫任何模型。三個系統都用 Gemini 2.5 Flash，看到的是同樣檢索出來的四張合約。題目和系統輸出保留英文原文。

正在載入實驗紀錄…

會改變計算的慣例，由建庫時就寫在合約上的修改來處理，而且執行前要先通過檢查。模型不會改寫程式碼。這一頁呼叫的是線上的驗證器，過程中沒有用到 LLM。

合約 · fic_article_2164

每月貸款還款額

宣告的慣例 · 付款時點（SOFT）

驗證器檢查什麼

result_exprresult / (1 + annual_interest_rate / 12)
invariantresult_new * (1 + annual_interest_rate / 12) == result_old
max_expr_nodes13
  • ✓有上限。運算式的 AST 節點數不超過宣告的數量。
  • ✓安全。只能用白名單裡的名稱：不能 import，不能用 dunder，也不能新增函式呼叫。
  • ✓相符。結果是確定、有限的數值，而且在取樣的輸入上符合宣告的不變式。

程式碼修補 · NPV 的期初期末（概念驗證）

- for t, cf in enumerate(cash_flows, start=1): + for t, cf in enumerate(cash_flows, start=0): Call enumerate ├─ Name cash_flows └─ keyword start └─ Constant 1 → 0 唯一被改到的 AST 節點

只有在比對的片段剛好出現一次，而且修補後的輸出等於 (result + initial_investment) * (1 + discount_rate) - initial_investment 時才會接受。在 RepairBench 上，驗證器擋下 879 個錯誤修補中的 97.7%（20 個誤放，2.3%）。這是有範圍的數值驗證，不是形式上的等價證明。

線上系統。每送出一次，都會實際呼叫 Gemini 2.5 Flash 走完整個漏斗，所以結果可能和實驗紀錄不同：選合約、填數值和判斷歧義都是 LLM 步驟。題目和模型輸出維持英文。
輸入一個金融問題，或從上面選一個論文案例。漏斗會用合約的程式碼算出數字，或是停在某個有名字的出口，告訴你還缺什麼。

按 ⌘/Ctrl + Enter 送出。

進階參數