codelion/optillm

Can't install z3-solver, is it possible to support lean4?

Closed this issue · 20 comments

femto commented

Hello
1.Can't install z3-solver, is it possible to support lean4?
2.Is it possible to support alphageometry? For geometry problems, route to alphageometry, https://github.com/google-deepmind/alphageometry,
but I don't know how much effort to use it?

codelion commented

Can you tell me what error you faced with z3? It should be straightforward to install on mac/linux with pip install z3-solver.

It is possible to add lean4 or other tools. I am planning to add support for plugins so anyone could just add a script that will allow them to execute python code in between request and response of the proxy.

femto commented

can't install on localhost

 File "/private/var/folders/nh/vsykft2139j3bbhvv98q4f_00000gn/T/pip-build-env-x6sfb9jd/overlay/lib/python3.11/site-packages/setuptools/_distutils/cmd.py", line 303, in get_finalized_command
          cmd_obj.ensure_finalized()
        File "/private/var/folders/nh/vsykft2139j3bbhvv98q4f_00000gn/T/pip-build-env-x6sfb9jd/overlay/lib/python3.11/site-packages/setuptools/_distutils/cmd.py", line 111, in ensure_finalized
          self.finalize_options()
        File "<string>", line 267, in finalize_options
      KeyError: ('darwin', 'x86_64')

so I tried using docker
while can generate the z3 code, but failed to execute it
2024-09-30 05:51:57,135 - INFO - 127.0.0.1 - - [30/Sep/2024 05:51:57] "GET /health HTTP/1.1" 200 -
2024-09-30 13:52:06 2024-09-30 05:52:06,156 - ERROR - Execution timed out

femto commented

for running in docker, I'm solving this,
https://artofproblemsolving.com/wiki/index.php/2024_AIME_I_Problems/Problem_7,
code generated is

from z3 import *

# Define real variables for the real and imaginary parts of z
x = Real('x')
y = Real('y')

# Define the magnitude constraint |z| = 4, which translates to x^2 + y^2 = 16
magnitude_constraint = x**2 + y**2 == 16

# Define the real part of (96 + 144i) / (x + yi)
numerator_real = 96
numerator_imag = 144
denominator_real = x
denominator_imag = y

# Avoid division by zero by ensuring denominator is non-zero
denominator = denominator_real**2 + denominator_imag**2

# Real part of the division
real_part_division = If(denominator != 0,
                        (numerator_real * denominator_real + numerator_imag * denominator_imag) / denominator,
                        0)

# Define the objective function to maximize
objective = 75*x - 117*y + real_part_division

# Create an optimizer
opt = Optimize()

# Add the magnitude constraint
opt.add(magnitude_constraint)

# Maximize the objective function
opt.maximize(objective)

# Check for solution
if opt.check() == sat:
    model = opt.model()
    max_real_part = model.evaluate(objective)
    print(f"Maximum real part: {max_real_part}")
else:
    print("No solution found")

I suspect it's the code itself timeout?

codelion commented

yes, likely the formulation is not correct and times out. Which model did you use? And do you have the prompt with the question itself? I did try some of these problems with the techniques in this but the maximum I got was around 16.67% with z3 and re2 see #31 (comment)

codelion commented

can't install on localhost

 File "/private/var/folders/nh/vsykft2139j3bbhvv98q4f_00000gn/T/pip-build-env-x6sfb9jd/overlay/lib/python3.11/site-packages/setuptools/_distutils/cmd.py", line 303, in get_finalized_command
          cmd_obj.ensure_finalized()
        File "/private/var/folders/nh/vsykft2139j3bbhvv98q4f_00000gn/T/pip-build-env-x6sfb9jd/overlay/lib/python3.11/site-packages/setuptools/_distutils/cmd.py", line 111, in ensure_finalized
          self.finalize_options()
        File "<string>", line 267, in finalize_options
      KeyError: ('darwin', 'x86_64')

What is the version of setuptools on your machine? Looks like some issue with it.

femto commented 
Python 3.11.4
pip show setuptools:
Name: setuptools
Version: 75.1.0
femto commented

I'm using z3-gpt-4o(I found prefix approach a bit weird?)
the prompt be:

