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.
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!
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.
Scratch is awesome for kids. My kids love it. My older daughter has afternoon lessons at school, and I help her debug her projects if there is a problem. I am not sure how I would teach her, if I had to start from zero.
I found a few videos on how to make games in Scratch, and I learned a lot about Scratch from them, but sometimes the author uses in the algorithm a mathematical expression that seems a bit too complicated for a small child. For example, how to make a moving object stop right before the wall. Like, if it moves 10 pixels each turn, and the wall is 5 pixels ahead, you want it to go 5 pixels at the last step; neither 10 nor 0. The author’s solution is to go 10 pixels forward, and then “repeat 10 times: if there is a collision with the wall, go 1 pixel back”. (Collisions of pictures are a primitive operation in Scratch.) That sounds trivial, but because the speed could be 10 pixels per turn or −10 pixels for turn, and it’s not even guaranteed to be an integer, the algorithm becomes “repeat ceil(abs(V)) times: if there is a collision with the wall, go V/ceil(abs(V)) pixels back”, and which point my daughter just says “I don’t get it”. (This is not a problem with Scratch per se; you could limit the speed to integer, and maybe avoid the absolute value by using an if-statement and doing the positive and negative values separately; and maybe ceil(abs(V)) could be a local variable. I am just saying that the videos are generally great… but you get one or two moments of this per video.)
In a bookstore I found a translation of Carol Vorderman’s Computer Coding For Kids, which seems good (so it’s going to be a Christmas present); the first 1⁄3 of the book is Scratch, the remaining 2⁄3 are Python.
.
I like the definition of disorder as domination of public space for private purposes. As I see it, the problem with informal systems of preventing disorder is that some people are resistant to shame; specifically:
assholes
criminals
homeless
mentally ill
drug addicts
teenagers, when encouraged by other teenagers (unless you happen to know their parents)
Once your neighborhood becomes a favorite place of these, you either need a strong community (the kind that can summon a group of adult men with baseball bats, who would ask the disorderly people to kindly leave and never set their foot in this neighborhood again), or you have to call the police. Or you give up your public space.
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.
Scratch is awesome for kids. My kids love it. My older daughter has afternoon lessons at school, and I help her debug her projects if there is a problem. I am not sure how I would teach her, if I had to start from zero.
I found a few videos on how to make games in Scratch, and I learned a lot about Scratch from them, but sometimes the author uses in the algorithm a mathematical expression that seems a bit too complicated for a small child. For example, how to make a moving object stop right before the wall. Like, if it moves 10 pixels each turn, and the wall is 5 pixels ahead, you want it to go 5 pixels at the last step; neither 10 nor 0. The author’s solution is to go 10 pixels forward, and then “repeat 10 times: if there is a collision with the wall, go 1 pixel back”. (Collisions of pictures are a primitive operation in Scratch.) That sounds trivial, but because the speed could be 10 pixels per turn or −10 pixels for turn, and it’s not even guaranteed to be an integer, the algorithm becomes “repeat ceil(abs(V)) times: if there is a collision with the wall, go V/ceil(abs(V)) pixels back”, and which point my daughter just says “I don’t get it”. (This is not a problem with Scratch per se; you could limit the speed to integer, and maybe avoid the absolute value by using an if-statement and doing the positive and negative values separately; and maybe ceil(abs(V)) could be a local variable. I am just saying that the videos are generally great… but you get one or two moments of this per video.)
In a bookstore I found a translation of Carol Vorderman’s Computer Coding For Kids, which seems good (so it’s going to be a Christmas present); the first 1⁄3 of the book is Scratch, the remaining 2⁄3 are Python.
.
I like the definition of disorder as domination of public space for private purposes. As I see it, the problem with informal systems of preventing disorder is that some people are resistant to shame; specifically:
assholes
criminals
homeless
mentally ill
drug addicts
teenagers, when encouraged by other teenagers (unless you happen to know their parents)
Once your neighborhood becomes a favorite place of these, you either need a strong community (the kind that can summon a group of adult men with baseball bats, who would ask the disorderly people to kindly leave and never set their foot in this neighborhood again), or you have to call the police. Or you give up your public space.