Skip to content

Commit 3d737f8

Browse files
K-dizzledK-dizzled
authored
Merge pull request #56 from JetBrains-Research/deepseek-support
Support DeepSeek in benchmarks and plugin
2 parents 6351238 + 3cd6f6c commit 3d737f8

21 files changed

+599
-15
lines changed

‎package.json

+92-5
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@
119119
},
120120
"temperature": {
121121
"type": "number",
122-
"description": "Temperature of the OpenAI model.",
122+
"description": "Temperature of the OpenAI model. Should be in range [0, 2], otherwise an error will be produced.",
123123
"default": 1
124124
},
125125
"apiKey": {
@@ -306,7 +306,7 @@
306306
},
307307
"temperature": {
308308
"type": "number",
309-
"description": "Temperature of the LM Studio model.",
309+
"description": "Temperature of the LM Studio model. Should be in range [0, 2], otherwise an error will be produced.",
310310
"default": 1
311311
},
312312
"port": {
@@ -376,6 +376,93 @@
376376
"markdownDescription": "List of configurations that fetch completions from a locally running LLM inside [LM Studio](https://lmstudio.ai).",
377377
"order": 3
378378
},
379+
"coqpilot.deepSeekModelsParameters": {
380+
"type": "array",
381+
"items": {
382+
"type": "object",
383+
"properties": {
384+
"modelId": {
385+
"type": "string",
386+
"markdownDescription": "Unique identifier of this model to distinguish it from others. Could be any string.",
387+
"default": "deep-seek-v3"
388+
},
389+
"modelName": {
390+
"type": "string",
391+
"markdownDescription": "Model to use from the DeepSeek public API. List of models known to CoqPilot: \n * deepseek-chat \n * deepseek-reasoner",
392+
"default": "deepseek-chat"
393+
},
394+
"temperature": {
395+
"type": "number",
396+
"description": "Temperature of the DeepSeek model. Should be in range [0, 2], otherwise an error will be produced.",
397+
"default": 1
398+
},
399+
"apiKey": {
400+
"type": "string",
401+
"description": "Api key to communicate with the DeepSeek api. You can get one [here](https://platform.deepseek.com/api_keys).",
402+
"default": "None"
403+
},
404+
"choices": {
405+
"type": "number",
406+
"description": "Number of attempts to generate proof for one hole with this model. All attempts are made as a single request, so this parameter should not have a significant impact on performance. However, more choices mean more tokens spent on generation.",
407+
"default": 15
408+
},
409+
"systemPrompt": {
410+
"type": "string",
411+
"description": "Prompt for the DeepSeek model to begin a chat with. It is sent as a system message, which means it has more impact than other messages.",
412+
"default": "Generate proof of the theorem from user input in Coq. You should only generate proofs in Coq. Never add special comments to the proof. Your answer should be a valid Coq proof. It should start with 'Proof.' and end with 'Qed.'."
413+
},
414+
"maxTokensToGenerate": {
415+
"type": "number",
416+
"description": "Number of tokens that the model is allowed to generate as a response message (i.e. message with proof).",
417+
"default": 2048
418+
},
419+
"tokensLimit": {
420+
"type": "number",
421+
"description": "Total length of input and generated tokens, it is determined by the model.",
422+
"default": 4096
423+
},
424+
"maxContextTheoremsNumber": {
425+
"type": "number",
426+
"description": "Maximum number of context theorems to include in the prompt sent to the DeepSeek model as examples for proof generation. Lower values reduce token usage but may decrease the likelihood of generating correct proofs.",
427+
"default": 100
428+
},
429+
"multiroundProfile": {
430+
"type": "object",
431+
"properties": {
432+
"maxRoundsNumber": {
433+
"type": "number",
434+
"description": "Maximum number of rounds to generate and further fix the proof. Default value is 1, which means each proof will be only generated, but not fixed.",
435+
"default": 1
436+
},
437+
"proofFixChoices": {
438+
"type": "number",
439+
"description": "Number of attempts to generate a proof fix for each proof in one round. Warning: increasing `proofFixChoices` can lead to exponential growth in generation requests if `maxRoundsNumber` is relatively large.",
440+
"default": 1
441+
},
442+
"proofFixPrompt": {
443+
"type": "string",
444+
"description": "Prompt for the proof-fix request that will be sent as a user chat message in response to an incorrect proof. It may include the `${diagnostic}` substring, which will be replaced by the actual compiler diagnostic.",
445+
"default": "Unfortunately, the last proof is not correct. Here is the compiler's feedback: `${diagnostic}`. Please, fix the proof."
446+
},
447+
"maxPreviousProofVersionsNumber": {
448+
"type": "number",
449+
"description": "Maximum number of previous proof versions to include in the proof-fix chat, each presented as a dialogue: the user's diagnostic followed by the assistant's corresponding proof attempt. The most recent proof version being fixed is always included and is not affected by this parameter.",
450+
"default": 100
451+
}
452+
},
453+
"default": {
454+
"maxRoundsNumber": 1,
455+
"proofFixChoices": 1,
456+
"proofFixPrompt": "Unfortunately, the last proof is not correct. Here is the compiler's feedback: `${diagnostic}`. Please, fix the proof.",
457+
"maxPreviousProofVersionsNumber": 100
458+
}
459+
}
460+
}
461+
},
462+
"default": [],
463+
"markdownDescription": "List of configurations for DeepSeek models. Each configuration will be fetched for completions independently in the order they are listed.",
464+
"order": 4
465+
},
379466
"coqpilot.contextTheoremsRankerType": {
380467
"type": "string",
381468
"enum": [
@@ -390,7 +477,7 @@
390477
],
391478
"description": "Context of the LLM is limited. Usually not all theorems from the file may be used in the completion request. This parameter defines the way theorems are selected for the completion.",
392479
"default": "distance",
393-
"order": 4
480+
"order": 5
394481
},
395482
"coqpilot.loggingVerbosity": {
396483
"type": "string",
@@ -404,13 +491,13 @@
404491
],
405492
"description": "The verbosity of the logs.",
406493
"default": "info",
407-
"order": 5
494+
"order": 6
408495
},
409496
"coqpilot.coqLspServerPath": {
410497
"type": "string",
411498
"description": "Path to the Coq LSP server. If not specified, CoqPilot will try to find the server automatically at the default location: coq-lsp at PATH.",
412499
"default": "coq-lsp",
413-
"order": 6
500+
"order": 7
414501
}
415502
}
416503
}

