{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"id": "10ec473f",
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"import os\n",
"from openai import OpenAI\n",
"\n",
"from dotenv import load_dotenv\n",
"\n",
"load_dotenv()"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "d2637726",
"metadata": {},
"outputs": [],
"source": [
"API_BASE_URL = os.getenv(\"API_BASE_URL\", \"https://router.huggingface.co/v1\")\n",
"MODEL_NAME = os.getenv(\"MODEL_NAME\", \"Qwen/Qwen2.5-72B-Instruct\")\n",
"# API_KEY = os.getenv(\"HF_TOKEN\")\n",
"API_KEY = os.getenv(\"GEMINI_API_KEY\")\n",
"TEMPERATURE = float(os.getenv(\"TEMPERATURE\", \"0.2\"))"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "0150dbb3",
"metadata": {},
"outputs": [],
"source": [
"client = OpenAI(base_url=API_BASE_URL, api_key=API_KEY)\n"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "d9d8e747",
"metadata": {},
"outputs": [],
"source": [
"response = client.chat.completions.create(\n",
" model=MODEL_NAME,\n",
" messages=[\n",
" # {\"role\": \"system\", \"content\": _get_system_prompt(task_id)},\n",
" {\"role\": \"user\", \"content\": \"Hi there!\"},\n",
" ],\n",
" temperature=TEMPERATURE,\n",
" response_format={\"type\": \"json_object\"}\n",
")"
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "bda4a780",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"ChatCompletion(id='cQrZaZbxMIjWg8UPh8LAkAg', choices=[Choice(finish_reason='stop', index=0, logprobs=None, message=ChatCompletionMessage(content='* User input: \"Hi there!\"\\n * Constraint 1: Only generate a valid, parseable JSON.\\n * Constraint 2: Besides scalars, boolean, and null, other values must be double-quoted as valid strings.\\n * Constraint 3: No comments inside the JSON block.\\n * Constraint 4: If multiple JSON are requested, return a single parseable JSON array.\\n * Constraint 5: Do not include any extra text outside of the JSON string.\\n\\n * The user said \"Hi there!\". This is a greeting.\\n * Since the system instruction requires *only* JSON, I cannot respond with a conversational text. I must respond with a JSON object representing a response.\\n\\n * Option A: `{\"message\": \"Hello! How can I help you today?\"}`\\n * Option B: `[\"Hello! How can I help you today?\"]`\\n\\n * The prompt asks for \"a valid, parseable JSON\".\\n * A simple object is standard.\\n\\n * `{\"response\": \"Hello! How can I help you today?\"}`\\n\\n * Valid JSON? Yes.\\n * Double-quoted strings? Yes.\\n * No comments? Yes.\\n * No extra text? Yes.\\n\\n `{\"message\": \"Hello! How can I help you today?\"}`{\\n \"message\": \"Hello! How can I help you today?\"\\n}', refusal=None, role='assistant', annotations=None, audio=None, function_call=None, tool_calls=None, extra_content={'google': {'thought': True}}))], created=1775831666, model='gemma-4-26b-a4b-it', object='chat.completion', service_tier=None, system_fingerprint=None, usage=CompletionUsage(completion_tokens=18, prompt_tokens=4, total_tokens=324, completion_tokens_details=None, prompt_tokens_details=None))\n"
]
}
],
"source": [
"print(response)"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "2e29f995",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"\n",
"Step: 6 / 25\n",
"Progress: 0.33\n",
"Verified: evalBinOp\n",
"Remaining: evalExpr, divisionProof\n",
"Failing: {}\n",
"\n",
"\n",
"\n",
"\n",
"Name: evalExpr\n",
"Description: Recursively evaluate an expression tree. Propagate None on division by zero.\n",
"Depends on: ['evalBinOp']\n",
"Proof required: False\n",
"\n",
"\n",
"\n",
"int eval_expr(const Expr *expr, long long *out) {\n",
" if (expr->tag == EXPR_LIT) {\n",
" *out = expr->lit;\n",
" return 1;\n",
" }\n",
" long long left_val, right_val;\n",
" if (!eval_expr(expr->binop.left, &left_val)) return 0;\n",
" if (!eval_expr(expr->binop.right, &right_val)) return 0;\n",
" return eval_bin_op(expr->binop.op, left_val, right_val, out);\n",
"}\n",
"\n",
"\n",
"\n",
"def evalExpr : ExprSpec.Expr → Option Int\n",
" | .Lit n => some n\n",
" | .BinOp op l r =>\n",
" match evalExpr l, evalExpr r with\n",
" | some a, some b => evalBinOp op a b\n",
" | _, _ => none\n",
"\n",
"\n",
"\n",
"The following dependency code is automatically prepended to your submission. Do NOT redefine these symbols.\n",
"\n",
"\n",
"evalBinOp (verified):\n",
"```rust\n",
"#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Op { Add, Sub, Mul, Div } pub fn eval_bin_op(op: Op, a: i64, b: i64) -> Option { match op { Op::Add => Some(a + b), Op::Sub => Some(a - b), Op::Mul => Some(a * b), Op::Div => if b == 0 { None } else { Some(a / b) } } }\n",
"```\n",
"\n",
"\n",
"\n",
"\n",
"Step 5: type=inspect fn=evalExpr reward=0.050\n",
"\n",
"\n",
"Decide the next action. Return ONLY valid JSON.\n"
]
}
],
"source": [
"print(\"\"\"\\nStep: 6 / 25\\nProgress: 0.33\\nVerified: evalBinOp\\nRemaining: evalExpr, divisionProof\\nFailing: {}\\n\\n\\n\\n\\nName: evalExpr\\nDescription: Recursively evaluate an expression tree. Propagate None on division by zero.\\nDepends on: ['evalBinOp']\\nProof required: False\\n\\n\\n\\nint eval_expr(const Expr *expr, long long *out) {\\n if (expr->tag == EXPR_LIT) {\\n *out = expr->lit;\\n return 1;\\n }\\n long long left_val, right_val;\\n if (!eval_expr(expr->binop.left, &left_val)) return 0;\\n if (!eval_expr(expr->binop.right, &right_val)) return 0;\\n return eval_bin_op(expr->binop.op, left_val, right_val, out);\\n}\\n\\n\\n\\ndef evalExpr : ExprSpec.Expr → Option Int\\n | .Lit n => some n\\n | .BinOp op l r =>\\n match evalExpr l, evalExpr r with\\n | some a, some b => evalBinOp op a b\\n | _, _ => none\\n\\n\\n\\nThe following dependency code is automatically prepended to your submission. Do NOT redefine these symbols.\\n\\n\\nevalBinOp (verified):\\n```rust\\n#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Op { Add, Sub, Mul, Div } pub fn eval_bin_op(op: Op, a: i64, b: i64) -> Option { match op { Op::Add => Some(a + b), Op::Sub => Some(a - b), Op::Mul => Some(a * b), Op::Div => if b == 0 { None } else { Some(a / b) } } }\\n```\\n\\n\\n\\n\\nStep 5: type=inspect fn=evalExpr reward=0.050\\n\\n\\nDecide the next action. Return ONLY valid JSON.\"\"\")"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "7ca7bcd1",
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "openenv-lean-migrate (3.13.12)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.13.12"
}
},
"nbformat": 4,
"nbformat_minor": 5
}