> I had started looking at HOL due to John's use of it at Intel:
> economists use econometric packages, and finance houses use trading
> or risk management packages that may contain a lot of infelicities
> - JP Morgan, for example, has blamed their recent 'London Whale'
> trading losses on change in their VaR ('value at risk') model.
>
> Interesting! May I offer some advice? I read John's thesis (not too
> carefully), and it really seemed to me that John's work at Intel
> involves John proving actual mathematical theorem for Intel, proofs
> involving floating point algorithms that are very hard for humans to
> check the correctness of. That sounds like a very valuable
> contribution of math to society, but it's not the same as using HOL
> Light to check the correctness of a random computer program.
Thank you Bill.
My thoughts on how to use theorem provers in economics and finance are still
quite nascent. To develop the examples above a bit further:
1. econometric software. McCullough's 2009 chapter in the Handbook of
Computational Econometrics (Belsley & Kontoghiorghes, eds), the main source of
my knowledge in this area, argues that econometric software is usually fairly
informally verified. In some cases (e.g. NIST), there are test datasets, whose
parameters the package should be able to estimate arbitrarily precisely. In
other cases, particular implementations of estimation routines have been
proposed as benchmarks. Thus, econometricians often report results from more
than one estimation package, as a robustness check: there is no formal checking
on the level of "Intel chip such-and-such correctly implements IEEE standard
such-and-such".
2. finance software. Currently, major financial institutions like banks use a
measure called 'value at risk' (VaR) to manage their market risk (i.e. the risk
of price movements in assets like equities). VaR is the preferred measure of
the Basel Committee on Banking Supervision, and has therefore been adopted as a
regulatory requirement in many jurisdictions. Banks wishing to operate in
these jurisdictions can often demonstrate compliance either by using a VaR
model developed by the regulators, or by submitting their own VaR model to the
regulator for approval. As I understand it, the regulator would then 'stress
test' any submitted VaR model on various datasets - likely including actual
historical as well as simulated. Again, though, this is a weaker standard than
a formal verification that a VaR model actually possesses the VaR property.
> How does VaR and the London Whale compare?
It remains unclear to me how much of the JPMorgan / London Whale loss was due
to errors in their VaR model. The press has quoted various risk managers as
saying that it is naïve to believe the change in their model to be more than an
excuse. The New York Times has offered an explanation in terms of more human
factors - a conflict between London and New York trading desks that worsened
when the head of the chief investment office became ill in 2010, and lost
control over her group:
http://www.nytimes.com/2012/05/20/business/discord-at-jpmorgan-investment-office-blamed-in-huge-loss.html?_r=1&pagewanted=all
Whatever the details of the JPMorgan case, it remains the case that checking
risk management models remain informal, and that this may therefore be both
inefficient and introduce operational/model risk.
Best,
Colin Rowat
University of Birmingham
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
