3 ms·

I have no comments about the result itself, but the process and the AI policy which facilitated it is inspiring and easily transferable to any moderately compli

by baq 11mo ago

I have no comments about the result itself, but the process and the AI policy which facilitated it is inspiring and easily transferable to any moderately complicated software engineering problem. Much to learn regardless of the maths.

nsoonhui 11mo ago
But software engineering problems are more fuzzy and less amendable to mathematical analysis, so exactly how can those AI policies developed for math be applied to software engineering problems?
- boerseth 11mo ago
  Not sure which way the difference puts the pressure. Does the fuzziness require more prudent policies, or allow us to get away with less?
- contravariant 11mo ago
  Don't use them for the parts that are fuzzy. I mean it should be obvious that making executive decisions about what the code should do exactly should only be left to a RNG powered model if the choices made are unimportant.
robrenaud 11mo ago
I think you underestimate how powerful lean is, and close it is to the tedious part of formal math. A theorem prover needs consult no outside resource. A formal math LLM-like generator need only consult the theorem prover to get rid of hallucinations. This is why it's actually much easier than SWE to optimize/hill climb on. Low level, automated theorem providing is going to fall way quicker than most expected, like AlphaGo, precisely because an MCTS++ search over lean proofs is scalable/amendable to self play/relevant to a significant chunk of professional math. Legit, I almost wish the US and China would sign a Formal Mathematics Profileration Treaty, as a sign of good will between very powerful parties who have much to gain from each other. When your theorem prover is sufficiently better than most Fields medalists alive, you share your arch/algorithms/process with the world. So Mathematics stays in the shared realm of human culture, and it doesn't just happen to belong to DeepMind, OpenAI, or Deepseek.
- baq 11mo ago
  On the contrary I think we're low key on the verge of model checkers being widely deployed in the industry. I've been experimenting with Opus 4.5 + Alloy and the preliminary results I'm getting are crossing usability thresholds in a step-function pattern (not surprising IMHO), I just haven't seen anyone pick up on it publicly yet. The workflow I'm envisioning here is the plan document we're all making nowadays isn't being translated directly into code, but into a TLA+/Alloy/... model as executable docs and only then lowered into the code space while conformance is continuously monitored (which is where the toil makes it not worth it most of the time without LLMs). The AI literature search for similar problems and solutions is also obviously helpful during all phases of the sweng process.
  - robot-wrangler 11mo ago
    > The workflow I'm envisioning here is the plan document we're all making nowadays isn't being translated directly into code, but into a TLA+/Alloy/... model as executable docs and only then lowered into the code space while conformance is continuously monitored I'm sure we've agreed on this before, but I agree again ;) There are dozens of us at least, dozens! There's also a recent uptick in posts with related ideas, for example this hit the front-page briefly ( https://news.ycombinator.com/item?id=46251667 https://news.ycombinator.com/item?id=46251667 ). I was tempted to start with alloy/tla for my own experiments along these lines due to their popularity, but since the available training data is so minimal for everything in the space.. I went with something more obscure (MCMAS) just for access to "agents" as primitives in the model-checker.
    - baq 11mo ago
      > available training data is so minimal for everything in the space Haven't tried anything other than Alloy yet, but I've got a feeling Anthropic has employed some dark arts to synthesize either Alloy models or something closely related and trained Opus on the result - e.g. GPT 5.1 commits basic syntax errors, while Opus writes models like it's just another day at the office.
- gaigalas 11mo ago

by baq 11mo ago

nsoonhui 11mo ago

But software engineering problems are more fuzzy and less amendable to mathematical analysis, so exactly how can those AI policies developed for math be applied to software engineering problems?

boerseth 11mo ago
Not sure which way the difference puts the pressure. Does the fuzziness require more prudent policies, or allow us to get away with less?
contravariant 11mo ago
Don't use them for the parts that are fuzzy. I mean it should be obvious that making executive decisions about what the code should do exactly should only be left to a RNG powered model if the choices made are unimportant.

robrenaud 11mo ago

I think you underestimate how powerful lean is, and close it is to the tedious part of formal math. A theorem prover needs consult no outside resource. A formal math LLM-like generator need only consult the theorem prover to get rid of hallucinations. This is why it's actually much easier than SWE to optimize/hill climb on. Low level, automated theorem providing is going to fall way quicker than most expected, like AlphaGo, precisely because an MCTS++ search over lean proofs is scalable/amendable to self play/relevant to a significant chunk of professional math. Legit, I almost wish the US and China would sign a Formal Mathematics Profileration Treaty, as a sign of good will between very powerful parties who have much to gain from each other. When your theorem prover is sufficiently better than most Fields medalists alive, you share your arch/algorithms/process with the world. So Mathematics stays in the shared realm of human culture, and it doesn't just happen to belong to DeepMind, OpenAI, or Deepseek.

baq 11mo ago
On the contrary I think we're low key on the verge of model checkers being widely deployed in the industry. I've been experimenting with Opus 4.5 + Alloy and the preliminary results I'm getting are crossing usability thresholds in a step-function pattern (not surprising IMHO), I just haven't seen anyone pick up on it publicly yet. The workflow I'm envisioning here is the plan document we're all making nowadays isn't being translated directly into code, but into a TLA+/Alloy/... model as executable docs and only then lowered into the code space while conformance is continuously monitored (which is where the toil makes it not worth it most of the time without LLMs). The AI literature search for similar problems and solutions is also obviously helpful during all phases of the sweng process.
- robot-wrangler 11mo ago
  > The workflow I'm envisioning here is the plan document we're all making nowadays isn't being translated directly into code, but into a TLA+/Alloy/... model as executable docs and only then lowered into the code space while conformance is continuously monitored I'm sure we've agreed on this before, but I agree again ;) There are dozens of us at least, dozens! There's also a recent uptick in posts with related ideas, for example this hit the front-page briefly ( https://news.ycombinator.com/item?id=46251667 https://news.ycombinator.com/item?id=46251667 ). I was tempted to start with alloy/tla for my own experiments along these lines due to their popularity, but since the available training data is so minimal for everything in the space.. I went with something more obscure (MCMAS) just for access to "agents" as primitives in the model-checker.
  - baq 11mo ago
    > available training data is so minimal for everything in the space Haven't tried anything other than Alloy yet, but I've got a feeling Anthropic has employed some dark arts to synthesize either Alloy models or something closely related and trained Opus on the result - e.g. GPT 5.1 commits basic syntax errors, while Opus writes models like it's just another day at the office.
gaigalas 11mo ago