links 12/9/24

• https://gasstationmanager.github.io/ai/2024/11/04/a-proposal.html
  • a proposal that tentatively makes a lot of sense to me, for making LLM-generated code more robust and trustworthy.
  • the goal: give a formal specification (in e.g. Lean) of what you want the code to do; let the AI generate both the code and a proof that it meets the specification.
  • as a means to this end, a crowdsourced website called "Code With Proofs: The Arena", like LeetCode, where "players" can compete to submit code + proofs to solve coding challenges. This provides a source of training data for LLMs, producing both correct and incorrect (code, proof) pairs for each problem specification. A model can then be trained "given a problem specification, produce code that provably meets the specification".
    • In real life, the model would probably use the proof assistant's verifier directly at inference time, to ensure it only returned code + proofs that the automatic verifier confirmed were valid. It could use the error messages and intermediate feedback of the verifier to more efficiently search for code + proofs that were likely to be correct.
• https://en.wikipedia.org/wiki/Post-quantum_cryptography  I know nothing about this field but it sure looks like the cryptography people have come a long way towards being ready, if and when quantum computers start being able to break RSA
• https://en.m.wikipedia.org/wiki/Freik%C3%B6rperkultur  the German tradition of public nudity
• https://theconversation.com/japanese-scientists-were-pioneers-of-ai-yet-theyre-being-written-out-of-its-history-243762  this piece is gratuitously anti-Big Tech, but does present an interesting part of the history of neural networks.
  • In general I wonder why Americans tend to be blind to Japanese scientific/technological innovation these days! A lot of great stuff was invented in Japan!
• https://scratch.mit.edu/projects/editor/?tutorial=getStarted  a popular kids' programming language designed for making games and animations.
• https://bayesshammai.substack.com/p/conditional-on-getting-to-trade-your Ricki Heicklen on adverse selection
• https://www.complexsystemspodcast.com/episodes/teaching-trading-ricki-heicklen/ Patrick McKenzie and Ricki Heicklen on teaching trading. (It's mostly focused on the kind of quant finance you might see at a firm like Jane Street, not about managing your personal stock portfolio.)
• https://www.nature.com/articles/s41592-024-02523-znew nucleotide transformer model just dropped. Can be fine-tuned to do things like predict whether a sequence is a promoter, enhancer, or splice site.
• https://thecausalfallacy.com/p/disorder-at-the-starbucks I'm more civil-libertarian, but Charles Fain Lehman seems to be the thoughtful tough-on-crime advocate to keep an eye on.
  • I tend to think that the public will demand a certain level of safety and pleasantness in their environments no matter what, and it's the civil libertarian's job to find a way to deliver that without infringing anybody's rights and while avoiding undue cruelty/harm to those suspected of crime or viewed as "disorderly." If the public is unsatisfied, they will demand "tough on crime" policies sooner or later; we need to ensure that when they do, we end up with something reasonable and effective rather than overkill.
  • In that context, Lehman does seem concerned with using the least-harsh solutions where available. He recognizes that usually, if you want to deter a fairly mild public nuisance, you don't need to arrest or jail anybody, you just have cops and ordinary citizens tell troublemakers to knock it off, with escalating to tougher enforcement being an option that's usually not needed. We're on the same page that (valid) rules should be enforced, and that enforcement ultimately has to be backed by physical force, but ideally we wouldn't resort to force often. That's a reasonable basis for beginning to negotiate on policy.
  • OTOH his picture of reducing crime is entirely about calling for more enforcement, rather than addressing other points of failure like the lack of accountability (eg qualified immunity) for police generally. Lack of funding and tight restrictions on enforcement activities are not the only reason police might fail to enforce laws and catch criminals; sometimes they are gang-affiliated themselves, or are not bothering to do their jobs, in the fashion typical of any employee with infinite job security. When a police department is seriously dysfunctional, you're not going to get better public safety by giving it more funding and more freedom to operate.