‎src/benchmark/framework/experiment/setupDSL/benchmarkingBundleBuilder.ts

+7-2
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@ export type LLMServiceStringIdentifier =
1010
| "predefined"
1111
| "openai"
1212
| "grazie"
13-
| "lmstudio";
13+
| "lmstudio"
14+
| "deepseek";
1415

1516
export type CorrespondingInputParams<T extends LLMServiceStringIdentifier> =
1617
T extends "predefined"
@@ -21,7 +22,9 @@ export type CorrespondingInputParams<T extends LLMServiceStringIdentifier> =
2122
? InputBenchmarkingModelParams.GrazieParams
2223
: T extends "lmstudio"
2324
? InputBenchmarkingModelParams.LMStudioParams
24-
: never;
25+
: T extends "deepseek"
26+
? InputBenchmarkingModelParams.DeepSeekParams
27+
: never;
2528

2629
export class BenchmarkingBundle {
2730
constructor() {}
@@ -46,6 +49,8 @@ export class BenchmarkingBundle {
4649
return LLMServiceIdentifier.GRAZIE;
4750
case "lmstudio":
4851
return LLMServiceIdentifier.LMSTUDIO;
52+
case "deepseek":
53+
return LLMServiceIdentifier.DEEPSEEK;
4954
}
5055
}
5156
}

‎src/benchmark/framework/structures/common/llmServiceIdentifier.ts

+1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,5 @@ export enum LLMServiceIdentifier {
33
OPENAI = "Open AI",
44
GRAZIE = "Grazie",
55
LMSTUDIO = "LM Studio",
6+
DEEPSEEK = "DeepSeek",
67
}

‎src/benchmark/framework/structures/inputParameters/inputBenchmarkingModelParams.ts

