[HN Gopher] Designing Predictable LLM-Verifier Systems for Forma...
       ___________________________________________________________________
        
       Designing Predictable LLM-Verifier Systems for Formal Method
       Guarantee
        
       Author : PaulHoule
       Score  : 50 points
       Date   : 2025-12-28 15:02 UTC (7 hours ago)
        
 (HTM) web link (arxiv.org)
 (TXT) w3m dump (arxiv.org)
        
       | brantmv wrote:
       | Maybe I'm wrong, but it looks like the authors did not actually
       | have any LLMs write or verify any code for their experiments.
       | Instead, their experiments consist of simulating the _simplified
       | Markov chain model itself_. They simulated their simple Markov
       | chain and checked if the theorem 's predictions matched empirical
       | statistics. This amounts to a test not of their model, but of
       | basic Markov chain theory.
       | 
       | Did I misread or miss something?
        
       | mapontosevenths wrote:
       | This line made me pause:
       | 
       | "We prove that for any non-zero stage success probability, the
       | system reaches the verified state _almost_ surely "
       | 
       | What's the point if its still stochastic?
        
         | IanCal wrote:
         | Hash collisions are possible but can be provably so rare that
         | they're not a relevant concern.
        
         | jaggederest wrote:
         | "almost surely" means "happens with a probability 1", which in
         | infinite set contexts doesn't mean that there aren't other
         | outcomes, but that they have probability 0.
         | 
         | So like, imagine that you had some finite list of integers, and
         | you were picking a random number from 0 to infinity - because
         | the domain is infinite, any finite set has 0 probability, but
         | that doesn't mean it doesn't exist.
         | 
         | https://en.wikipedia.org/wiki/Almost_surely
        
           | mapontosevenths wrote:
           | Thank you. That makes this a pretty big deal doesn't it?
           | 
           | The ability to deterministcly identify that code eventually
           | reaches a halting state, implies that we can use these
           | stochastic tools to generate deterministic outcomes reliably
           | in the future doesn't it?
        
             | jaggederest wrote:
             | Well, reliably but still with a chance of failure - in the
             | same way that you can have a program which is provably
             | correct but can still run into real world issues like being
             | killed, but yes I would say that "almost surely" is a
             | pretty large jump from "more than likely" (50%+1) where I'd
             | say LLM output generally lives these days.
        
               | MiniMax42 wrote:
               | > a chance of failure
               | 
               | Well, technically, no chance of failure. The chance of
               | failure is absolute zero. Not close to zero, absolute
               | zero. There will be no failure if the assumptions of the
               | model are correct.
               | 
               | The real catch here is in the assumptions.
               | 
               | How long do you have before you need to have a solution?
               | An hour, a year, a century? Too bad, almost sure
               | convergence only provides a guarantee if you wait an
               | infinite amount of time.
               | 
               | And then there's the question of the probability space
               | you assume. (The sigma algebra.) Which things do you
               | assume to have probability zero from the start and is
               | that realistic?
        
       ___________________________________________________________________
       (page generated 2025-12-28 23:00 UTC)