FormaFin: Solver-Verified Loan Covenant Monitoring with a Small Language Model

A 7B covenant formalizer trained with SFT, then GRPO with a solver-checked reward.

FormaFin turns a financial covenant from a loan agreement into an SMT-LIB formula covenant_holds(...) over the line items of the borrower's compliance certificate. The Z3 solver then answers a lender's quarterly questions exactly:

1. Status: comply, breach, or undetermined
2. Earnings cushion: how far earnings (e.g. EBITDA) can fall before a breach
3. Debt capacity: how much more debt the borrower can take before a breach

The model is a LoRA adapter on Qwen2.5-Coder-7B-Instruct. It is small enough to run in-house on one GPU, so confidential certificate figures never reach a model: they enter the solver as facts. Code, data and the benchmark: https://github.com/verifiedfinance/loan-agent.

Adapters in this repository

Folder	Training	Benchmark score
rl_v2_s42 (recommended)	SFT, then GRPO with the interface-gated solver reward, seed 42	95.0
rl_v2_s43	same, seed 43	96.2
rl_v2_s44	same, seed 44	93.8
sft789	SFT only (789 teacher-written pairs)	85.8
rl_v1	first GRPO run, reward without the interface gate (kept for reproducibility; not recommended)	58.4

rl_v2_s42 is the pre-registered run; seeds 43 and 44 replicate it. Each folder has a training/ subfolder with the exact run configuration, trainer state and per-sample reward logs.

Usage

import torch
from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer

repo, sub = "bethelhall/formafin", "rl_v2_s42"
tok = AutoTokenizer.from_pretrained(repo, subfolder=sub)
base = AutoModelForCausalLM.from_pretrained("Qwen/Qwen2.5-Coder-7B-Instruct", torch_dtype=torch.bfloat16, device_map="auto")
model = PeftModel.from_pretrained(base, repo, subfolder=sub).eval()

SYSTEM = ("Translate the real financial covenant into SMT-LIB2. Return exactly a set-logic command and one "
          "define-fun named covenant_holds that returns Bool and is true exactly when the borrower complies.")
PROMPT = """Covenant clause:

{clause}

Write (define-fun covenant_holds (<parameters>) Bool <body>) with EXACTLY these parameters, in this order and with
these types (do not add, rename or drop any):
{params}
Amounts are in US dollars as reported in the borrower's compliance certificate; test_date is the test date as an
integer YYYYMMDD (e.g. 20121231), so a threshold that changes over time is written with test_date comparisons.
covenant_holds is true exactly when every financial covenant in the clause that applies on test_date is satisfied.
Return only the SMT-LIB2 (set-logic QF_NRA or QF_LIA/QF_LRA as needed, then the define-fun)."""

clause = "The Borrower shall maintain at all times a Total Debt to EBITDA Ratio of not more than 3.0 to 1.0."
params = "(total_debt Real) ; Consolidated Total Debt\n(ebitda Real) ; Consolidated EBITDA\n(test_date Int) ; test date as YYYYMMDD"
messages = [{"role": "system", "content": SYSTEM},
            {"role": "user", "content": PROMPT.format(clause=clause, params=params)}]
inputs = tok.apply_chat_template(messages, add_generation_prompt=True, return_tensors="pt", return_dict=True).to(model.device)
out = model.generate(**inputs, max_new_tokens=1024, do_sample=False)
formula = tok.decode(out[0][inputs["input_ids"].shape[-1]:], skip_special_tokens=True)
print(formula)

Pass the parameter list exactly: one Real per certificate line item (name and description), then test_date as Int, then one Bool per condition flag. A formula whose parameters differ cannot be evaluated.

Checking a certificate with Z3 (pip install z3-solver):

import re, z3

smt = re.sub(r"```\w*", "", formula)
smt = smt[smt.index("(define-fun"):]                      # keep only the definition
decls = "(declare-const total_debt Real)(declare-const ebitda Real)(declare-const test_date Int)"
facts = "(assert (= total_debt 453900000.0))(assert (= ebitda 149800000.0))(assert (= test_date 20121231))"

def holds(extra=""):
    s = z3.Solver()
    s.from_string(smt + decls + facts + extra)
    return s.check() == z3.sat

complies = holds("(assert (covenant_holds total_debt ebitda test_date))")
print("comply" if complies else "breach")               # Total Debt / EBITDA = 3.03 > 3.0: breach

The earnings cushion and debt capacity come from a bisection over the varied item with the same check; the full evaluator (status including undetermined, cushion, capacity) is src/headroom/headroom.py in the GitHub repository.

Training

• SFT. A teacher model wrote formulas for 1,000 financial-ratio clauses from EDGAR credit agreements. A pair was kept only if Z3 parses it, a semantic review accepts it, and every parameter has one grounded comment: 789 pairs. LoRA rank 16, alpha 32, all attention and MLP projections, 1 epoch, learning rate 1e-4.
• GRPO (TRL) on 586 further unlabeled clauses (no answers), from the SFT adapter, 1,000 steps, 4 samples per clause, temperature 0.8, learning rate 5e-6, no KL penalty. The reward needs no labels and no judge model:
  • interface gate: 0 unless the formula keeps exactly the required parameters and Z3 parses it;
  • solver score s: for every limit written in the clause (e.g. debt / EBITDA <= 3.0), Z3 tests the formula just inside the limit (compliance must be possible), at it, and just outside it (a breach must be forced);
  • reward = 0.3 + 0.7 x s.

Evaluation

Borrower-disjoint benchmark: 143 covenant clauses from borrowers that never appear in training, 1,064 compliance certificates (constructed, since delivered quarterly certificates are not public). Score: mean per-clause share of the three questions answered correctly.

System	Size	Score	Earnings cushion
Qwen2.5-Coder-7B, reads the clause and answers directly	7B	64.8	33.7
Qwen2.5-Coder-32B, reads directly	32B	85.8	75.6
Qwen3.8-27B, reads directly	27B	88.8	84.8
FormaFin SFT + Z3	7B	85.8	78.3
FormaFin SFT + GRPO + Z3 (3 seeds)	7B	95.0 ± 1.2	88.1 ± 3.2

GRPO adds +9.2 points over SFT (all three seeds, Holm-corrected p < 0.001). 71% of the RL formulas are proven equivalent to the reference reading by Z3 for every possible certificate, and when two independently trained seeds produce formulas that Z3 proves equivalent (92% of clauses), those formulas are correct 97.9% of the time: a label-free check of which covenants can run unattended.

Limitations

• Benchmark certificates are constructed; references are two agreeing model readings validated through Z3, not expert annotations.
• Each certificate line item is given as one amount; applying an agreement's definitions (add-backs, caps) to raw financial statements is not covered.
• GRPO was trained only on clauses without date schedules or condition flags; on clauses that have them, it does not improve on SFT.
• Agreements come from US public companies (EDGAR, mostly 1996–2008). Always verify a formula before relying on it; this is a research artifact, not financial or legal advice.

Data and licenses

Clauses come from the loan-agreement text data of Ganglmair and Wardlaw (CC BY 4.0; "Complexity, Standardization, and the Design of Loan Agreements", SSRN 2952567). The base model, Qwen2.5-Coder-7B-Instruct, is released under Apache 2.0; its terms apply to the combined model.