+3
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import {
2+
DeepSeekUserModelParams,
23
GrazieUserModelParams,
34
LMStudioUserModelParams,
45
OpenAiUserModelParams,
@@ -22,4 +23,6 @@ export namespace InputBenchmarkingModelParams {
2223
export interface GrazieParams extends GrazieUserModelParams, Params {}
2324

2425
export interface LMStudioParams extends LMStudioUserModelParams, Params {}
26+
27+
export interface DeepSeekParams extends DeepSeekUserModelParams, Params {}
2528
}

‎src/benchmark/framework/utils/commonStructuresUtils/llmServicesUtils.ts

+11
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
import { ErrorsHandlingMode } from "../../../../llm/llmServices/commonStructures/errorsHandlingMode";
2+
import { DeepSeekModelParamsResolver } from "../../../../llm/llmServices/deepSeek/deepSeekModelParamsResolver";
3+
import { DeepSeekService } from "../../../../llm/llmServices/deepSeek/deepSeekService";
24
import { GrazieModelParamsResolver } from "../../../../llm/llmServices/grazie/grazieModelParamsResolver";
35
import { GrazieService } from "../../../../llm/llmServices/grazie/grazieService";
46
import { LLMService } from "../../../../llm/llmServices/llmService";
@@ -29,6 +31,8 @@ export function getShortName(identifier: LLMServiceIdentifier): string {
2931
return "Grazie";
3032
case LLMServiceIdentifier.LMSTUDIO:
3133
return "LM Studio";
34+
case LLMServiceIdentifier.DEEPSEEK:
35+
return "DeepSeek";
3236
}
3337
}
3438

@@ -53,6 +57,9 @@ export function selectLLMServiceBuilder(
5357
case LLMServiceIdentifier.LMSTUDIO:
5458
return (eventLogger, errorsHandlingMode) =>
5559
new LMStudioService(eventLogger, errorsHandlingMode);
60+
case LLMServiceIdentifier.DEEPSEEK:
61+
return (eventLogger, errorsHandlingMode) =>
62+
new DeepSeekService(eventLogger, errorsHandlingMode);
5663
}
5764
}
5865

@@ -61,6 +68,7 @@ export interface LLMServicesParamsResolvers {
6168
openAiModelParamsResolver: OpenAiModelParamsResolver;
6269
grazieModelParamsResolver: GrazieModelParamsResolver;
6370
lmStudioModelParamsResolver: LMStudioModelParamsResolver;
71+
deepSeekModelParamsResolver: DeepSeekModelParamsResolver;
6472
}
6573

6674
export function createParamsResolvers(): LLMServicesParamsResolvers {
@@ -70,6 +78,7 @@ export function createParamsResolvers(): LLMServicesParamsResolvers {
7078
openAiModelParamsResolver: new OpenAiModelParamsResolver(),
7179
grazieModelParamsResolver: new GrazieModelParamsResolver(),
7280
lmStudioModelParamsResolver: new LMStudioModelParamsResolver(),
81+
deepSeekModelParamsResolver: new DeepSeekModelParamsResolver(),
7382
};
7483
}
7584

@@ -86,5 +95,7 @@ export function getParamsResolver(
8695
return paramsResolvers.grazieModelParamsResolver;
8796
case LLMServiceIdentifier.LMSTUDIO:
8897
return paramsResolvers.lmStudioModelParamsResolver;
98+
case LLMServiceIdentifier.DEEPSEEK:
99+
return paramsResolvers.deepSeekModelParamsResolver;
89100
}
90101
}

‎src/extension/pluginContext.ts

+7
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import { Disposable, WorkspaceConfiguration, window, workspace } from "vscode";
55

66
import { LLMServices, disposeServices } from "../llm/llmServices";
77
import { ErrorsHandlingMode } from "../llm/llmServices/commonStructures/errorsHandlingMode";
8+
import { DeepSeekService } from "../llm/llmServices/deepSeek/deepSeekService";
89
import { GrazieService } from "../llm/llmServices/grazie/grazieService";
910
import { LMStudioService } from "../llm/llmServices/lmStudio/lmStudioService";
1011
import { OpenAiService } from "../llm/llmServices/openai/openAiService";
@@ -67,6 +68,12 @@ export class PluginContext implements Disposable {
6768
path.join(this.llmServicesLogsDir, "lmstudio-logs.txt"),
6869
this.llmServicesSetup.debugLogs
6970
),
71+
deepSeekService: new DeepSeekService(
72+
this.llmServicesSetup.eventLogger,
73+
this.llmServicesSetup.errorsHandlingMode,
74+
path.join(this.llmServicesLogsDir, "deepseek-logs.txt"),
75+
this.llmServicesSetup.debugLogs
76+
),
7077
};
7178

