VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims

Bethel Hall; Sachi Shome; William Eiers

REVIEW 3 major objections 5 minor 22 references

VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2608.10213 v1 pith:RPTUWUS7 submitted 2026-08-10 cs.CE

Bethel Hall , Sachi Shome , William Eiers This is my paper · ORCID

classification cs.CE

keywords LargeLanguageModelsSMTSolversFormalVerificationXBRLFinancialQuestionAnsweringNeurosymbolicReasoningUnsatisfiableCoresClaim

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.'

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

That 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.

Other 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.

The 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.

Referee Report

3 major / 5 minor

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.

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 (3)

[§4.1, §3.4, §3.5] 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.
[§5.1, Table 2] 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.
[§3.5, §3.6, §2] 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.

minor comments (5)

[Figure 4] 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.
[§4.1] 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.
[§3.6] 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.
[Table 3] 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.
[Reproducibility] 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.

Circularity Check

1 steps flagged · score 6.0 of 10

XBRLFiling zero-false-accept claim is partly built into the benchmark: gold labels and VeriFin's formula authority are the same calculation linkbases, so accepted claims equal ground truth by construction once the plan binds correctly; only FinanceBench provides independent evidence.

self definitional [Section 3.5 (Establishing Formula Provenance) and Section 4.1 (Datasets: XBRLFiling)]
"For linkbase-derived subtotals, issuer-declared child concepts and arc weights 𝑤𝑖∈{−1,+1} define the formula directly as 𝑓(𝑥1,...,𝑥𝑛)= Σ𝑛𝑖=1𝑤𝑖𝑥𝑖. ... For each filing we take every target subtotal 𝑝 the calculation linkbase declares, read off the line items {𝑐1,...,𝑐𝑛} it says compose 𝑝 and their signs 𝑤𝑖∈{−1,+1}, and record the identity 𝑝= Σ𝑛𝑖=1𝑤𝑖𝑐𝑖 as ground truth."

On XBRLFiling, the gold answer and the formula used for verification are extracted from the same filing calculation linkbase. Whenever the Verification Planner binds the operands, period, unit, and concept correctly, the Claim Verifier's expected value v_hat=f(x) equals the linkbase identity p, which is the gold label by definition. Therefore any claim accepted as Verified necessarily matches the gold answer; the reported zero false accepts on this benchmark is a restatement of the acceptance check rather than an independent test of formula selection or provenance. The benchmark still exercises planner grounding of period, unit, and concept, but it cannot support the paper's broader claim that the formula authority is established independently of the answer label.

full rationale

The circularity is confined to the XBRLFiling evaluation. In §4.1 the benchmark defines ground truth as p=sum wi ci from the filing's calculation linkbase, and in §3.5 VeriFin derives exactly the same identity as its authorized formula for linkbase-derived subtotals. Hence for correctly grounded plans, v_hat equals the gold value by construction, making the zero-false-accept result on that dataset a near-tautological check of the arithmetic identity rather than a test of independent source verification. The paper guards against the candidate claim influencing grounding, which is good, but the formula authority and the label remain the same artifact. FinanceBench is genuinely independent: VeriFin abstains on 13 of 67 questions and rejects all 17 incorrect decided claims, and this is real evidence of false-accept control. However, with only 17 incorrect FinanceBench cases, the statistical strength is limited, and the headline 'zero observed false accepts' relies heavily on the definitional XBRLFiling result. The core derivation (grounding operands, compiling constraints, Z3 check) is not circular in itself; the circularity is in the benchmark construction that makes the primary empirical claim partly self-confirming. Score 6 reflects partial circularity rather than full equivalence, because the planner and FinanceBench still contribute independent content.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The central verification claim rests on the correctness of the planner's semantic parsing, the authority of XBRL facts and calculation linkbases, the completeness and correctness of the metric registry, and the soundness of Z3. No fitted numerical parameters appear in the core claim, but the retrieval and concept-matching stages contain unstated hyperparameters that affect coverage.

free parameters (3)

lambda (retrieval hybrid weight) = not reported
Weights lexical score against dense similarity in Eq. 1; affects which evidence chunks are retrieved and therefore what the planner can ground, though failures tend to cause abstention rather than false accepts.
K (evidence chunk count) = not reported
Number of evidence chunks selected in §3.2; no value is given in the paper, so the retrieval budget is not reproducible as specified.
concept-matching and plausibility thresholds = not reported
The symbolic label-matching heuristic accepts a concept only when row tokens are a subset of concept label (§3.5), and the third heuristic stage is guarded by an unspecified plausibility check; these rules affect role-to-concept binding and can gate whether a claim is verified or abstained.

assumptions (5)

