Skip to content

VERAFI: Verified Agentic Financial Intelligence through Neurosymbolic Policy Generation

🕒 Published (v1): 2025-12-12 17:17 UTC · Source: Arxiv · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

VERAFI is a neurosymbolic agentic RAG framework for financial QA that addresses post-retrieval reasoning errors by embedding formally-specified SMT-lib financial policies (GAAP, SEC) directly into agent prompts as in-context constraints. It achieves 94.7% factual correctness on FinanceBench-style tasks, an 81% relative improvement over a dense-retrieval-with-reranking baseline. The neurosymbolic policy layer alone contributes +4.3 percentage points over the agentic baseline without it.

Problem

Standard RAG systems fail not at retrieval but during reasoning: even with correct documents retrieved, LLMs commit arithmetic errors, temporal inconsistencies, and regulatory compliance violations in the generation phase. Prior agentic RAG work (e.g., Multi-HyDE) reduces hallucinations but cannot prevent post-generation logical errors when the model has correct context but reasons incorrectly over it.

Method

VERAFI has three integrated stages:

  1. Dense retrieval + reranking: Qwen3-Embedding-4B encodes queries and documents; top-15 candidates are reranked to top-3 using Jina-reranker-v3 cross-encoder.
  2. Agentic financial reasoning: Claude Sonnet 4 via the Strands framework, equipped with a symbolic calculator, Python REPL, and Tavily web search, performs multi-step financial computations with explicit tool invocations and source citations.
  3. Policy-guided generation (neurosymbolic layer): Financial domain constraints (80+ rules) are autoformalised into SMT-lib specifications using LLM-based translation (Amazon Bedrock Automated Reasoning checks), then embedded as dual-representation context—both the SMT-lib expression and a natural-language alternate—into the agent's system prompt. Policies act as soft in-context constraints during generation, not post-hoc formal verification.

Key Contributions

  • Neurosymbolic autoformalization of financial validation requirements (GAAP, SEC) into SMT-lib format, generating 80+ machine-readable constraint rules.
  • Policy-guided agentic generation: formally-specified policies injected into the agent's prompt context so constraints guide reasoning during (not after) generation.
  • Empirical ablation on FinanceBench-style tasks isolating retrieval, agentic, and neurosymbolic contributions.

Results

  • VERAFI (full): 94.7% factual correctness, 96.4% completeness
  • Agentic RAG w/ web search (no neurosymbolic): 90.4% factual correctness
  • Dense + Reranker (no agent): 52.4% factual correctness
  • RAG only dense: 33.3% factual correctness
  • Neurosymbolic layer contribution: +4.3 pp over agentic baseline
  • Best retrieval (Dense+Rerank): Recall@3 = 0.667, NDCG@3 = 0.486; BM25 alone: Recall@3 = 0.095
  • Evaluation set: four companies (American Water Works, AMD, American Express, Boeing) from ConvFinQA/FinanceBench; judge: Amazon Bedrock LLM-as-a-Judge (Claude 3.7 Sonnet v1)

Limitations

  • Evaluation dataset is narrow: four companies, limited filing years; generalizability to broader financial corpora is undemonstrated.
  • Policies act as soft in-context constraints, not hard formal verification—violations are not caught or rejected post-hoc; the agent can still ignore them.
  • Evaluation methodology (Bedrock LLM-as-a-Judge with Claude 3.7) differs from prior work (RAGAS + GPT-4), making direct numerical comparisons unreliable.
  • Retrieval ceiling remains at 66.7% Recall@3; ~33% of queries receive incomplete context, and the system cannot fully compensate.
  • The 80+ rule set is manually curated for GAAP/SEC; extension to other regulatory regimes requires new policy authoring.

Relevance to Harnesses / Meta-Harnesses

VERAFI exemplifies a policy-injection harness pattern: a structured pipeline that wraps a base LLM agent with formally-specified domain policies loaded at runtime and injected into the reasoning context, functioning as a meta-layer that constrains agent behavior without modifying the model. The SMT-lib policy file acts as a machine-readable harness configuration—analogous to a system-level prompt template or rule engine—that is loaded, formatted, and prepended to agent instructions programmatically (see Algorithm 1). This is directly relevant to harness/meta-harness research as a concrete instantiation of how domain-specific validation logic can be encoded externally and applied uniformly across agent invocations, enabling systematic behavior control and auditability without per-query prompt engineering.