4 ms·

I had a surprising interaction with Gemini 2.5 Pro that this project reminds me of. I was asking the LLM for help using an online CAS system to solve a system o

by chrchr 1y ago

I had a surprising interaction with Gemini 2.5 Pro that this project reminds me of. I was asking the LLM for help using an online CAS system to solve a system of equations, and the CAS system wasn't working as I expected. After a couple back and forths with Gemini about the CAS system, Gemini just gave me the solution. I was surprised because it's the kind of thing I don't expect LLMs to be good at. It said it used Python's sympy symbolic computation package to arrive at the solution. So, yes, the marriage of fuzzy LLMs with more rigorous tools can have powerful effects.

TrainedMonkey 1y ago
Just like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.
- jonplackett 1y ago
  Maybe the number crunching program the text generation program creates will, with enough effort become good at generating text, an will in turn make another number crunching computer and then…
  - psadri 1y ago
    Watch the movie “The Thirteenth Floor”
    - Barbing 1y ago
      This is somewhat unusual: 28% on the Tomatometer, but 7 out of 10 on IMDb. Beyond its relevancy to the parent comment, would you consider it a good movie yourself? (for a random/average HN commenter to watch)
      - c-hendricks 1y ago
        It didn't do well critically, but audience scores on many platforms are 60-70%. It came hot on the heels of The Matrix, has similar themes, but nowhere near as ... everything compared to Matrix. I'd bet the only reason it did so poorly critically is due to the timing of the release. It's a fine movie though.
        Barbing 1y ago
        Thank you :)
      - bonoboTP 1y ago
        If you like Matrix, Memento, Truman Show, Black Mirror (San Junipero, Bandersnatch), Inception, Interstellar, 12 Monkeys etc. you may also like it. These are not necessarily thematically aligned but based on vibes they cluster near it for me. I definitely enjoyed it many years ago as a younger person.
        Barbing 1y ago
        Nice, thanks :)
      - self 1y ago
        Three movies with overlapping themes came out in mid-1999: The Matrix, The Thirteenth Floor, and eXistenZ (probably in that order of box office revenue).
        Barbing 1y ago
        Ah interesting thanks!
- patcon 1y ago
  I love this kind of thought. Thanks.
- idiotsecant 1y ago
  Parent post is talking about symbolic manipulation, not rote number crunching, which is exactly what we're supposed to be good at and machines are supposed to be bad at.
- 29athrowaway 1y ago
  We do plenty of number crunching all the time, just not consciously. Like the inverse kinematics required for your arm and fingers to move.
  - pstoll 1y ago
    I’d argue we aren’t solving those inverse kinematics / kinetics via “number crunching” - but rather that our neuromuscular systems are analog. Which I don’t usually call that “number crunching” in the sense current computers … compute.
    - tomcloyd 1y ago
      As a psychologist, I completely agree. It absolutely is NOT number crunching. Analog computation is primary and dominant in animals. It has to be, for so many reasons. I continue to be amazed at how much IT people do NOT grasp human and animal IT. And that, I would argue, is why so many IT folks keep talking about our supposedly approaching human intelligence in technology. If they really understood human intelligence the absurdity of that statement would keep them quiet. An elegant, artful puppet is still a puppet, and without the personal history context and consciousness we possess, not to mention a vast complex of analogue computation functionality we rely upon, that puppet will only ever be a clever number-cruncher. We are so much more.
      - galaxyLogic 1y ago
        Are our brains "analog"? Or are they in fact "digital"? I would think actually more digital than analog. A synapse triggers or it does not trigger. It either triggers or not, not something in between. In this sense it is 0 or 1. Similarly transistor-based logic is based on such thresholds, when current or voltage reaches a certain level then a state-transition happens.
        fwip 1y ago
        Well, no, synapses aren't binary in response.
- emporas 1y ago
  Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.
  - eru 1y ago
    Your checks don't have to be deterministic either. Eg randomised quicksort works really well.
    - emporas 1y ago
      Couldn't disagree more. Sorting a finite number of elements in a sequence, is a very narrow application of AI, akin to playing chess. Usually very simple approaches like RL work totally fine for problems like these, but auto-regression/diffusion models have to take steps that are not well defined at all, and the next step towards solving the problem is not obvious. As an example, imagine a robot trying to grab a tomato from a table. It's arm extends across 1 meter maximum, and the tomato is placed 0.98 meters away. Is it able to grab the tomato from the point it stands, or it needs to move closer, and only then try to grab the tomato? That computation should better be calculated deterministically. Deterministic computation is faster, cheaper and more secure. It has to prove that: $tomato_distance + $tomato_size < $arm_length. If this constraint is not satisfied, then: move_closer(); Calculate again:$tomato_distance + $tomato_size < $arm_length. From the paper: > Our system employs a custom interpreter that parses "LLM-Thoughts" (represented as DSL code snippets) to generate First Order Logic programs, which are then verified by a Z3 theorem prover.
      - eru 1y ago
        > Sorting a finite number of elements in a sequence, is a very narrow application of AI, [...] Sorry, I did not suggest you should use AI to sort numbers. I was solely replying to this: > Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. You don't necessarily need your checks to be deterministic. In fact, it's often better for them to be not deterministic. See also https://fsharpforfunandprofit.com/series/property-based-testing/ https://fsharpforfunandprofit.com/series/property-based-test... I don't understand your claim about 'Deterministic computation is faster, cheaper and more secure.' That's not true at all. In fact, for many problems the fastest and simplest known solutions are non-deterministic. And in eg cryptography you _need_ non-determinism to get any security at all.
