|
|
#!/usr/bin/env python3
|
|
|
"""
|
|
|
快速DeepSeek v3.1测试脚本
|
|
|
独立运行,不依赖复杂导入
|
|
|
"""
|
|
|
|
|
|
import os
|
|
|
import requests
|
|
|
import json
|
|
|
import time
|
|
|
|
|
|
|
|
|
def quick_deepseek_test():
|
|
|
"""快速测试DeepSeek v3.1 API"""
|
|
|
print("🚀 DeepSeek v3.1 快速测试")
|
|
|
print("=" * 40)
|
|
|
|
|
|
# 检查API密钥
|
|
|
api_key = os.getenv('SILICONFLOW_API_KEY')
|
|
|
if not api_key:
|
|
|
print("❌ 错误: 未设置 SILICONFLOW_API_KEY 环境变量")
|
|
|
return
|
|
|
|
|
|
print(f"📡 连接模型: deepseek-ai/DeepSeek-V3.1")
|
|
|
print(f"🔑 API密钥: {api_key[:20]}...")
|
|
|
|
|
|
try:
|
|
|
# 测试连接
|
|
|
headers = {
|
|
|
"Authorization": f"Bearer {api_key}",
|
|
|
"Content-Type": "application/json"
|
|
|
}
|
|
|
|
|
|
data = {
|
|
|
"model": "deepseek-ai/DeepSeek-V3.1",
|
|
|
"messages": [
|
|
|
{
|
|
|
"role": "system",
|
|
|
"content": "你是CBMC形式化验证专家,为C代码生成CBMC规约。只输出CBMC代码。"
|
|
|
},
|
|
|
{
|
|
|
"role": "user",
|
|
|
"content": """为以下C函数生成CBMC规约:
|
|
|
|
|
|
int add_numbers(int a, int b) {
|
|
|
return a + b;
|
|
|
}
|
|
|
|
|
|
验证目标: functional_correctness
|
|
|
|
|
|
生成CBMC规约:
|
|
|
\\requires ...
|
|
|
\\ensures ...
|
|
|
\\assigns ..."""
|
|
|
}
|
|
|
],
|
|
|
"temperature": 0.1,
|
|
|
"max_tokens": 512,
|
|
|
"stream": False
|
|
|
}
|
|
|
|
|
|
print("\n⏳ 调用DeepSeek v3.1 API...")
|
|
|
start_time = time.time()
|
|
|
|
|
|
response = requests.post(
|
|
|
"https://api.siliconflow.cn/v1/chat/completions",
|
|
|
headers=headers,
|
|
|
json=data,
|
|
|
timeout=30
|
|
|
)
|
|
|
|
|
|
response_time = time.time() - start_time
|
|
|
|
|
|
if response.status_code == 200:
|
|
|
result = response.json()
|
|
|
content = result['choices'][0]['message']['content']
|
|
|
tokens_used = result.get('usage', {}).get('total_tokens', 0)
|
|
|
|
|
|
print(f"✅ API调用成功!")
|
|
|
print(f"⏱️ 响应时间: {response_time:.2f}s")
|
|
|
print(f"🔤 消耗Token: {tokens_used}")
|
|
|
|
|
|
print(f"\n📋 生成的CBMC规约:")
|
|
|
print("-" * 40)
|
|
|
print(content)
|
|
|
print("-" * 40)
|
|
|
|
|
|
# 提取CBMC规约
|
|
|
lines = content.split('\n')
|
|
|
cbmc_lines = []
|
|
|
for line in lines:
|
|
|
line = line.strip()
|
|
|
if (line.startswith(r'\requires') or
|
|
|
line.startswith(r'\ensures') or
|
|
|
line.startswith(r'\assigns')):
|
|
|
cbmc_lines.append(line)
|
|
|
|
|
|
if cbmc_lines:
|
|
|
print(f"\n🔧 提取的CBMC规约:")
|
|
|
print("-" * 30)
|
|
|
print('\n'.join(cbmc_lines))
|
|
|
print("-" * 30)
|
|
|
|
|
|
else:
|
|
|
print(f"❌ API调用失败: {response.status_code}")
|
|
|
print(f"错误信息: {response.text}")
|
|
|
|
|
|
except Exception as e:
|
|
|
print(f"❌ 测试失败: {str(e)}")
|
|
|
|
|
|
print(f"\n🎉 快速测试完成!")
|
|
|
|
|
|
|
|
|
if __name__ == "__main__":
|
|
|
quick_deepseek_test() |