{"id":"1c672498-5e46-453f-adf4-b8a132c86f32","arxiv_id":"2608.10213","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"A neurosymbolic verifier that grounds LLM financial claims in filed XBRL facts and authorized formulas accepted zero incorrect claims across two benchmarks and six answer models.","lead":"VeriFin is a system that checks whether numbers generated by AI models about company filings are supported by the documents themselves, using formal logic rather than a second AI judge. On two financial question benchmarks it accepted no wrong claims, while simpler baselines accepted many, though it declined to render a verdict on some cases.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The headline zero-false-accept result is largely built into the primary benchmark: XBRLFiling labels are the linkbase subtotals and VeriFin's formula authority is the same linkbase, so accepted claims equal ground truth by construction; only FinanceBench's 17 incorrect cases independently test the…","rationale":"The paper's architecture is sound and clearly described: claim generation is decoupled from verification, grounded XBRL facts and authorized formulas are compiled into Z3 constraints, and abstention is an explicit control decision. The reader's CONDITIONAL verdict is reasonable. My concern differs from the reader's stated weakest assumption: rather than the Verification Planner's semantic accuracy being the main risk, the primary experimental benchmark cannot falsify the central claim. Because XBRLFiling's gold labels are exactly the linkbase-declared subtotals, and VeriFin's formula authority for those same subtotals is the same linkbase, any claim that survives verification is correct by construction. The zero-false-accept result on XBRLFiling is therefore a consistency check of the retrieval and planning stages, not an empirical demonstration that source-grounded symbolic verification catches wrong calculations in general. FinanceBench is a genuinely independent check, but it is small: only 17 incorrect claims among 54 decided cases, with 13 abstentions, and no confidence intervals are reported. This does not warrant rejecting the paper, but it does mean the headline claim should be conditioned on an independent benchmark rather than presented as established by the 600-question suite. No ad hominem is intended; the paper is transparent about its construction, and the architecture has real merit. The appropriate verdict remains CONDITIONAL: accept only after the tautological-benchmark concern is addressed with source-independent evaluation or explicit acknowledgment that the primary benchmark tests planner grounding rather than formula authorization.","tokens_in":11825,"tokens_out":6713,"duration_ms":76995,"concrete_test":"Construct an independent ground-truth split: take 100 XBRLFiling questions and withhold the calculation linkbase from VeriFin's formula authority; instead authorize formulas only from the question template or the curated metric registry, and label gold independently from the filed reported subtotal. If VeriFin still records zero false accepts on this split, with FA counts and abstentions reported, the tautology concern is resolved. As a companion check, inject adversarial near-miss claims (previous-year subtotal, scale error ×1000, one omitted component, period shifted by one year) into the fixed candidate pool and verify that every injected incorrect claim is rejected.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing weakness is that XBRLFiling's ground truth and VeriFin's formula source are the same artifact. In §4.1, the benchmark is built by reading from each filing's calculation linkbase the identity p = Σ w_i c_i and labeling p as gold. In §3.4–3.5, VeriFin's formula-authority hierarchy gives priority to the filing's calculation linkbase for exactly these subtotals. Thus, whenever the Verification Planner resolves the question, the solver's expected value v_hat is the gold value by construction; any claim accepted as Verified is correct unless the planner binds the wrong period, unit, or concept. The reported 92/92 rejection therefore tests planner grounding of period, unit, and concept, but it cannot test the paper's broader claim that source-grounded verification controls formula selection and provenance: on this benchmark the formula is not independent of the label. The only source-independent evidence is FinanceBench (54 decided cases containing 17 incorrect claims; 13 abstentions). Zero observed false accepts there is real but statistically weak (upper 95% confidence bound is roughly 16% for 0/17), and no confidence intervals or code artifacts with commit hashes are supplied to rule out planner leakage or prompt inconsistencies. The central 'zero false accept' claim therefore overstates what the 600-question benchmark can establish.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces VeriFin, a neurosymbolic framework that verifies numerical claims produced by LLMs over financial filings. VeriFin grounds each operand in filed XBRL facts, obtains an authorized formula from the question, the filing's calculation linkbase, a curated metric registry, or disclosure text, and then checks the candidate claim with the Z3 SMT solver, returning Verified, Violated, or Abstain. The authors construct XBRLFiling, a 600-question benchmark derived from 10-K calculation linkbases, and also evaluate on a 67-question numerical subset of FinanceBench. Using fixed candidate claims shared by all methods, they report zero false accepts for VeriFin across six answer-generator models, while baseline verifiers accept between 6 and 92 incorrect claims on XBRLFiling and between 4 and 21 on FinanceBench. They further show that solver-derived unsatisfiable cores improve repair of rejected claims, with pass@3 recovery up to 69.9% on XBRLFiling.","tokens_in":12081,"tokens_out":5631,"duration_ms":57782,"significance":"If the central empirical claim were fully supported, VeriFin would be a meaningful contribution: it provides an auditable acceptance control with explicit abstention, and its same-candidate evaluation is a methodologically sound way to isolate verifier behavior from candidate generation. The Judge+Formula baseline is a particularly effective control, showing that providing the correct formula and grounded operands to an LLM judge is insufficient unless they are enforced as hard constraints. The multi-model robustness evaluation and the use of UNSAT cores for repair are also valuable. However, the headline zero-false-accept result is substantially weaker than the paper claims because the primary benchmark is circular with respect to formula authority, and the independent evidence on FinanceBench is statistically thin. With appropriate reframing and additional analysis, the underlying framework remains defensible.","major_comments":[{"comment":"The XBRLFiling ground truth and VeriFin's formula authority are the same artifact. In §4.1, each benchmark label is generated by reading from the filing's calculation linkbase the identity p = Σ w_i c_i; in §3.5, the Provenance Verifier authorizes the formula for linkbase-derived subtotals from that same calculation linkbase. Consequently, on XBRLFiling any claim that satisfies the grounded constraints is correct by construction, provided the Verification Planner binds the right concept, period, unit, and scale. The reported zero false accepts on XBRLFiling therefore test planner grounding but cannot test formula selection or provenance authority, which the abstract and §5.1 credit to the system. Please reframe the central claim or add a benchmark whose gold labels are independent of the formula authority, for example using registry-derived or disclosure-text formulas where the formula is not also the labeling criterion.","section":"§4.1, §3.4, §3.5"},{"comment":"The only source-independent evidence for zero false accepts rests on FinanceBench's 17 incorrect claims among 54 decided cases. With 0 successes in 17 trials, the 95% confidence interval for the false-accept rate extends to roughly 19% (by the rule of three, 3/17), so the data cannot support the paper's stronger statements about a reliable acceptance control. Please report exact confidence intervals for the zero-false-accept rates, for example Clopper-Pearson intervals, and explicitly present the FinanceBench result as preliminary. The 13 abstentions on FinanceBench (19.4% of the 67 questions) should also be discussed as part of the safety-coverage trade-off rather than only as an aside.","section":"§5.1, Table 2"},{"comment":"The zero-false-accept result is conditional on the Verification Planner's semantic parsing. As the paper itself states in §2, 'given a complete and correctly grounded verification plan, VeriFin uses Z3 to deterministically check' the claim; if the planner binds a role to the wrong taxonomy concept, period, or unit, the solver can return Verified for an incorrect claim. Because the zero-false-accept claim is empirical rather than a formal guarantee, the paper should quantify planner-induced failures: report how often plans were misparsed, how those misparses affected the verdicts, and whether any Verified claims were accepted on the basis of a wrong plan. Without this analysis, the conclusion in §5.2 that 'whenever VeriFin establishes the required computation, none of the incorrect candidate claims in our evaluations are accepted' is too strong.","section":"§3.5, §3.6, §2"}],"minor_comments":[{"comment":"The false-accept labels above the bars are easy to misread as percentages; please clarify in the caption that they are counts, or format them distinctly from the percentage bars.","section":"Figure 4"},{"comment":"The paper reports 86 10-K submissions and 15 target subtotals but only 600 questions; please state explicitly how many filings lack a given subtotal, since not all filings report all 15 target subtotals.","section":"§4.1"},{"comment":"The tolerance τ is described as half a unit in the last place reported by the filing, but the constraint Φ shows only |v_hat - v_c| ≤ τ; please clarify how τ is computed when the filing presents figures in mixed scales or when percentages are stated to varying decimal places.","section":"§3.6"},{"comment":"The recovery counts differ slightly between naive and guided conditions (e.g., 230 vs. 231 true catches for Qwen3-30B on XBRLFiling); please clarify whether the naive and guided conditions are scored on the same underlying cases and, if possible, provide a paired comparison.","section":"Table 3"},{"comment":"The anonymous GitHub URL should be replaced with a persistent repository and a commit hash; without this, the machine-checkable reproducibility implied by the evaluation cannot be confirmed.","section":"Reproducibility"}],"recommendation":"major_revision","confidential_remarks":"The paper's main claim needs reframing: the XBRLFiling benchmark cannot validate formula-selection behavior because the labels and formula authority are the same calculation linkbase. The FinanceBench evidence is genuinely independent but statistically weak, so the authors should either gather more incorrect cases or present the result with appropriate confidence bounds. The framework itself is sound and the same-candidate control is a strength; I would be willing to revisit after major revision. I also recommend asking for a persistent code repository with a commit hash at revision time."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The real news is that VeriFin is a clean, working design: it treats LLM claims as untrusted, grounds operands in filed XBRL facts, authorizes formulas from non-generative sources, and pushes the final arithmetic check to Z3. The same-candidate evaluation across Direct LLM, LLM judge, Judge+Formula, and PoT is a good control, and the new XBRLFiling benchmark is a genuinely useful artifact. The UNSAT-core-guided repair loop is a nice contribution, and the paper is honest about the abstention/coverage trade-off.\n\nThat said, the central claim needs reframing. On XBRLFiling, both the gold labels and VeriFin's formula authority come from the same calculation linkbase. An accepted claim therefore agrees with gold by construction once the Verification Planner binds the right concept, period, and unit. So the 92/92 rejection on XBRLFiling tests planner grounding, not the independent-formula-selector part of the claim. The paper is transparent about this in the construction, but the abstract and headline overstate what the 600-question benchmark can establish. The genuinely independent evidence is FinanceBench: 17 incorrect claims per model, zero false accepts across six models (0/102), which is real but statistically thin, and the paper gives no confidence intervals.\n\nOther soft spots are minor by comparison. Correct-claim rejection is substantial (46–73 on XBRLFiling depending on the model), FinanceBench coverage drops to 49–82%, and the repair results are descriptive, with varying counts and no paired tests. These are all disclosed, so I don't consider them load-bearing flaws. What would tighten the paper is releasing code with commit hashes and rephrasing the XBRLFiling result as a validation of the planner plus solver rather than as independent evidence of formula control.\n\nThe related work is accurate and the citation pattern looks fine. This paper deserves a serious referee; the right response is peer review with a request for artifacts and a more careful statistical framing, not desk rejection.","headline":"A clean neurosymbolic verification design with a useful new benchmark, but the headline zero-false-accept result is partly baked into XBRLFiling because gold labels and formula authority share the same linkbase.","tokens_in":12662,"tokens_out":3082,"would_cite":true,"duration_ms":30751,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that a filing-grounded symbolic verifier can make false acceptance of LLM financial claims zero on the fixed candidate pools it evaluates, while baselines admit dozens of incorrect claims.","keywords":["Large Language Models","SMT Solvers","Formal Verification","XBRL","Financial Question Answering","Neurosymbolic Reasoning","Unsatisfiable Cores","Claim Verification"],"falsifier":"Construct a test set from the XBRLFiling questions in which each question is paired with a near-distractor evidence excerpt (the prior year's value in the target row, or the same statement restated in a different display scale such as thousands instead of millions) while the gold answer is kept fixed, then count how many times VeriFin returns Verified for the wrong-period or wrong-scale claim. Any nonzero count would falsify the zero-observed-false-accept claim as a general statement, and a systematic pattern would isolate which planning stage fails.","tokens_in":11587,"feed_emoji":"✅","tokens_out":14184,"duration_ms":122169,"temperature":0.7,"pith_summary":"The paper is trying to establish that acceptance of an LLM's numerical financial claim can be controlled by grounding rather than plausibility: a claim should be marked Verified only when it follows from the filing's own XBRL facts (the standardized machine-readable line items in corporate filings) and from an independently authorized calculation. VeriFin realizes this by parsing the question into a verification plan, binding every operand to a specific reported fact, authorizing the formula from non-generative sources such as the filing's calculation linkbase or a documented metric definition, and checking the resulting arithmetic constraints with the logical constraint solver Z3. On the two benchmarks and six answer-generator models it evaluates, VeriFin records zero observed false accepts, while the baselines accept between 6 and 92 incorrect claims on XBRLFiling and between 4 and 21 on FinanceBench. A secondary result is that the solver's unsatisfiable cores give targeted repair feedback, recovering up to 69.9% of true catches when the generator is asked to fix a rejected claim. The work matters because it makes the audit trail for a numerical financial claim explicit: every accepted number is traceable to a filed fact and an authorized formula, and every refused number comes with a reason.","feed_headline":"A solver-backed verifier accepts zero wrong LLM financial claims","feed_subtitle":"Grounded in filed XBRL facts and authorized formulas, it rejects every bad claim that LLM judges let through.","key_machinery":"The load-bearing object is the verification plan $C=(M,F,R,\\mathbf{u},\\boldsymbol{\\rho},S)$, a tuple naming the target metrics, authorized formulas, operand roles, expected units, reporting periods, and formula sources. The Provenance Verifier binds each operand role to a specific filed XBRL fact by resolving the role to a taxonomy concept through the filing's calculation linkbase (the machine-readable record of which line items sum to which subtotal), a curated concept registry, or a label-matching heuristic; by requiring the fact's reporting period and unit to match the question; and by taking the reported value directly from the filing, never from the LLM. Formula authority follows a strict hierarchy over non-generative sources: explicit operations in the question, the filing's calculation linkbase, a curated metric registry, or an explicit definition in the disclosure text; if no complete and unambiguous formula is authorized, the system abstains. The Claim Verifier then encodes the grounded operands, the authorized formula, and the candidate value, with a tolerance of half a unit in the last reported digit, into quantifier-free real arithmetic for Z3, with named constraints so an unsatisfiable core can identify which filed value, formula condition, or claim bound conflicts.","core_discovery":"VeriFin's core claim is that a fixed numerical claim from an LLM should be treated as untrusted, and that acceptance can be decided deterministically once three things are fixed: which filed XBRL facts supply the operands, which formula is authorized, and what precision the filing reports. With those fixed, the Claim Verifier builds the constraint system $\\Phi=\\bigwedge_i(x_i=m_i^\\star)\\wedge(\\hat v=f(x))\\wedge(|\\hat v-v_c|\\le\\tau)$ and asks Z3 whether it is satisfiable; satisfiable means Verified, unsatisfiable means Violated, and when the necessary facts or a source-backed formula cannot be established, the result is Abstain. On the fixed candidate pools used in the paper, VeriFin returns zero observed false accepts in all twelve model-dataset settings, with 100% accepted-claim precision; it covers 98.8% of XBRLFiling's 600 questions and 80.6% of FinanceBench's 67, with the FinanceBench drop being an explicit abstention rather than an acceptance of uncertainty. The same evaluation shows that giving an LLM judge the correct operands and formula does not enforce them: that baseline accepts 75 of the 92 incorrect XBRLFiling claims, whereas VeriFin's hard constraints accept none.","pith_inferences":["Read as a deployment guarantee, this suggests the zero-false-accept result is best stated as 'no acceptance without source-backed authority' rather than 'no wrong answers,' since open-ended metrics not declared in a filing's calculation linkbase would likely raise abstention.","Because the Verification Planner is the only semantic step, a natural stress test would be to adversarially vary period wording, display scale, and concept labels while keeping the arithmetic identical; any wrong Verified verdicts or increased abstention would localize the residual risk to planning rather than solving.","The named-constraint unsatisfiable-core pattern is generic, so the same separation of candidate proposal from source-grounded symbolic checking could be reused in other domains with machine-readable authoritative formulas, such as tax schedules, regulated energy reporting, or clinical trial arithmetic.","The pass@3 gains suggest that the bottleneck for repeated repair is still generation diversity rather than diagnosis; pairing the core with an explicit instruction to change only the flagged role might recover more true catches without relaxing the acceptance rule."],"forward_implications":["Accepted numerical claims become auditable: each Verified result carries a trace from a specific filed XBRL fact through an authorized formula to the solver's satisfiability check.","Formula grounding plus hard constraints, not arithmetic execution alone, is what controls false accepts: Program-of-Thought still admits incorrect claims, and providing the correct formula to an LLM judge still accepts most incorrect claims.","The framework's abstention is a deliberate control decision: when facts or formula authority cannot be established unambiguously, it returns Abstain and explains what is missing, preventing unsupported numbers from entering a workflow.","Rejected claims can be repaired with solver diagnostics: unsatisfiable cores name the conflicting facts, roles, formula, and claim bound, improving one-shot recovery by up to 39.8 percentage points over generic retry on XBRLFiling.","Coverage cost is explicit: on FinanceBench, coverage falls to 80.6% because the system declines to verify claims it cannot ground or authorize, so the guarantee is best read as 'nothing accepted without filing-backed support,' not 'everything decided.'"],"supporting_citations":[{"why":"Supplies the Z3 SMT solver used by the Claim Verifier to decide satisfiability of the grounded arithmetic constraints.","marker":"[5]"},{"why":"FinanceBench is the public numeric-subset benchmark on which VeriFin's generality beyond the paper's own construction is tested.","marker":"[8]"},{"why":"FinQA's evidence-plus-program format motivates XBRLFiling's design, which inverts the construction by starting from declared XBRL calculations.","marker":"[4]"},{"why":"Program-of-Thoughts is the executable-arithmetic baseline that VeriFin must beat; it still accepts incorrect claims because the model chooses operands and computation.","marker":"[3]"},{"why":"SEC-QA applies Program-of-Thoughts to SEC filings and motivates the need for formal grounding of operands and computation.","marker":"[10]"},{"why":"Provides the public corporate-filing source from which the 10-K submissions and their XBRL calculation linkbases are collected for XBRLFiling.","marker":"[16]"},{"why":"FinGround is the atomic-claim verification approach contrasted with VeriFin's same-candidate evaluation and candidate-independent provenance.","marker":"[6]"}],"fun_headline_variants":["Zero false accepts: Z3 checks LLM financial claims","Neurosymbolic verifier rejects every wrong claim from LLMs","Solver-grounded verification admits zero bad LLM numbers","Z3-based check accepts no incorrect financial claims","LLM financial claims: symbolic proof blocks every false accept"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The system's guarantee rests on the Verification Planner getting the semantic bindings right: if the planner assigns the wrong taxonomy concept, reporting period, unit scale, or authorized formula for any operand, Z3 will faithfully mark the resulting wrong claim Verified, because the solver only checks the plan it was given.","fun_headline_variants_meta":{"raw":{"variants":["Zero false accepts: Z3 checks LLM financial claims","Neurosymbolic verifier rejects every wrong claim from LLMs","Solver-grounded verification admits zero bad LLM numbers","Z3-based check accepts no incorrect financial claims","LLM financial claims: symbolic proof blocks every false accept"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000238,"raw_usage":{"total_tokens":1582,"prompt_tokens":1087,"completion_tokens":495,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":703,"completion_tokens_details":{"reasoning_tokens":414}},"tokens_in":703,"tokens_out":495,"duration_ms":4637,"temperature":1.0,"reasoning_tokens":414,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:10:55.576541+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a test set from the XBRLFiling questions in which each question is paired with a near-distractor evidence excerpt (the prior year's value in the target row, or the same statement restated in a different display scale such as thousands instead of millions) while the gold answer is kept fixed, then count how many times VeriFin returns Verified for the wrong-period or wrong-scale claim. Any nonzero count would falsify the zero-observed-false-accept claim as a general statement, and a systematic pattern would isolate which planning stage fails.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"FinQA's evidence-plus-program format motivates XBRLFiling's design, which inverts the construction by starting from declared XBRL calculations."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"SEC-QA applies Program-of-Thoughts to SEC filings and motivates the need for formal grounding of operands and computation."},{"cited_title":"Securities and Exchange Commission","cited_arxiv_id":null,"evidence_quote":"Provides the public corporate-filing source from which the 10-K submissions and their XBRL calculation linkbases are collected for XBRLFiling."}],"review_version":1}