Filtration-Compiled Autoformalization of Dynamic Financial Models

Language models can translate mathematical prose into formal statements and produce machine-checked proofs, and they are increasingly used in finance. Such a proof, however, certifies the model as written, not the model intended. In dynamic finance the difference concerns information: a position must be chosen using only what is known when it is taken, and an exercise decision cannot depend on prices not yet observed. A formalization that allows more information than the model specifies can be proved correct and still be financially inadmissible. We show that auditing realized outcomes cannot detect such errors: one realized history is consistent with exponentially many patterns of look-ahead, while two scenarios suffice to expose one. We build the model’s information structure into the formalization procedure, so that every intermediate quantity provably uses only information available at its date, and verify the main theorems in Lean 4. On 2960 synthetic instances, removing only the information rules lowers certified success by 19.8 percentage points, and the procedure then declares 91.5% of look-ahead errors valid. When the model is read from prose, the main residual error is a timing convention the text never states; in an exploratory experiment, requiring a verbatim quotation for each convention eliminated it.