Get response from the LLM for a proof problem
(problem: str, model: str, client: OpenAI, extra_body: dict = None, timeout: int = 600)
| 217 | |
| 218 | |
| 219 | def get_llm_response(problem: str, model: str, client: OpenAI, extra_body: dict = None, timeout: int = 600) -> Dict: |
| 220 | """ |
| 221 | Get response from the LLM for a proof problem |
| 222 | """ |
| 223 | try: |
| 224 | kwargs = {} |
| 225 | if extra_body: |
| 226 | kwargs["extra_body"] = extra_body |
| 227 | |
| 228 | response = client.with_options(timeout=timeout).chat.completions.create( |
| 229 | model=model, |
| 230 | messages=[ |
| 231 | {"role": "system", "content": SYSTEM_PROMPT}, |
| 232 | {"role": "user", "content": problem} |
| 233 | ], |
| 234 | max_tokens=64000, # Extended for complex proofs |
| 235 | temperature=0.1, |
| 236 | **kwargs |
| 237 | ) |
| 238 | |
| 239 | solution_text = response.choices[0].message.content.strip() |
| 240 | reasoning_tokens = getattr(response.usage, 'reasoning_tokens', 0) |
| 241 | total_tokens = response.usage.total_tokens if hasattr(response.usage, 'total_tokens') else 0 |
| 242 | |
| 243 | return { |
| 244 | "solution": solution_text, |
| 245 | "reasoning_tokens": reasoning_tokens, |
| 246 | "total_tokens": total_tokens, |
| 247 | "success": True |
| 248 | } |
| 249 | |
| 250 | except Exception as e: |
| 251 | logger.error(f"Error getting LLM response: {e}") |
| 252 | return { |
| 253 | "solution": f"Error: {str(e)}", |
| 254 | "reasoning_tokens": 0, |
| 255 | "total_tokens": 0, |
| 256 | "success": False |
| 257 | } |
| 258 | |
| 259 | |
| 260 | def save_result(filename: str, result: Dict): |