7279
private parseLoggingVerbosity(config: WorkspaceConfiguration): Severity {

‎src/extension/settings/configReaders.ts

+25-2
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,13 @@ import { LLMService } from "../../llm/llmServices/llmService";
66
import { ModelParams, ModelsParams } from "../../llm/llmServices/modelParams";
77
import { SingleParamResolutionResult } from "../../llm/llmServices/utils/paramsResolvers/abstractResolvers";
88
import {
9+
DeepSeekUserModelParams,
910
GrazieUserModelParams,
1011
LMStudioUserModelParams,
1112
OpenAiUserModelParams,
1213
PredefinedProofsUserModelParams,
1314
UserModelParams,
15+
deepSeekUserModelParamsSchema,
1416
grazieUserModelParamsSchema,
1517
lmStudioUserModelParamsSchema,
1618
openAiUserModelParamsSchema,
@@ -108,14 +110,27 @@ export function readAndValidateUserModelsParams(
108110
jsonSchemaValidator
109111
)
110112
);
113+
const deepSeekUserParams: DeepSeekUserModelParams[] =
114+
config.deepSeekModelsParameters.map((params: any) =>
115+
validateAndParseJson(
116+
params,
117+
deepSeekUserModelParamsSchema,
118+
jsonSchemaValidator
119+
)
120+
);
111121

112122
validateIdsAreUnique([
113123
...predefinedProofsUserParams,
114124
...openAiUserParams,
115125
...grazieUserParams,
116126
...lmStudioUserParams,
127+
...deepSeekUserParams,
117128
]);
118-
validateApiKeysAreProvided(openAiUserParams, grazieUserParams);
129+
validateApiKeysAreProvided(
130+
openAiUserParams,
131+
grazieUserParams,
132+
deepSeekUserParams
133+
);
119134

120135
const modelsParams: ModelsParams = {
121136
predefinedProofsModelParams: resolveParamsAndShowResolutionLogs(
@@ -134,6 +149,10 @@ export function readAndValidateUserModelsParams(
134149
llmServices.lmStudioService,
135150
lmStudioUserParams
136151
),
152+
deepSeekParams: resolveParamsAndShowResolutionLogs(
153+
llmServices.deepSeekService,
154+
deepSeekUserParams
155+
),
137156
};
138157

139158
validateModelsArePresent([
@@ -198,7 +217,8 @@ function validateIdsAreUnique(allModels: UserModelParams[]) {
198217

199218
function validateApiKeysAreProvided(
200219
openAiUserParams: OpenAiUserModelParams[],
201-
grazieUserParams: GrazieUserModelParams[]
220+
grazieUserParams: GrazieUserModelParams[],
221+
deepSeekUserParams: DeepSeekUserModelParams[]
202222
) {
203223
const buildApiKeyError = (
204224
serviceName: string,
@@ -218,6 +238,9 @@ function validateApiKeysAreProvided(
218238
if (grazieUserParams.some((params) => params.apiKey === "None")) {
219239
throw buildApiKeyError("Grazie", "grazie");
220240
}
241+
if (deepSeekUserParams.some((params) => params.apiKey === "None")) {
242+
throw buildApiKeyError("Deep Seek", "deepSeek");
243+
}
221244
}
222245

223246
function validateModelsArePresent<T>(allModels: T[]) {

‎src/extension/settings/settingsValidationError.ts

+2-1
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,8 @@ export function toSettingName(llmService: LLMService<any, any>): string {
3434
() => "predefinedProofs",
3535
() => "openAi",
3636
() => "grazie",
37-
() => "lmStudio"
37+
() => "lmStudio",
38+
() => "deepSeek"
3839
);
3940
return `${pluginId}.${serviceNameInSettings}ModelsParameters`;
4041
}

‎src/llm/llmIterator.ts

+11
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ export class LLMSequentialIterator
3636
);
3737
}
3838

39+
// TODO: Implement a smarter way of ordering the services
3940
private createHooks(
4041
proofGenerationContext: ProofGenerationContext,
4142
modelsParams: ModelsParams,
@@ -48,6 +49,16 @@ export class LLMSequentialIterator
4849
services.predefinedProofsService,
4950
"predefined-proofs"
5051
),
52+
// Here DeepSeek service is reordered to the beginning
53+
// of the list, due to it's strong performance and
54+
// low costs. Refer to discussion:
55+
// https://github.com/JetBrains-Research/coqpilot/pull/56#discussion_r1935180516
56+
...this.createLLMServiceHooks(
57+
proofGenerationContext,
58+
modelsParams.deepSeekParams,
59+
services.deepSeekService,
60+
"deepseek"
61+
),
5162
...this.createLLMServiceHooks(
5263
proofGenerationContext,
5364
modelsParams.openAiParams,

0 commit comments

Comments
 (0)