Formalizing =/= proof. There’s nothing to prove. Don’t change the headline if you don’t know what you’re talking about.
Also it’s funny how this formalization reveals MANY inconsistencies in the law. I have no doubt that the legal system is formally a huge turd. Imagine if they did this for the death penalty. Too bad these computers are controlled by the ultra privileged. Ofc they’re trying to dodge taxes.
The legal system, famously completely deterministic with no human-judgement element whatsoever and therefore modelable as computer code.
LLMs, famously super reliable in the legal field.
sits down with a biiig bucket of popcorn
I can’t wait for somebody to actually try to argue a case with this.
One of the better uses for LLMs is finding a needle in a haystack, where a hard to find but easily verifiable result is buried somewhere in a mass of text. Tax loopholes are obviously harder to verify, and you probably need a lawyer for that, but you don’t need to find them all either.
deleted by creator
Also, a lot of things people refer to as tax loopholes aren’t actually gaps in logic. A lot of them are things that exist for a logical reason, but are being applied in a way that isn’t intentional.
Things like “I own a convenience store, my wife and kids work there” which then gets used when some billionaire spins up a subcontractor of his business, hires his wife and kids as the only employees, and then assigns his house as an asset owned by that business and uses it to siphon away expenses or whatever.
I’m not a tax lawyer either 😛, but the point is that a lot of the loopholes exist for a sensible purpose, but are being chained or applied outside their original purpose.
If only we had some sort of investigative and regulatory arm the would stop silly uses of reasonable laws like that. Oh look; they gutted the IRS budget again… Hmmmmmmmm.
Skimming this, it’s not clear to me what exactly is being done in Lean. It sounds like an LLM is translating the tax code into lean and then using those lean statements. But the translation step is highly error prone. Tax codes are not mathematically complicated (which is what Lean is good for) but logically complicated (which LLMs suck at)
Maybe someone with more patience can chime in
not mathematically complicated but logically complicated
Lean is more than capable of modeling logic.
Lean is capable of modeling formal logic. The jump to legal “logic” is highly questionable.
Not really my point, but sure.
Then what was your point?
Lean helps a lot in formalising advanced mathematics, because it is able to express statements and proofs of that mathematics in a way that most tools can’t, and it can be checked by computer. It doesn’t help much in formalising logically complicated scenarios because you can express those in any old formal language.
If your tax bill depended on the convergence of some gnarly integral, Lean would be great. But it doesn’t; it depends on a billion bits of trivial mathematics composed together with rules that combine to be ambiguous and complicated. No computer environment helps with the ambiguity, whilst any computer environment can formalise that complication once an interpretation has been chosen.
So what formal language do you think would be more appropriate than Lean for this purpose?
PHP.
Half kidding, but you’re asking the wrong questions. Go read my original comment again.
formal methods will always have a huge place in my heart
deleted by creator