COT_PROBLEM_INSTRUCTION = """
Let's approach this problem by systematically breaking it down into distinct, logical steps. For each step, provide a clear explanation of the reasoning behind it, considering any underlying assumptions, potential biases, and alternative approaches. Explore how different assumptions or methodologies might lead to varying outcomes and critically assess the consequences of each decision. Additionally, consider the broader implications of these decisions within the context of the problem. Once all aspects have been thoroughly analyzed, synthesize the findings to reach a well-supported conclusion. Clearly express your final conclusion, ensuring that it is directly accessible and requires no further interpretation by presenting it explicitly within the tags <final_answer></final_answer>. Finally, include a verbalized confidence level for your conclusion (e.g., “Confidence: 60% / Medium”) to convey your level of certainty in the analysis and decision-making process.
"""
ASK_PROMPT = """context:
{input.short_context}
instruction:
{input.instruction}
query_type:
{input.query_type}
query:
{input.query}
"""
then:
(COT_PROBLEM_INSTRUCTION + ASK_PROMPT).format(input=self.input)
where input.query is
query="Find the largest possible real part of[(75+117i)z+\frac{96+144i}{z}]where $z$ is a complex number with $|z|=4$.",
input.instruction = "let's think step by step to solve this problem"

I don't think input.short_context
& input.query_type has value

codelion commented

I was able to get the right answer (540) with re2-gpt-4o-mini without the CoT prompt

Just with initial_query as "Find the largest possible real part of[(75+117i)z+\frac{96+144i}{z}]where z is a complex number with |z|=4" and empty system_prompt.

codelion commented

I'm using z3-gpt-4o(I found prefix approach a bit weird?)

this was to make it easy and not require any change in the openai python sdk that people are already using. I will add ability to pass it in extra_body param as noted in #39 .

femto commented

I was able to get the right answer (540) with re2-gpt-4o-mini without the CoT prompt

Just with initial_query as "Find the largest possible real part of[(75+117i)z+\frac{96+144i}{z}]where z is a complex number with |z|=4" and empty system_prompt.

Yes,I also able to make it work with bon with gpt-4o,
I think the problem is 1. it may not be stable
2.I want to implement general solution that divides math problem into subpart,
and each part invoke suitable tool to find answer,
this question is just an example.
I'll see what re2 is.

background is I'm doing this minion framework https://github.com/femto/minion,
so currently I also have code to divide problem. I'm trying to do aime and
see how much percentage I can make it pass.

  • 👍1
femto commented
image I'm doing this aime task, but I'm not sure openai's 15 questions refers to [I](https://artofproblemsolving.com/wiki/index.php/2024_AIME_I) or [II](https://artofproblemsolving.com/wiki/index.php/2024_AIME_II)
codelion commented

It has been hard to combine different approaches in my experience for a specific problem like cot + z3. Unless we implement it with a particular task in mind. For math like problems I believe it may well work. For AIME I used https://huggingface.co/datasets/AI-MO/aimo-validation-aime and picked the problems that had 2024. Not sure if that is the same as what openai used but this dataset has been used by others in the community for similar comparison e.g. here -https://github.com/hughbzhang/o1_inference_scaling_laws

femto commented

Yes, so I did dividing very complex. Dividing to each subtask,
and connect each subtask with input/output protocol.
Definitely we can communicate more as I move along these aime questions.

  • 👍1
femto commented

you can consider my many different minions like your different algorithms

  • 👍1
femto commented

1.Is it possible to add approach to prompt? Just adds to user prompt: "Use bon approach to solve this.",
Or <optillm_config>bon</optillm_config> in prompt and doing regex to extract this,
maybe it's bit easier than change model name or adding extra_body params if using existing framework.
Currently I use metagpt's ActionNode to call llm and do response format parsing, it allow me to
pass in user prompts.
2.Could you test Problem 8 to Problem 11 from https://artofproblemsolving.com/wiki/index.php/2024_AIME_I_Problems#Problem_8,
all failed miserably, I think geometry problems should route to AlphaGeometry,
but I'm not sure how much effort is that.
3.z3's code looks similar to sympy, It appeared they solve the same thing? Then how about switching to sympy? Sympy is much easier to install than z3.

codelion commented

1.Is it possible to add approach to prompt? Just adds to user prompt: "Use bon approach to solve this.",
Or <optillm_config>bon</optillm_config> in prompt and doing regex to extract this,
maybe it's bit easier than change model name or adding extra_body params if using existing framework.

I have added support for this in #40

codelion commented

3.z3's code looks similar to sympy, It appeared they solve the same thing? Then how about switching to sympy? Sympy is much easier to install than z3.

Will implement it as part of #41

codelion commented

I have added sympy also to the list of libraries that can be used along with z3 for the solver approach here - 083a058#diff-19d890e5ca0dd11f52a9fa2911675351962520d210c2fbc438c302f96051c31c

Haven't had the time to test it extensively yet.

codelion commented

Closing this bug report but feel free to open a discussion post for sharing further ideas and issues.