anotherpaulg 1y ago
I really like LLM+sympy for math. I have the LLM write me a sympy program, so I can trust that the symbolic manipulation is done correctly. The code is also a useful artifact that can be iteratively edited and improved by both the human and LLM, with git history, etc. Running and passing tests/assertions helps to build and maintain confidence that the math remains correct. I use helper functions to easily render from the sympy code to latex, etc. A lot of the math behind this quantum eraser experiment was done this way. https://github.com/paul-gauthier/entangled-pair-quantum-eraser/ https://github.com/paul-gauthier/entangled-pair-quantum-eras...
DrewADesign 1y ago
I get having it walk you through figuring out a problem with a tool: seems like a good idea and it clearly worked even better than expected. But deliberately coaxing an LLM into doing math correctly instead of a CAS because you’ve got one handy seems like moving apartments with dozens of bus trips rather than taking the bus to a truck rental place, just because you’ve already got a bus pass.
- afiori 1y ago
  I feel like a better analogy is trying to rent a truck to move to a new apartment and after repeated failures of trucks not working they just hire a moving company for you to get you to leave
  - DrewADesign 1y ago
    All of those tools are purpose-built for moving people. LLMs are not at all built for doing math.
jansan 1y ago
How die that work? Did Gemini call sympy on your maschine, or is access to sympy built-in and available through normal chat?
- 7734128 1y ago
  https://cloud.google.com/vertex-ai/generative-ai/docs/multimodal/code-execution https://cloud.google.com/vertex-ai/generative-ai/docs/multim...
fennecfoxy 1y ago
Yeah it feels like these early LLMs are pretty decent at the coming up with a plan and executing a plan part. Probably the main deficiencies are confusion as the context grows (therefore confusion as task complexity grows).
selinkocalar 1y ago
The combination of LLMs and formal verification tools is pretty interesting. We've been thinking about this for compliance automation - there are a lot of regulatory requirements that could theoretically be expressed as formal constraints. Curious about the performance though. Z3 can be really slow on complex problems, and if you're chaining that with LLM calls, the latency could get rough for interactive use cases.

by chrchr 1y ago

TrainedMonkey 1y ago

Just like humans... we are not so good at hard number crunching, but we can invent computers that are amazing at it. And with a lot of effort we can make a program that uses a whole lot of number crunching to be ok at predicting text but kind of bad at crunching hard numbers. And then that program can predict how to create and use programs which are good at number crunching.

jonplackett 1y ago
Maybe the number crunching program the text generation program creates will, with enough effort become good at generating text, an will in turn make another number crunching computer and then…
- psadri 1y ago
  Watch the movie “The Thirteenth Floor”
  - Barbing 1y ago
    This is somewhat unusual: 28% on the Tomatometer, but 7 out of 10 on IMDb. Beyond its relevancy to the parent comment, would you consider it a good movie yourself? (for a random/average HN commenter to watch)
    - c-hendricks 1y ago
      It didn't do well critically, but audience scores on many platforms are 60-70%. It came hot on the heels of The Matrix, has similar themes, but nowhere near as ... everything compared to Matrix. I'd bet the only reason it did so poorly critically is due to the timing of the release. It's a fine movie though.
      - Barbing 1y ago
        Thank you :)
    - bonoboTP 1y ago
      If you like Matrix, Memento, Truman Show, Black Mirror (San Junipero, Bandersnatch), Inception, Interstellar, 12 Monkeys etc. you may also like it. These are not necessarily thematically aligned but based on vibes they cluster near it for me. I definitely enjoyed it many years ago as a younger person.
      - Barbing 1y ago
        Nice, thanks :)
    - self 1y ago
      Three movies with overlapping themes came out in mid-1999: The Matrix, The Thirteenth Floor, and eXistenZ (probably in that order of box office revenue).
      - Barbing 1y ago
        Ah interesting thanks!
