Revise and implemented requested changes from PR#56 review

K-dizzled · K-dizzled · commit 6cb827da42d1 · 2025-01-31T12:13:08.000+01:00
diff --git a/src/benchmark/framework/experiment/setupDSL/benchmarkingBundleBuilder.ts b/src/benchmark/framework/experiment/setupDSL/benchmarkingBundleBuilder.ts
@@ -21,9 +21,9 @@ export type CorrespondingInputParams<T extends LLMServiceStringIdentifier> =
           : T extends "grazie"
             ? InputBenchmarkingModelParams.GrazieParams
             : T extends "lmstudio"
-              ? InputBenchmarkingModelParams.DeepSeekParams
+              ? InputBenchmarkingModelParams.LMStudioParams
               : T extends "deepseek"
-                ? InputBenchmarkingModelParams.LMStudioParams
+                ? InputBenchmarkingModelParams.DeepSeekParams
                 : never;
 
 export class BenchmarkingBundle {
diff --git a/src/extension/settings/configReaders.ts b/src/extension/settings/configReaders.ts
@@ -126,7 +126,7 @@ export function readAndValidateUserModelsParams(
         ...lmStudioUserParams,
         ...deepSeekUserParams,
     ]);
-    validateApiKeysAreProvided(openAiUserParams, grazieUserParams);
+    validateApiKeysAreProvided(openAiUserParams, grazieUserParams, deepSeekUserParams);
 
     const modelsParams: ModelsParams = {
         predefinedProofsModelParams: resolveParamsAndShowResolutionLogs(
@@ -213,7 +213,8 @@ function validateIdsAreUnique(allModels: UserModelParams[]) {
 
 function validateApiKeysAreProvided(
     openAiUserParams: OpenAiUserModelParams[],
-    grazieUserParams: GrazieUserModelParams[]
+    grazieUserParams: GrazieUserModelParams[],
+    deepSeekUserParams: DeepSeekUserModelParams[]
 ) {
     const buildApiKeyError = (
         serviceName: string,
@@ -233,6 +234,9 @@ function validateApiKeysAreProvided(
     if (grazieUserParams.some((params) => params.apiKey === "None")) {
         throw buildApiKeyError("Grazie", "grazie");
     }
+    if (deepSeekUserParams.some((params) => params.apiKey === "None")) {
+        throw buildApiKeyError("Deep Seek", "deepSeek");
+    }
 }
 
 function validateModelsArePresent<T>(allModels: T[]) {
diff --git a/src/llm/llmIterator.ts b/src/llm/llmIterator.ts
@@ -36,6 +36,7 @@ export class LLMSequentialIterator
         );
     }
 
+    // TODO: Implement a smarter way of ordering the services
     private createHooks(
         proofGenerationContext: ProofGenerationContext,
         modelsParams: ModelsParams,
@@ -48,6 +49,16 @@ export class LLMSequentialIterator
                 services.predefinedProofsService,
                 "predefined-proofs"
             ),
+            // Here DeepSeek service is reordered to the beginning
+            // of the list, due to it's strong performance and
+            // low costs. Refer to discussion: 
+            // https://github.com/JetBrains-Research/coqpilot/pull/56#discussion_r1935180516
+            ...this.createLLMServiceHooks(
+                proofGenerationContext,
+                modelsParams.deepSeekParams,
+                services.deepSeekService,
+                "deepseek"
+            ),
             ...this.createLLMServiceHooks(
                 proofGenerationContext,
                 modelsParams.openAiParams,
@@ -66,12 +77,6 @@ export class LLMSequentialIterator
                 services.lmStudioService,
                 "lm-studio"
             ),
-            ...this.createLLMServiceHooks(
-                proofGenerationContext,
-                modelsParams.deepSeekParams,
-                services.deepSeekService,
-                "deepseek"
-            ),
         ];
     }
 
diff --git a/src/llm/llmServices/deepSeek/deepSeekModelParamsResolver.ts b/src/llm/llmServices/deepSeek/deepSeekModelParamsResolver.ts
@@ -19,8 +19,8 @@ export class DeepSeekModelParamsResolver
         .requiredToBeConfigured()
         .validate([
             (value) =>
-                DeepSeekModelParamsResolver._allowedModels.includes(value),
-            `be one of the allowed models: ${DeepSeekModelParamsResolver._allowedModels.join(
+                DeepSeekModelParamsResolver.allowedModels.includes(value),
+            `be one of the allowed models: ${DeepSeekModelParamsResolver.allowedModels.join(
                 ", "
             )}`,
         ]);
@@ -36,5 +36,5 @@ export class DeepSeekModelParamsResolver
         .requiredToBeConfigured()
         .validateAtRuntimeOnly();
 
-    static readonly _allowedModels = ["deepseek-chat", "deepseek-reasoner"];
+    static readonly allowedModels = ["deepseek-chat", "deepseek-reasoner"];
 }
diff --git a/src/llm/llmServices/deepSeek/deepSeekService.ts b/src/llm/llmServices/deepSeek/deepSeekService.ts
@@ -11,11 +11,11 @@ import { ProofVersion } from "../commonStructures/proofVersion";
 import { GeneratedProofImpl } from "../generatedProof";
 import { LLMServiceImpl } from "../llmService";
 import { LLMServiceInternal } from "../llmServiceInternal";
-import { OpenAiModelParams } from "../modelParams";
 import { DeepSeekModelParams } from "../modelParams";
 import { toO1CompatibleChatHistory } from "../utils/o1ClassModels";
 
 import { DeepSeekModelParamsResolver } from "./deepSeekModelParamsResolver";
+import { illegalState } from "../../../utils/throwErrors";
 
 export class DeepSeekService extends LLMServiceImpl<
     DeepSeekUserModelParams,
@@ -31,8 +31,6 @@ export class DeepSeekService extends LLMServiceImpl<
         this.generationsLoggerBuilder
     );
     protected readonly modelParamsResolver = new DeepSeekModelParamsResolver();
-
-    static readonly baseApiUrl = "https://api.deepseek.com/v1";
 }
 
 export class DeepSeekGeneratedProof extends GeneratedProofImpl<
@@ -44,7 +42,7 @@ export class DeepSeekGeneratedProof extends GeneratedProofImpl<
     constructor(
         rawProof: GeneratedRawContentItem,
         proofGenerationContext: ProofGenerationContext,
-        modelParams: OpenAiModelParams,
+        modelParams: DeepSeekModelParams,
         llmServiceInternal: DeepSeekServiceInternal,
         previousProofVersions?: ProofVersion[]
     ) {
@@ -64,10 +62,12 @@ class DeepSeekServiceInternal extends LLMServiceInternal<
     DeepSeekGeneratedProof,
     DeepSeekServiceInternal
 > {
+    static readonly baseApiUrl = "https://api.deepseek.com/v1";
+
     constructGeneratedProof(
         rawProof: GeneratedRawContentItem,
         proofGenerationContext: ProofGenerationContext,
-        modelParams: OpenAiModelParams,
+        modelParams: DeepSeekModelParams,
         previousProofVersions?: ProofVersion[] | undefined
     ): DeepSeekGeneratedProof {
         return new DeepSeekGeneratedProof(
@@ -81,22 +81,22 @@ class DeepSeekServiceInternal extends LLMServiceInternal<
 
     async generateFromChatImpl(
         analyzedChat: AnalyzedChatHistory,
-        params: OpenAiModelParams,
+        params: DeepSeekModelParams,
         choices: number
     ): Promise<GeneratedRawContent> {
         LLMServiceInternal.validateChoices(choices);
 
-        const openai = new OpenAI({
+        const openaiCompatibleApi = new OpenAI({
             apiKey: params.apiKey,
-            baseURL: DeepSeekService.baseApiUrl,
+            baseURL: DeepSeekServiceInternal.baseApiUrl,
         });
         const formattedChat = this.formatChatHistory(analyzedChat.chat, params);
         this.logDebug.event("Completion requested", {
             history: formattedChat,
         });
 
         try {
-            const completion = await openai.chat.completions.create({
+            const completion = await openaiCompatibleApi.chat.completions.create({
                 messages: formattedChat,
                 model: params.modelName,
                 n: choices,
@@ -107,7 +107,7 @@ class DeepSeekServiceInternal extends LLMServiceInternal<
             const rawContentItems = completion.choices.map((choice) => {
                 const content = choice.message.content;
                 if (content === null) {
-                    throw Error("response message content is null");
+                    illegalState("response message content is null");
                 }
                 return content;
             });
@@ -131,7 +131,7 @@ class DeepSeekServiceInternal extends LLMServiceInternal<
         rawContentItems: string[],
         tokensUsage: OpenAI.Completions.CompletionUsage | undefined,
         analyzedChat: AnalyzedChatHistory,
-        params: OpenAiModelParams
+        params: DeepSeekModelParams
     ): GeneratedRawContent {
         const promptTokens =
             tokensUsage?.prompt_tokens ??
@@ -150,8 +150,8 @@ class DeepSeekServiceInternal extends LLMServiceInternal<
 
     private formatChatHistory(
         chat: ChatHistory,
-        modelParams: OpenAiModelParams
+        modelParams: DeepSeekModelParams
     ): ChatHistory {
-        return toO1CompatibleChatHistory(chat, modelParams.modelName, "openai");
+        return toO1CompatibleChatHistory(chat, modelParams.modelName, "deepseek");
     }
 }
diff --git a/src/llm/llmServices/utils/o1ClassModels.ts b/src/llm/llmServices/utils/o1ClassModels.ts
@@ -9,6 +9,10 @@ const o1ClassModelsOpenAI = [
 
 const o1ClassModelsGrazie = ["openai-o1", "openai-o1-mini"];
 
+// TODO: When DeepSeek API becomes stable: 
+// check whether the r1 model chat history is compatible with o1 model
+const o1ClassModelsDeepSeek = ["deepseek-reasoner"];
+
 /**
  * As of November 2024, o1 model requires a different format of chat history.
  * It doesn't support the system prompt, therefore we manually
@@ -18,10 +22,15 @@ const o1ClassModelsGrazie = ["openai-o1", "openai-o1-mini"];
 export function toO1CompatibleChatHistory(
     chatHistory: ChatHistory,
     modelName: string,
-    service: "openai" | "grazie"
+    service: "openai" | "grazie" | "deepseek"
 ): ChatHistory {
     const o1ClassModels =
-        service === "openai" ? o1ClassModelsOpenAI : o1ClassModelsGrazie;
+        service === "openai"
+            ? o1ClassModelsOpenAI
+            : service === "grazie"
+            ? o1ClassModelsGrazie
+            : o1ClassModelsDeepSeek;
+        
     if (o1ClassModels.includes(modelName)) {
         return chatHistory.map((message: ChatMessage) => {
             return {
diff --git a/src/test/llm/parseUserModelParams.test.ts b/src/test/llm/parseUserModelParams.test.ts
@@ -66,7 +66,7 @@ suite("Parse `UserModelParams` from JSON test", () => {
     const validOpenAiUserModelParamsComplete = {
         ...validUserModelParamsCompelete,
         modelName: "gpt-model",
-        temperature: 36.6,
+        temperature: 0.8,
         apiKey: "api-key",
     };
     const validGrazieUserModelParamsComplete = {
@@ -77,13 +77,13 @@ suite("Parse `UserModelParams` from JSON test", () => {
     };
     const validLMStudioUserModelParamsComplete = {
         ...validUserModelParamsCompelete,
-        temperature: 36.6,
+        temperature: 0.8,
         port: 555,
     };
     const validDeepSeekUserModelParamsComplete = {
         ...validUserModelParamsCompelete,
         modelName: "deepseek-chat",
-        temperature: 36.6,
+        temperature: 0.8,
         apiKey: "api-key",
     };
 