domain assumption The calculation linkbase accurately represents the issuer's intended subtotal compositions and is an authoritative source for formula authorization.
Used in §3.5 and §4.1 to derive formulas and gold answers for XBRLFiling; if a linkbase is wrong or incomplete, both the benchmark and the verifier share the error.
domain assumption Filed XBRL facts are authoritative and correctly reported by issuers.
Operand values are bound exclusively to filed facts (§3.5); any filing error propagates into the verified value.
domain assumption The curated metric registry definitions, compiled from CFA curriculum materials, are correct and unambiguous.
Registry formulas authorize computations when linkbases do not apply (§3.5, footnote 2); a wrong registry formula can yield a Verified incorrect claim.
domain assumption The LLM-based Verification Planner correctly parses the question into metric, roles, period, unit, and formula source.
Z3's deterministic verdict is conditioned on plan correctness; the paper states in §2 that with a complete and correctly grounded plan, checking is deterministic.
standard math Z3 is sound for quantifier-free real arithmetic.
The Claim Verifier relies on Z3's decision procedure (§3.6); any solver soundness issue would invalidate the Verified verdict.

how reviews work

0 comments

Cite this review

Pith. "Pith review of VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims." pith.science (2026). https://pith.science/paper/RPTUWUS7

@misc{pith2026260810213,
  author       = {Pith},
  title        = {Pith review of: VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RPTUWUS7}},
  note         = {Machine review of arXiv:2608.10213}
}

read the original abstract

Large language models often produce plausible numerical claims from financial filings while using the wrong reporting period, unit, line item, or formula. Verifying such claims requires more than rechecking arithmetic: a verifier must ground the relevant facts, establish the authorized calculation, and determine whether the candidate value follows from both. We propose VeriFin, a neurosymbolic verification framework for numerical financial question answering that grounds operands in filed XBRL facts, derives calculations from the question, filing linkbases, or documented metric definitions, and checks claims using Z3. When a claim is inconsistent, solver-derived unsatisfiable cores identify the conflicting facts, formula, and candidate value, enabling targeted repair. We evaluate VeriFin on XBRLFiling, a new 600-question benchmark constructed from 10-K filings of 28 U.S. companies, and on FinanceBench. On fixed candidate pools shared by all verification methods, VeriFin accepts none of the incorrect claims, whereas the baselines accept 6 to 92 incorrect claims on XBRLFiling's 600 claims and 4 to 21 incorrect claims on FinanceBench's 67 claims. The zero false-accept result persists across multiple answer-generator models. Solver-derived feedback further improves repair, achieving up to 69.9% recovery among true catches. These results show that source-grounded symbolic verification can provide a reliable and auditable acceptance control for LLM-generated financial claims.

Figures

Figures reproduced from arXiv: 2608.10213 by the authors.

**Figure 1.** VeriFin applies formal verification to numerical claims generated by LLMs. For an Apple FY2025 operating-expense query, it retrieves filing evidence and obtains an untrusted candidate claim. A Verification Planner specifies the metric, period, unit, operands, and computation. The Provenance Verifier independently grounds the operands in XBRL facts and authorizes the formula from candidate-independent sources. The Cl… view at source ↗

**Figure 2.** Overview of VeriFin Recent work has improved financial question answering through retrieval, structured XBRL access, calculation tools, and executable programs [7, 8, 10, 17], yet numerical reliability remains a challenge. FinanceBench, XBRL-Agent, and Fin-RATE show that errors continue even when models have access to filings and external tools, particularly when questions require the correct entity, reporting per… view at source ↗

