A note on scope: This paper compares FVLM to LLMs because LLMs have become the default tool for many mathematical tasks. This comparison is not meant to suggest one is universally better than the other. LLMs and formally verified systems serve different purposes. LLMs excel at research, creative work, text generation, and exploratory tasks where flexibility matters more than guarantees. Formally verified systems like FVLM are better suited for math-heavy domains like quantitative finance, where correctness is non-negotiable. Think of it like quantum computers versus classical computers: different tools for different problems. Both should coexist. The argument here is that for disciplines requiring mathematical certainty, formal verification should be the default, not an afterthought.
The Problem
In quantitative finance, correctness is non-negotiable. A floating-point error in a derivatives pricing calculation, a silent NaN propagating through a risk model, or a nondeterministic output in a regulatory report can cost millions.
Language models have demonstrated strong capabilities in code generation and natural language understanding. However, they have three fundamental limitations for high-stakes financial computation:
Probabilistic outputs: Language models sample from probability distributions. The same prompt can yield different responses, making reproducibility impossible.
No formal guarantees: A model can generate code that appears correct but contains subtle numerical errors. There is no mechanism to prove correctness.
Silent failure modes: When models fail, they often fail silently. A pricing model might return 0.0847 when the true value is 8.47, a 100x error with no warning.
The industry response has been to add post-hoc validation layers that catch some errors after generation. This approach is backwards. The correct approach: make invalid outputs impossible to generate.