FormaFin

FormaFin — LoRA-адаптер на Qwen2.5-Coder-7B-Instruct, который переводит финансовый ковенант из кредитного договора в SMT-LIB формулу covenant_holds(...) над статьями справки о соблюдении ковенантов заёмщика. Солвер Z3 затем точно отвечает на квартальные вопросы кредитора. 7B-модель достаточно мала, чтобы работать в организации на одной GPU.

⚙ Ключевые особенности

• 💼 На входе — текст ковенанта, на выходе — формула SMT-LIB2 с фиксированным набором параметров.
• ✅ Z3 отвечает на три вопроса: статус (comply / breach / undetermined), запас по прибыли (насколько может упасть EBITDA) и запас по долгу.
• 🔒 Конфиденциальные цифры из справок не попадают в модель — они входят в солвер как факты.
• 🎯 Обучение: SFT на 789 отобранных парах, затем GRPO с наградой от солвера — без разметки и без judge-модели.
• 📦 В репозитории несколько адаптеров, рекомендуется rl_v2_s42.

💻 Пример

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

Подробнее

Бенчмарк: 95.0 ± 1.2 у SFT + GRPO + Z3 против 85.8 у SFT и 88.8 у Qwen3.8-27B «в лоб»; GRPO даёт +9.2 пункта.
Справки в бенчмарке сконструированы, а не взяты из реальных квартальных отчётов.
Не покрывает применение определений договора (add-backs, caps) к сырой финансовой отчётности.
GRPO обучен только на клаузах без графиков дат и флагов условий; это исследовательский артефакт, не финансовый или юридический совет.