**Figure 3.** An XBRLFiling income-statement numerical ques [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Verification performance on XBRLFiling (n=600) and FinanceBench (n=67) for a fixed set of candidate claims generated by Claude Haiku 4.5. Bars report accepted-claim precision, accuracy, and abstention rate; labels above the bars report false-accept counts. VeriFin is t…

**Figure 5.** Figure 5: Left: Percentage of incorrect claims generated by each LLM and rejected by [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 11 canonical work pages

[1]

Adewale Akinfaderin and Shreyas Subramanian. 2025. VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generation.arXiv preprint arXiv:2512.14744(2025)

arXiv 2025
[2]

Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, et al. 2025. A neurosymbolic approach to natural language formalization and verification. arXiv preprint arXiv:2511.09008(2025)

arXiv 2025
[3]

Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. 2022. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks.arXiv preprint arXiv:2211.12588(2022)

arXiv 2022
[4]

Zhiyu Chen, Wenhu Chen, Charese Smiley, Sameena Shah, Iana Borova, Dylan Langdon, Reema Moussa, Matt Beane, Ting-Hao Huang, Bryan R Routledge, et al

work page
[5]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340

2008
[6]

Dongxin Guo, Jikun Wu, and Siu Ming Yiu. 2026. FinGround: Detecting and Grounding Financial Hallucinations via Atomic Claim Verification.arXiv preprint arXiv:2604.23588(2026)

arXiv 2026
[7]

Shijie Han, Haoqiang Kang, Bo Jin, Xiao-Yang Liu, and Steve Y Yang. 2024. Xbrl agent: Leveraging large language models for financial report analysis. In Proceedings of the 5th ACM International Conference on AI in Finance. 856–864

2024
[8]

Pranab Islam, Anand Kannappan, Douwe Kiela, Rebecca Qian, Nino Scherrer, and Bertie Vidgen. 2023. Financebench: A new benchmark for financial question answering.arXiv preprint arXiv:2311.11944(2023)

arXiv 2023

Show all 22 references

[9]

Yidong Jiang, Junrong Chen, Eftychia Makri, Jialin Chen, Peiwen Li, Ali Maatouk, Leandros Tassiulas, Eliot Brenner, Bing Xiang, and Rex Ying. 2026. Fin-rate: A real-world financial analytics and tracking evaluation benchmark for llms on sec filings.arXiv preprint arXiv:2602.07...

2026 arXiv
[10]

Viet Lai, Michael Krumdick, Charles Lovering, Varshini Reddy, Craig Schmidt, and Chris Tanner. 2025. Sec-qa: A systematic evaluation corpus for financial qa. InProceedings of The 10th Workshop on Financial Technology and Natural Language Processing. 221–236

2025
[11]

Stephanie Lin, Jacob Hilton, and Owain Evans. 2022. Truthfulqa: Measuring how models mimic human falsehoods. InProceedings of the 60th annual meeting of the association for computational linguistics (volume 1: long papers). 3214–3252

2022
[12]

Sewon Min, Kalpesh Krishna, Xinxi Lyu, Mike Lewis, Wen-tau Yih, Pang Koh, Mohit Iyyer, Luke Zettlemoyer, and Hannaneh Hajishirzi. 2023. FActScore: Fine- grained atomic evaluation of factual precision in long form text generation. InProceedings of the 2023 conference on empiric...

2023
[13]

Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. InProceedings of the 2023 Conference on Empirical ...

2023
[14]

Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. InFindings of the Association for Computational Linguistics: EMNLP

2023
[15]

Silu Panda. 2026. FinVerBench: Benchmark Validity and Calibration in Large Language Model Financial Statement Verification.arXiv preprint arXiv:2605.29586 (2026)

2026 arXiv
[16]

Securities and Exchange Commission

U.S. Securities and Exchange Commission. [n. d.]. EDGAR Company Filings. https://sec.gov. Accessed: 2026-07-30

2026
[17]

Xinyu Wang, Jijun Chi, Zhenghan Tai, Tung Sum Thomas Kwok, Hailin He, Zhuhong Li, Yuchen Hua, Muzhi Li, Peng Lu, Suyucheng Wang, et al . 2025. Finsage: A multi-aspect rag system for financial filings question answering. InProceedings of the 34th ACM International Conference on...

2025
[18]

Yan Wang, Xuguang Ai, Jaisal Patel, Xueqing Peng, Fengran Mo, Yupeng Cao, Haohang Li, Mingyu Cao, Lingfei Qian, and Víctor Gutiérrez-Basulto. 2026. AUDITFLOW: Executable Symbolic Environments for Structured Financial Re- porting Verification.arXiv preprint arXiv:2606.03031(2026)

2026 arXiv
[19]

Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. Satlm: Satisfiability-aided language models using declarative prompting.Advances in Neural Information Processing Systems36 (2023), 45548–45580

2023
[20]

Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, et al. 2023. Judging llm-as-a-judge with mt-bench and chatbot arena.Advances in neural information processing systems36 (2023), 46595–46623

2023
[2021]

InProceedings of the 2021 Conference on Empirical Methods in Natural Language Processing

Finqa: A dataset of numerical reasoning over financial data. InProceedings of the 2021 Conference on Empirical Methods in Natural Language Processing. 3697–3711

2021
[2023]

VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims

3806–3824. VeriFin: A Neurosymbolic Framework for Verifying LLM-Generated Financial Claims

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Adewale Akinfaderin and Shreyas Subramanian. 2025. VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generation.arXiv preprint arXiv:2512.14744(2025)

arXiv 2025

[2] [2]

Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, et al. 2025. A neurosymbolic approach to natural language formalization and verification. arXiv preprint arXiv:2511.09008(2025)

arXiv 2025

[3] [3]

Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. 2022. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks.arXiv preprint arXiv:2211.12588(2022)

arXiv 2022

[4] [4]

Zhiyu Chen, Wenhu Chen, Charese Smiley, Sameena Shah, Iana Borova, Dylan Langdon, Reema Moussa, Matt Beane, Ting-Hao Huang, Bryan R Routledge, et al

work page

[5] [5]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340

2008

[6] [6]

Dongxin Guo, Jikun Wu, and Siu Ming Yiu. 2026. FinGround: Detecting and Grounding Financial Hallucinations via Atomic Claim Verification.arXiv preprint arXiv:2604.23588(2026)

arXiv 2026

[7] [7]

Shijie Han, Haoqiang Kang, Bo Jin, Xiao-Yang Liu, and Steve Y Yang. 2024. Xbrl agent: Leveraging large language models for financial report analysis. In Proceedings of the 5th ACM International Conference on AI in Finance. 856–864

2024

[8] [8]

Pranab Islam, Anand Kannappan, Douwe Kiela, Rebecca Qian, Nino Scherrer, and Bertie Vidgen. 2023. Financebench: A new benchmark for financial question answering.arXiv preprint arXiv:2311.11944(2023)

arXiv 2023