patcon 1y ago
I love this kind of thought. Thanks.
idiotsecant 1y ago
Parent post is talking about symbolic manipulation, not rote number crunching, which is exactly what we're supposed to be good at and machines are supposed to be bad at.
29athrowaway 1y ago
We do plenty of number crunching all the time, just not consciously. Like the inverse kinematics required for your arm and fingers to move.
- pstoll 1y ago
  I’d argue we aren’t solving those inverse kinematics / kinetics via “number crunching” - but rather that our neuromuscular systems are analog. Which I don’t usually call that “number crunching” in the sense current computers … compute.
  - tomcloyd 1y ago
    As a psychologist, I completely agree. It absolutely is NOT number crunching. Analog computation is primary and dominant in animals. It has to be, for so many reasons. I continue to be amazed at how much IT people do NOT grasp human and animal IT. And that, I would argue, is why so many IT folks keep talking about our supposedly approaching human intelligence in technology. If they really understood human intelligence the absurdity of that statement would keep them quiet. An elegant, artful puppet is still a puppet, and without the personal history context and consciousness we possess, not to mention a vast complex of analogue computation functionality we rely upon, that puppet will only ever be a clever number-cruncher. We are so much more.
    - galaxyLogic 1y ago
      Are our brains "analog"? Or are they in fact "digital"? I would think actually more digital than analog. A synapse triggers or it does not trigger. It either triggers or not, not something in between. In this sense it is 0 or 1. Similarly transistor-based logic is based on such thresholds, when current or voltage reaches a certain level then a state-transition happens.
      - fwip 1y ago
        Well, no, synapses aren't binary in response.
emporas 1y ago
Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. That's when A.I. starts advancing itself and needs humans in the loop no more.
- eru 1y ago
  Your checks don't have to be deterministic either. Eg randomised quicksort works really well.
  - emporas 1y ago
    Couldn't disagree more. Sorting a finite number of elements in a sequence, is a very narrow application of AI, akin to playing chess. Usually very simple approaches like RL work totally fine for problems like these, but auto-regression/diffusion models have to take steps that are not well defined at all, and the next step towards solving the problem is not obvious. As an example, imagine a robot trying to grab a tomato from a table. It's arm extends across 1 meter maximum, and the tomato is placed 0.98 meters away. Is it able to grab the tomato from the point it stands, or it needs to move closer, and only then try to grab the tomato? That computation should better be calculated deterministically. Deterministic computation is faster, cheaper and more secure. It has to prove that: $tomato_distance + $tomato_size < $arm_length. If this constraint is not satisfied, then: move_closer(); Calculate again:$tomato_distance + $tomato_size < $arm_length. From the paper: > Our system employs a custom interpreter that parses "LLM-Thoughts" (represented as DSL code snippets) to generate First Order Logic programs, which are then verified by a Z3 theorem prover.
    - eru 1y ago
      > Sorting a finite number of elements in a sequence, is a very narrow application of AI, [...] Sorry, I did not suggest you should use AI to sort numbers. I was solely replying to this: > Small steps of nondeterministic computation, checked thoroughly with deterministic computation every so often, and the sky is the limit. You don't necessarily need your checks to be deterministic. In fact, it's often better for them to be not deterministic. See also https://fsharpforfunandprofit.com/series/property-based-testing/ https://fsharpforfunandprofit.com/series/property-based-test... I don't understand your claim about 'Deterministic computation is faster, cheaper and more secure.' That's not true at all. In fact, for many problems the fastest and simplest known solutions are non-deterministic. And in eg cryptography you _need_ non-determinism to get any security at all.

anotherpaulg 1y ago

I really like LLM+sympy for math. I have the LLM write me a sympy program, so I can trust that the symbolic manipulation is done correctly. The code is also a useful artifact that can be iteratively edited and improved by both the human and LLM, with git history, etc. Running and passing tests/assertions helps to build and maintain confidence that the math remains correct. I use helper functions to easily render from the sympy code to latex, etc. A lot of the math behind this quantum eraser experiment was done this way. https://github.com/paul-gauthier/entangled-pair-quantum-eraser/ https://github.com/paul-gauthier/entangled-pair-quantum-eras...

DrewADesign 1y ago

I get having it walk you through figuring out a problem with a tool: seems like a good idea and it clearly worked even better than expected. But deliberately coaxing an LLM into doing math correctly instead of a CAS because you’ve got one handy seems like moving apartments with dozens of bus trips rather than taking the bus to a truck rental place, just because you’ve already got a bus pass.

afiori 1y ago
I feel like a better analogy is trying to rent a truck to move to a new apartment and after repeated failures of trucks not working they just hire a moving company for you to get you to leave
- DrewADesign 1y ago
  All of those tools are purpose-built for moving people. LLMs are not at all built for doing math.

jansan 1y ago

How die that work? Did Gemini call sympy on your maschine, or is access to sympy built-in and available through normal chat?

7734128 1y ago
https://cloud.google.com/vertex-ai/generative-ai/docs/multimodal/code-execution https://cloud.google.com/vertex-ai/generative-ai/docs/multim...

fennecfoxy 1y ago

Yeah it feels like these early LLMs are pretty decent at the coming up with a plan and executing a plan part. Probably the main deficiencies are confusion as the context grows (therefore confusion as task complexity grows).

selinkocalar 1y ago

The combination of LLMs and formal verification tools is pretty interesting. We've been thinking about this for compliance automation - there are a lot of regulatory requirements that could theoretically be expressed as formal constraints. Curious about the performance though. Z3 can be really slow on complex problems, and if you're chaining that with LLM calls, the latency could get rough for interactive use cases.