ACM ICAIF '26 · companion demo

See the funnel decide

Replay the recorded runs behind the paper's tables, try a verified repair, or send your own question to the live system. Everything runs on the paper's 250-contract library with the top 4 contracts retrieved, on Gemini 2.5 Flash.

Every output on this tab is a recorded run from the paper's experiments, scored by the paper's scorer. Nothing here calls a model. All three systems use Gemini 2.5 Flash and see the same four retrieved contracts.

Loading the recorded runs…

A convention that changes the computation is handled by an edit declared on the contract at build time and checked before it runs. The model never rewrites the code. This tab calls the live verifier, which uses no LLM.

Contract · fic_article_2164

Monthly loan payment

principal annual_interest_rate loan_term_years

Declared convention · payment timing (SOFT)

End of period (ordinary annuity)Default. The contract's code is the default, so no edit applies. Beginning of period (annuity-due)Applies the declared output transform once it passes verification.

What the verifier checks

result_exprresult / (1 + annual_interest_rate / 12)

invariantresult_new * (1 + annual_interest_rate / 12) == result_old

max_expr_nodes13

✓Bounded. The expression's AST stays within the declared node count.
✓Safe. Whitelisted names only: no imports, no dunders, no new calls.
✓Matches. Deterministic, finite, and agrees with the declared invariant on sampled bindings.

Code patch · NPV timing (proof of concept)

- 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 the only changed AST node

Accepted only if the pattern occurs exactly once and the patched output equals (result + initial_investment) * (1 + discount_rate) - initial_investment. On RepairBench the verifier rejects 97.7% of 879 wrong patches (20 false accepts, 2.3%). This is bounded numerical validation, not formal equivalence.

Live system. Each send makes real Gemini 2.5 Flash calls through the full funnel, so a result can differ from the recorded runs: selection, binding and ambiguity detection are LLM steps.

Also ask raw Gemini 2.5 Flash (no contracts, no funnel)

Ask a financial question, or pick a case from the paper above. The funnel either computes with a contract's code or stops at a named exit and asks for what it needs.

Context from PDF or notes

Press ⌘/Ctrl + Enter to send.